2. n :
3. n' :
4. n
n'
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
12. i : {(n+1)..(n'+1)
}
13. prime(i)
f(i) = 0
