2. b :
3. k :
4.
k1:.
4. k1<k
4.
4. (
g,h:({a..b
}
).
4. (is_prime_factorization(a; b; g) & is_prime_factorization(a; b; h)
4. (
4. (
{a..b}(g) = k1 {a..b}(g) = {a..b}(h) g = h)
5. g : {a..b
}
6. h : {a..b
}
7. is_prime_factorization(a; b; g)
8. is_prime_factorization(a; b; h)
9.
{a..b}(g) = k
10.
{a..b}(g) = {a..b}(h)
11. j : {a..b
}
12. 0<g(j)
13. prime(j)
14. j |
{a..b}(g)
15. j |
{a..b}(h)
16. 0<h(j)
17.
{a..b}(reduce_factorization(g; j))
17. =
17.
{a..b}(reduce_factorization(h; j))
reduce_factorization(g; j) = reduce_factorization(h; j)
