set Rez = Re z;
set Imz = Im z;
( Re ((Re z) + ((- (Im z)) * <i>)) = Re z & Im ((Re z) + ((- (Im z)) * <i>)) = - (Im z) ) by COMPLEX1:12;
then A1: ( Re (z * (z *')) = ((Re z) * (Re z)) - ((Im z) * (- (Im z))) & Im (z * (z *')) = ((Re z) * (- (Im z))) + ((Re z) * (Im z)) ) by COMPLEX1:9;
A2: z * (z *') = (Re (z * (z *'))) + ((Im (z * (z *'))) * <i>) by COMPLEX1:13
.= Re (z * (z *')) by A1 ;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63;
hence not Norm z is negative by A1, A2; :: thesis: verum