a,b:
, j:{a..b
}. 
{a..b}(trivial_factorization(j)) = ja,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))x,y:. x 
y trivial_factorization(x)(y) = 0 
x,y:. x = y trivial_factorization(x)(y) = 1 x:. x1 = xa,b:, e:({a..b}). (i:{a..b}. e(i) = 1) ( i:{a..b}. e(i)) = 1