k:{2...}, g:({2..k}), x:{2..k}.
  xx<k
  
  {2..k}(g) = {2..k}(split_factor1(g; x))
  & split_factor1(g; x)(xx) = 0
  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))

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

1

1. k : {2...} 2. g : {2..k} 3. x : {2..k} 4. xx<k 5. x<xx & x<xx   {2..k}(g) = {2..k}(split_factor1(g; x))   & split_factor1(g; x)(xx) = 0   & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))

4 steps

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