a:
, b:
, f:({a..b
}
), j:{a..b}.
Thm* 2
j 
0<f(j) 
{a..b}(reduce_factorization(f; j))<{a..b}(f)a,b:, f:({a..b}), z:{a..b}.
Thm* 0<f(z)
{a..b}(f) = z
{a..b}(reduce_factorization(f; z))i:{2...}, j:{1...}. j<ija:, b:, f:({a..b}). {a..b}(f) 