1. a : {2...}
2. b : 
3. k : 
4. k1:. 
4. k1<k
4. 
4. (g,h:({a..b}).
4. (is_prime_factorization(a; b; g) & is_prime_factorization(a; b; h)
4. (
4. ({a..b}(g) = k1  {a..b}(g) = {a..b}(h)  g = h)
5. g : {a..b}
6. h : {a..b}
7. is_prime_factorization(a; b; g)
8. is_prime_factorization(a; b; h)
9. {a..b}(g) = k
10. {a..b}(g) = {a..b}(h)
11. (j:{a..b}. 0<g(j))
  g = h

By:	Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. 0<f(i)) Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  f = (x.0)

1

12. {a..b}(g) = 1 13. {a..b}(h) = 1 14. g = (x.0) 15. h = (x.0)   g = h

Trivial

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