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

By:	ApFun: prime_mset_complete(f) = prime_mset_complete(g)  {2..(n+1)} to: x

1

prime_mset_complete(f) = prime_mset_complete(g)  {2..(n+1)}

1 step

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