1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k
5. x<xx
6. h : {2..k}
7. h = split_factor1(g; x)
8. h(xx) = 0
9. h(x) = g(x)+g(xx)+g(xx)
10. u:{2..k}. u = x  u = xx  h(u) = g(u)
  {2..x}(g)xg(x){x+1..xx}(g)(xx)g(xx){xx+1..k}(g)
  =
  {2..x}(h)xh(x){x+1..xx}(h)(xx)h(xx){xx+1..k}(h)

By:	MulFactorOut [{2..x}(g),{2..x}(h) ;{x+1..xx}(g),{x+1..xx}(h) ;{xx+1..k}(g),{xx+1..k}(h)] Concl ...a

1	{2..x}(g) = {2..x}(h)	1 step
2	{x+1..xx}(g) = {x+1..xx}(h)	1 step
3	{xx+1..k}(g) = {xx+1..k}(h)	1 step
4	xg(x)(xx)g(xx) = xh(x)(xx)h(xx)	PREMISE

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