1. a : 
2. b : 
3. f : {a..b}
4. j : {a..b}
5. 2j
6. 0<f(j)
  {a..b}(reduce_factorization(f; j))<j{a..b}(reduce_factorization(f; j))

By:	BackThru: Thm*  i:{2...}, j:{1...}. j<ij ...

1

{a..b}(reduce_factorization(f; j))  {1...}

1 step

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