let z be Element of F_Complex; :: thesis: z * (z *') = |.z.| ^2
reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;
thus z * (z *') = (|.a.| ^2) + (0 * <i>) by Th4
.= |.z.| ^2 ; :: thesis: verum