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 holds
not q,h are_coprime ) & ( for q being Prime st q in support 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 & q,h are_coprime ) or ex q being Prime st
( q in support & q,k are_coprime ) or ( s = h & t = k ) )

assume A2: s * t = h * k ; :: thesis: ( ex q being Prime st
( q in support & q,h are_coprime ) or ex q being Prime st
( q in support & q,k are_coprime ) or ( s = h & t = k ) )

assume A3: for q being Prime st q in support holds
not q,h are_coprime ; :: thesis: ( ex q being Prime st
( q in support & q,k are_coprime ) or ( s = h & t = k ) )

assume A4: for q being Prime st q in support 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 c= support by ;
A6: support c= support by ;
support () misses support () by ;
then support misses support () by NAT_3:def 9;
then A7: support misses support by NAT_3:def 9;
set f = + ;
set g = + ;
A8: (prime_factorization s) + is prime-factorization-like by ;
A9: (prime_factorization h) + is prime-factorization-like by ;
A10: Product () = () * () by
.= h * () by NAT_3:61
.= h * k by NAT_3:61 ;
A11: Product () = () * () by
.= s * () by NAT_3:61
.= s * t by NAT_3:61 ;
() \/ () = support () by PRE_POLY:38
.= support () by A11, INT_7:15, A8, A9, A10, A2
.= () \/ () by PRE_POLY:38 ;
then A12: ( support = support & support = support ) by A5, A6, A7, Th1;
A13: support = support () by ;
A14: support = support () by ;
A15: for p being Nat st p in support () holds
. p = p |^ (p |-count h)
proof
let p be Nat; :: thesis: ( p in support () implies . p = p |^ (p |-count h) )
assume A16: p in support () ; :: thesis: . p = p |^ (p |-count h)
then A17: p in support by NAT_3:def 9;
A18: p in support by ;
thus . p = () . p by
.= . p by Th3, A17, A7, INT_7:15, A8, A9, A10, A2, A11
.= p |^ (p |-count h) by ; :: thesis: verum
end;
A19: for p being Nat st p in support () holds
. p = p |^ (p |-count k)
proof
let p be Nat; :: thesis: ( p in support () implies . p = p |^ (p |-count k) )
assume A20: p in support () ; :: thesis: . p = p |^ (p |-count k)
then A21: p in support by NAT_3:def 9;
A22: p in support by ;
thus . p = () . p by
.= . p by Th4, A21, A7, A11, INT_7:15, A8, A9, A10, A2
.= p |^ (p |-count k) by ; :: thesis: verum
end;
thus s = Product by NAT_3:61
.= Product by
.= h by NAT_3:61 ; :: thesis: t = k
thus t = Product by NAT_3:61
.= Product by
.= k by NAT_3:61 ; :: thesis: verum