Def  f is a factorization of k
Def  == (x:Prime. k<x  f(x) = 0) & k = {2..k+1}(prime_mset_complete(f))

is mentioned by

Thm*  n:{1...}. !f:(Prime). f is a factorization of n	[fta_mset]
Thm*  n:, f,g:(Prime). Thm*  f is a factorization of n  g is a factorization of n  f = g	[prime_factorization_mset_unique]
Thm*  n:{1...}. f:(Prime). f is a factorization of n	[prime_factorization_exists2]
Thm*  f:(Prime), n,n':. Thm*  f is a factorization of n  f is a factorization of n'  n = n'	[only_one_factored_by]
Thm*  f:(Prime), n:. f is a factorization of n  0<n	[only_positives_prime_fed]
Thm*  n:, f,g:(Prime). Thm*  f is a factorization of n Thm*   Thm*  g is a factorization of n Thm*   Thm*  (x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x)) Thm*   Thm*  f = g	[prime_factorization_limit]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html