2. b :
3. f : {a..b
}
4. j : {a..b
}
5. 2
j
6. 0<f(j)
{a..b}(reduce_factorization(f; j))<{a..b}(f)
}
}
j
{a..b}(reduce_factorization(f; j))<{a..b}(f)| By: |
Thm*  a,b:, f:({a..b}), z:{a..b}.
Thm* 0<f(z)   {a..b}(f) = z {a..b}(reduce_factorization(f; z))
Using:[z:= j] ... |
| 1 |
{a..b}(reduce_factorization(f; j))<j{a..b}(reduce_factorization(f; j)) | 2 steps |
About:
 |  |  |  |  |  |  |  |  |