2. b :
3. j : {a..b
}
(
i:{a..b}. i
trivial_factorization(j)(i)) = j
}
( i:{a..b}. itrivial_factorization(j)(i)) = j| By: |
Thm*  a,c,b:, e:({a..b}  ).
Thm* a  c
Thm*  
Thm* c<b Thm*
Thm* ( i:{a..b}. e(i)) = ( i:{a..c}. e(i)) e(c)( i:{c+1..b}. e(i))
Using:[c:= j] |
| 1 |
( i:{a..j}. itrivial_factorization(j)(i))
 jtrivial_factorization(j)(j)( i:{j+1..b}. itrivial_factorization(j)(i))
=
j | 4 steps |
About:
 |  |  |  |  |  |  |  |  |  |  |