1. a : 
2. b : 
3. j : {a..b}
4. trivial_factorization(j)(j) = 1
  ( i:{a..j}. 1)j( i:{j+1..b}. 1) = j

By:	Rewrite by Thm*  a,b:, e:({a..b}). (i:{a..b}. e(i) = 1)  ( i:{a..b}. e(i)) = 1

1

1j1 = j

Auto

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