k:{2...}, g:({2..k}), x,y:{2..k}.
  xy<k
  
  x<y
  
  {2..k}(g) = {2..k}(split_factor2(g; x; y))
  & split_factor2(g; x; y)(xy) = 0
  & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))

By:	UnivCD ...w THEN Inst: Thm*  i,j:{2...}. i<ij & j<ij Using:[x | y]

1

1. k : {2...} 2. g : {2..k} 3. x : {2..k} 4. y : {2..k} 5. xy<k 6. x<y 7. x<xy & y<xy   {2..k}(g) = {2..k}(split_factor2(g; x; y))   & split_factor2(g; x; y)(xy) = 0   & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))

4 steps

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