At: prime factorization exists2

  n:{1...}. f:(Prime). f is a factorization of n

By:	SimilarTo Thm*  n:{1...}.  Thm*  h:({2..(n+1)}).  Thm*  n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)

1

1. n : {1...} 2. h:({2..(n+1)}). n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)   f:(Prime). f is a factorization of n

10 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html