let z be Complex; :: thesis: ( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 )
thus Re (z * (z *')) = ((Re z) * (Re (z *'))) - ((Im z) * (Im (z *'))) by Th9
.= ((Re z) * (Re z)) - ((Im z) * (Im (z *'))) by Th27
.= ((Re z) * (Re z)) - ((Im z) * (- (Im z))) by Th27
.= ((Re z) ^2) + ((Im z) ^2) ; :: thesis: Im (z * (z *')) = 0
thus Im (z * (z *')) = ((Re z) * (Im (z *'))) + ((Re (z *')) * (Im z)) by Th9
.= ((Re z) * (- (Im z))) + ((Re (z *')) * (Im z)) by Th27
.= (- ((Re z) * (Im z))) + ((Re z) * (Im z)) by Th27
.= 0 ; :: thesis: verum