1. f : Prime
2. n : 
3. n' : 
4. nn'
5. f is a factorization of n
6. f is a factorization of n'
7. x:Prime. n'<x  f(x) = 0
8. n' = {2..n'+1}(prime_mset_complete(f))
9. x:Prime. n<x  f(x) = 0
10. n = {2..n+1}(prime_mset_complete(f))
11. 0<n
  {2..n+1}(prime_mset_complete(f)) = {2..n'+1}(prime_mset_complete(f))

By:	Rewrite by Thm*  a,c,b:, f:({a..b}). Thm*  ac  cb  {a..b}(f) = {a..c}(f){c..b}(f) Using:[a:= 2 | b:= n'+1 | c:= n+1 | f:= prime_mset_complete(f)]

1

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

6 steps

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