let z be Complex; :: thesis: |.(z * z).| = ((Re z) ^2) + ((Im z) ^2)
( 0 <= ((Re z) ^2) + ((Im z) ^2) & |.(z * z).| = |.z.| * |.z.| ) by Lm1, Th65;
then |.(z * z).| = sqrt ((((Re z) ^2) + ((Im z) ^2)) ^2) by SQUARE_1:29;
hence |.(z * z).| = ((Re z) ^2) + ((Im z) ^2) by Lm1, SQUARE_1:22; :: thesis: verum