let n, m, n1, n2, m1, m2 be Nat; :: thesis: ( n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_coprime & n1 * m1 = n2 * m2 implies ( n1 = n2 & m1 = m2 ) )
assume A1: n1 in NatDivisors n ; :: thesis: ( not m1 in NatDivisors m or not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
then A2: n1 divides n by MOEBIUS1:39;
assume A3: m1 in NatDivisors m ; :: thesis: ( not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
then A4: m1 divides m by MOEBIUS1:39;
assume A5: n2 in NatDivisors n ; :: thesis: ( not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
then A6: n2 divides n by MOEBIUS1:39;
assume A7: m2 in NatDivisors m ; :: thesis: ( not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
assume A8: n,m are_coprime ; :: thesis: ( not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
assume A9: n1 * m1 = n2 * m2 ; :: thesis: ( n1 = n2 & m1 = m2 )
A10: m2 divides m by A7, MOEBIUS1:39;

A11: now :: thesis: not n1 <> n2

reconsider m19 = m1, m29 = m2 as non zero Nat by A3, A7, MOEBIUS1:39;
A12: n gcd m > 0 by A8, INT_2:def 3;
reconsider n19 = n1, n29 = n2 as non zero Nat by A1, A5, MOEBIUS1:39;
assume n1 <> n2 ; :: thesis: contradiction
then consider p being Element of NAT such that
A13: p is prime and
A14: p |-count n19 <> p |-count n29 by NAT_4:21;
reconsider p = p as Prime by A13;
(p |-count n19) + (p |-count m19) = p |-count (n19 * m19) by NAT_3:28
.= (p |-count n29) + (p |-count m29) by A9, NAT_3:28 ;
then ( p |-count m19 <> 0 or p |-count m29 <> 0 ) by A14;
then ( p divides m19 or p divides m29 ) by MOEBIUS1:6;
then A15: p divides m by A4, A10, INT_2:9;
( p |-count n19 <> 0 or p |-count n29 <> 0 ) by A14;
then ( p divides n19 or p divides n29 ) by MOEBIUS1:6;
then p divides n by A2, A6, INT_2:9;
then p divides n gcd m by A15, INT_2:def 2;
then A16: p <= n gcd m by A12, INT_2:27;
p > 1 by INT_2:def 4;
hence contradiction by A8, A16, INT_2:def 3; :: thesis: verum

end;

A17: 0 < n2 by A5, MOEBIUS1:39;
assume ( not n1 = n2 or not m1 = m2 ) ; :: thesis: contradiction
hence contradiction by A17, A9, A11, XCMPLX_1:5; :: thesis: verum