k:{2...}, g:({2..k
}
), z:{2..k}.
Thm*
prime(z)
Thm*
Thm* (
g':({2..k}).
Thm* (
{2..k}(g) = {2..k}(g')
Thm* (& g'(z) = 0
Thm* (& (
u:{2..k}. z<u g'(u) = g(u)))k:{2...}, g:({2..k}), x,y:{2..k}.
Thm* x
y<k
Thm*
Thm* (
h:({2..k}).
Thm* (
{2..k}(g) = {2..k}(h)
Thm* (& h(x
y) = 0
Thm* (& (
u:{2..k}. xy<u h(u) = g(u)))x:. prime(x) 
x<2 
(i,j:{2..x}. x = ij)