let z be complex number ; :: thesis: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2)
thus |.z.| ^2 = |.(z * z).| by COMPLEX1:151
.= ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:154 ; :: thesis: verum