let z be Element of COMPLEX ; :: thesis: z * (z *' ) = (|.z.| ^2 ) + (0 * <i> )
( 0 <= (Re z) ^2 & 0 <= (Im z) ^2 ) by XREAL_1:65;
then 0 + 0 <= ((Re z) ^2 ) + ((Im z) ^2 ) ;
then ((Re z) ^2 ) + ((Im z) ^2 ) = |.z.| ^2 by SQUARE_1:def 4;
then ( Re (z * (z *' )) = |.z.| ^2 & Im (z * (z *' )) = 0 ) by COMPLEX1:126;
hence z * (z *' ) = (|.z.| ^2 ) + (0 * <i> ) by COMPLEX1:29; :: thesis: verum