1. n : 
2. f : Prime
3. g : Prime
4. f is a factorization of n
5. g is a factorization of n
6. (x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x))
6. 
6. f = g
7. x : {2..(n+1)}
  prime_mset_complete(f)(x) = prime_mset_complete(g)(x)

1

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. x : {2..(n+1)}   prime_mset_complete(f)(x) = prime_mset_complete(g)(x)

2 steps

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