let z be Element of COMPLEX ; :: 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