theorem Th15: :: NAT_5:15

for n, m, n1, n2, m1, m2 being Nat st n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_coprime & n1 * m1 = n2 * m2 holds
( n1 = n2 & m1 = m2 )