let h, k, s, t be non zero Nat; :: thesis: ( h,k are_coprime & s * t = h * k & ( for q being Prime st q in support (prime_factorization s) holds
not q,h are_coprime ) & ( for q being Prime st q in support (prime_factorization t) holds
not q,k are_coprime ) implies ( s = h & t = k ) )
assume A1: h,k are_coprime ; :: thesis: ( not s * t = h * k or ex q being Prime st
( q in support (prime_factorization s) & q,h are_coprime ) or ex q being Prime st
( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )
assume A2: s * t = h * k ; :: thesis: ( ex q being Prime st
( q in support (prime_factorization s) & q,h are_coprime ) or ex q being Prime st
( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )
assume A3: for q being Prime st q in support (prime_factorization s) holds
not q,h are_coprime ; :: thesis: ( ex q being Prime st
( q in support (prime_factorization t) & q,k are_coprime ) or ( s = h & t = k ) )
assume A4: for q being Prime st q in support (prime_factorization t) holds
not q,k are_coprime ; :: thesis: ( s = h & t = k )
set ps = prime_factorization s;
set ph = prime_factorization h;
set pt = prime_factorization t;
set pk = prime_factorization k;
A5: support (prime_factorization s) c= support (prime_factorization h) by A3, Th6;
A6: support (prime_factorization t) c= support (prime_factorization k) by A4, Th6;
support (pfexp h) misses support (pfexp k) by NAT_3:44, A1;
then support (prime_factorization h) misses support (pfexp k) by NAT_3:def 9;
then A7: support (prime_factorization h) misses support (prime_factorization k) by NAT_3:def 9;
set f = (prime_factorization s) + (prime_factorization t);
set g = (prime_factorization h) + (prime_factorization k);
A8: (prime_factorization s) + (prime_factorization t) is prime-factorization-like by A7, A5, A6, XBOOLE_1:64, Lm1;
A9: (prime_factorization h) + (prime_factorization k) is prime-factorization-like by A7, Lm1;
A10: Product ((prime_factorization h) + (prime_factorization k)) = (Product (prime_factorization h)) * (Product (prime_factorization k)) by A7, NAT_3:19
.= h * (Product (prime_factorization k)) by NAT_3:61
.= h * k by NAT_3:61 ;
A11: Product ((prime_factorization s) + (prime_factorization t)) = (Product (prime_factorization s)) * (Product (prime_factorization t)) by A5, A6, XBOOLE_1:64, A7, NAT_3:19
.= s * (Product (prime_factorization t)) by NAT_3:61
.= s * t by NAT_3:61 ;
(support (prime_factorization s)) \/ (support (prime_factorization t)) = support ((prime_factorization s) + (prime_factorization t)) by PRE_POLY:38
.= support ((prime_factorization h) + (prime_factorization k)) by A11, INT_7:15, A8, A9, A10, A2
.= (support (prime_factorization h)) \/ (support (prime_factorization k)) by PRE_POLY:38 ;
then A12: ( support (prime_factorization s) = support (prime_factorization h) & support (prime_factorization t) = support (prime_factorization k) ) by A5, A6, A7, Th1;
A13: support (prime_factorization s) = support (pfexp h) by A12, NAT_3:def 9;
A14: support (prime_factorization t) = support (pfexp k) by A12, NAT_3:def 9;
A15: for p being Nat st p in support (pfexp h) holds
(prime_factorization s) . p = p |^ (p |-count h)

proof

let p be Nat; :: thesis: ( p in support (pfexp h) implies (prime_factorization s) . p = p |^ (p |-count h) )
assume A16: p in support (pfexp h) ; :: thesis: (prime_factorization s) . p = p |^ (p |-count h)
then A17: p in support (prime_factorization h) by NAT_3:def 9;
A18: p in support (prime_factorization s) by A16, A12, NAT_3:def 9;
thus (prime_factorization s) . p = ((prime_factorization s) + (prime_factorization t)) . p by Th3, A18, A5, A6, XBOOLE_1:64, A7
.= (prime_factorization h) . p by Th3, A17, A7, INT_7:15, A8, A9, A10, A2, A11
.= p |^ (p |-count h) by A16, NAT_3:def 9 ; :: thesis: verum

end;

A19: for p being Nat st p in support (pfexp k) holds
(prime_factorization t) . p = p |^ (p |-count k)

proof

let p be Nat; :: thesis: ( p in support (pfexp k) implies (prime_factorization t) . p = p |^ (p |-count k) )
assume A20: p in support (pfexp k) ; :: thesis: (prime_factorization t) . p = p |^ (p |-count k)
then A21: p in support (prime_factorization k) by NAT_3:def 9;
A22: p in support (prime_factorization t) by A12, A20, NAT_3:def 9;
thus (prime_factorization t) . p = ((prime_factorization s) + (prime_factorization t)) . p by Th4, A22, A5, A6, XBOOLE_1:64, A7
.= (prime_factorization k) . p by Th4, A21, A7, A11, INT_7:15, A8, A9, A10, A2
.= p |^ (p |-count k) by A20, NAT_3:def 9 ; :: thesis: verum

end;

thus s = Product (prime_factorization s) by NAT_3:61
.= Product (prime_factorization h) by A15, A13, NAT_3:def 9
.= h by NAT_3:61 ; :: thesis: t = k
thus t = Product (prime_factorization t) by NAT_3:61
.= Product (prime_factorization k) by A19, A14, NAT_3:def 9
.= k by NAT_3:61 ; :: thesis: verum