a,b:
, f:({a..b
}
), j:{a..b}.
Thm* 0<f(j)
Thm*
Thm* is_prime_factorization(a; b; f)
Thm*
Thm* is_prime_factorization(a; b; reduce_factorization(f; j))
a,b:, f:({a..b}), j:{a..b}.
Thm* 0<f(j)
(i:{a..b}. reduce_factorization(f; j)(i)
f(i))