let z1, z2 be Complex; |.(z1 * z2).| = |.z1.| * |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A1:
( 0 <= ((Re z1) ^2) + ((Im z1) ^2) & 0 <= ((Re z2) ^2) + ((Im z2) ^2) )
by Lm1;
A2: (Im (z1 * z2)) ^2 =
(((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) ^2
by Th9
.=
((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) ^2) + (((Re z2) * (Im z1)) ^2))
;
(Re (z1 * z2)) ^2 =
(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) ^2
by Th9
.=
((((Re z1) * (Re z2)) ^2) + (((Im z1) * (Im z2)) ^2)) + (- ((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2))))
;
then
((Re (z1 * z2)) ^2) + ((Im (z1 * z2)) ^2) = (((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))
by A2;
hence
|.(z1 * z2).| = |.z1.| * |.z2.|
by A1, SQUARE_1:29; verum