let z be Complex; :: thesis: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2)
thus |.z.| ^2 = |.(z * z).| by COMPLEX1:65
.= ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:68 ; :: thesis: verum