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)
  g = h

By:	Decide: j:{a..b}. 0<g(j) ...w

1	11. j:{a..b}. 0<g(j)   g = h	8 steps
2	11. (j:{a..b}. 0<g(j))   g = h	2 steps

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