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))

By:	FwdThru: Thm*  x:. prime(x)  x<2  (i,j:{2..x}. x = ij) on [ prime(z) ] THEN Analyze-1 ... THEN ExistHD Hyp:-1 THEN Inst: Hyp:3 Using:[i | j] ...a

1

6. i : {2..z} 7. j : {2..z} 8. z = ij 9. h:({2..k}).  9. {2..k}(g) = {2..k}(h) & h(ij) = 0 & (u:{2..k}. ij<u  h(u) = g(u))   g':({2..k}).    {2..k}(g) = {2..k}(g') & g'(z) = 0 & (u:{2..k}. z<u  g'(u) = g(u))

1 step

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