let z be Complex; :: thesis: ( z .|. z = |.z.| ^2 & |.z.| ^2 = Re (z .|. z) )
A1: ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63;
A2: |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2)) by COMPLEX1:def 12;
thus A3: z .|. z = ((Re z) ^2) + ((Im z) ^2) by Th28
.= |.z.| ^2 by A1, A2, SQUARE_1:def 2 ; :: thesis: |.z.| ^2 = Re (z .|. z)
|.z.| ^2 = (|.z.| ^2) + (0 * <i>) ;
hence |.z.| ^2 = Re (z .|. z) by A3, COMPLEX1:12; :: thesis: verum