theorem Th7: :: GROUP_17:7

for h, k, s, t being non zero Nat st 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 ) holds
( s = h & t = k )