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 ((Re z) ^2 ) + ((Im z) ^2 ) = |.z.| ^2 by SQUARE_1:def 4;
then A1: Re (z * (z *' )) = |.z.| ^2 by COMPLEX1:126;
Im (z * (z *' )) = 0 by COMPLEX1:126;
hence z * (z *' ) = (|.z.| ^2 ) + (0 * <i> ) by A1, COMPLEX1:29; :: thesis: verum