Nuprl - FTA LEMMAs for prime_factorization

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

Rank	Theorem	Name
12	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]
cites the following:
11	Thm* x:. prime(x) 2x	[natprimes_lb]
0	Thm* f:(Prime), x:Prime. prime_mset_complete(f)(x) = f(x)	[prime_mset_complete_isext]

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