k:{2...}, g:({2..k}), z:{2..k}.
  prime(z)
  
  (g':({2..k}). 
  ({2..k}(g) = {2..k}(g')
  (& g'(z) = 0
  (& (u:{2..k}. z<u  g'(u) = g(u)))

By:	SimilarTo Thm*  k:{2...}, g:({2..k}), x,y:{2..k}. Thm*  xy<k Thm*   Thm*  (h:({2..k}).  Thm*  ({2..k}(g) = {2..k}(h) Thm*  (& h(xy) = 0 Thm*  (& (u:{2..k}. xy<u  h(u) = g(u)))

1

1. k : {2...} 2. g : {2..k} 3. x,y:{2..k}. 3. xy<k 3.  3. (h:({2..k}).  3. ({2..k}(g) = {2..k}(h) 3. (& h(xy) = 0 3. (& (u:{2..k}. xy<u  h(u) = g(u))) 4. z : {2..k} 5. prime(z)   g':({2..k}).    {2..k}(g) = {2..k}(g') & g'(z) = 0 & (u:{2..k}. z<u  g'(u) = g(u))

2 steps

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