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}. 0<g(j)
g = h
{a..b
