n:, f,g:(Prime).
  f is a factorization of n
  
  g is a factorization of n
  
  (x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x))
  
  f = g

1

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) 7. x : Prime   f(x) = g(x)

5 steps

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