let z be Element of COMPLEX ; :: thesis: z * (z *') = (|.z.| ^2) + (0 * <i>)
( 0 <= (Re z) ^2 & 0 <= (Im z) ^2 ) by XREAL_1:63;
then ((Re z) ^2) + ((Im z) ^2) = |.z.| ^2 by SQUARE_1:def 2;
then A1: Re (z * (z *')) = |.z.| ^2 by COMPLEX1:40;
Im (z * (z *')) = 0 by COMPLEX1:40;
hence z * (z *') = (|.z.| ^2) + (0 * <i>) by A1, COMPLEX1:13; :: thesis: verum