let z1, z2 be complex number ; :: thesis: |.(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 Lm2;
A2: (Re (z1 * z2)) ^2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) ^2 by Th24
.= ((((Re z1) * (Re z2)) ^2 ) + (((Im z1) * (Im z2)) ^2 )) + (- ((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2)))) ;
(Im (z1 * z2)) ^2 = (((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) ^2 by Th24
.= ((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) ^2 ) + (((Re z2) * (Im z1)) ^2 )) ;
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:97; :: thesis: verum