let z be Element of COMPLEX ; :: thesis: ( z .|. z = |.z.| ^2 & |.z.| ^2 = Re (z .|. z) )
A1: (Re z) ^2 >= 0 by XREAL_1:65;
B2: (Im z) ^2 >= 0 by XREAL_1:65;
A3: |.z.| = sqrt (((Re z) ^2 ) + ((Im z) ^2 )) by COMPLEX1:def 16;
A4: |.z.| ^2 = (|.z.| ^2 ) + (0 * <i> ) ;
thus z .|. z = ((Re z) ^2 ) + ((Im z) ^2 ) by Th43
.= |.z.| ^2 by B2, A3, SQUARE_1:def 4, A1 ; :: thesis: |.z.| ^2 = Re (z .|. z)
hence |.z.| ^2 = Re (z .|. z) by A4, COMPLEX1:28; :: thesis: verum