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