let z be complex number ; :: 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 Th24
.= ((Re z) * (Re z)) - ((Im z) * (Im (z *' ))) by Th112
.= ((Re z) * (Re z)) - ((Im z) * (- (Im z))) by Th112
.= ((Re z) ^2 ) + ((Im z) ^2 ) ; :: thesis: Im (z * (z *' )) = 0
thus Im (z * (z *' )) = ((Re z) * (Im (z *' ))) + ((Re (z *' )) * (Im z)) by Th24
.= ((Re z) * (- (Im z))) + ((Re (z *' )) * (Im z)) by Th112
.= (- ((Re z) * (Im z))) + ((Re z) * (Im z)) by Th112
.= 0 ; :: thesis: verum