let z be complex number ; :: thesis: |.(z * z).| = ((Re z) ^2 ) + ((Im z) ^2 )
A1: 0 <= ((Re z) ^2 ) + ((Im z) ^2 ) by Lm2;
( |.(z * z).| = |.z.| * |.z.| & |.z.| = sqrt (((Re z) ^2 ) + ((Im z) ^2 )) ) by Th151;
then |.(z * z).| = sqrt ((((Re z) ^2 ) + ((Im z) ^2 )) ^2 ) by A1, SQUARE_1:97;
hence |.(z * z).| = ((Re z) ^2 ) + ((Im z) ^2 ) by Lm2, SQUARE_1:89; :: thesis: verum