1. n : 
2. f : Prime
3. g : Prime
4. x:Prime. n<x  f(x) = 0
5. n = {2..n+1}(prime_mset_complete(f))
6. x:Prime. n<x  g(x) = 0
7. n = {2..n+1}(prime_mset_complete(g))
8. (x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x))
8. 
8. f = g
9. {2..(n+1)}
  prime_mset_complete(f) = prime_mset_complete(g)  {2..(n+1)}

By:	BackThru:  Thm*  a:{2...}, b:, g,h:({a..b}). Thm*  is_prime_factorization(a; b; g) Thm*   Thm*  is_prime_factorization(a; b; h)  {a..b}(g) = {a..b}(h)  g = h THEN BackThru:  Thm*  f:(Prime), b:. is_prime_factorization(2; b; prime_mset_complete(f))

None

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