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