let x, y be G_INTEG; :: thesis: ( x is_associated_to y implies Norm x = Norm y )
assume A1: x is_associated_to y ; :: thesis: Norm x = Norm y
reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by Th3;
A2: x1 is_associated_to y1 by A1, Th38;
x1 divides y1 by A2, GCD_1:def 3;
then consider z1 being Element of Gauss_INT_Ring such that
A3: y1 = x1 * z1 by GCD_1:def 1;
y1 divides x1 by A2, GCD_1:def 3;
then consider z2 being Element of Gauss_INT_Ring such that
A4: x1 = y1 * z2 by GCD_1:def 1;
reconsider z3 = z1 * z2 as Element of Gauss_INT_Ring ;

per cases ( x1 * y1 <> 0. Gauss_INT_Ring or x1 * y1 = 0. Gauss_INT_Ring ) ;

suppose A5: x1 * y1 <> 0. Gauss_INT_Ring ; :: thesis: Norm x = Norm y

x1 * y1 = ((x1 * z1) * y1) * z2 by A3, A4, GROUP_1:def 3
.= ((x1 * y1) * z1) * z2 by GROUP_1:def 3
.= (x1 * y1) * z3 by GROUP_1:def 3 ;
then A6: z3 = 1. Gauss_INT_Ring by A5, GCD_1:17
.= 1 ;
reconsider zz1 = z1, zz2 = z2 as G_INTEG by Th2;
reconsider zz3 = z3 as G_INTEG by Th2;
A7: Norm zz1 = 1

proof

zz3 = zz1 * zz2 by Th6;
then Norm zz3 = (Norm zz1) * (Norm zz2) by Th34;
hence Norm zz1 = 1 by A6, COMPLEX1:30, NAT_1:15; :: thesis: verum

end;

y = x * zz1 by A3, Th6;
hence Norm y = (Norm x) * (Norm zz1) by Th34
.= Norm x by A7 ;
:: thesis: verum

end;

suppose A8: x1 * y1 = 0. Gauss_INT_Ring ; :: thesis: Norm x = Norm y

A9: x1 = 0. Gauss_INT_Ring

proof

assume A10: not x1 = 0. Gauss_INT_Ring ; :: thesis: contradiction
then y1 = 0. Gauss_INT_Ring by A8, VECTSP_2:def 1;
hence contradiction by A10, A4; :: thesis: verum

end;

y1 = 0. Gauss_INT_Ring

proof

assume A11: not y1 = 0. Gauss_INT_Ring ; :: thesis: contradiction
then x1 = 0. Gauss_INT_Ring by A8, VECTSP_2:def 1;
hence contradiction by A11, A3; :: thesis: verum

end;

hence Norm x = Norm y by A9; :: thesis: verum

end;

end;