let z be complex number ; :: thesis: (z ") *' = (z *') "
A1: ( Re z = Re (z *') & - (Im z) = Im (z *') ) by Th112;
thus Re ((z ") *') = Re (z ") by Th112
.= (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th64
.= Re ((z *') ") by A1, Th64 ; :: according to COMPLEX1:def 5 :: thesis: Im ((z ") *') = Im ((z *') ")
thus Im ((z ") *') = - (Im (z ")) by Th112
.= - ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) by Th64
.= (- (Im (z *'))) / (((Re (z *')) ^2) + ((Im (z *')) ^2)) by A1, XCMPLX_1:188
.= Im ((z *') ") by Th64 ; :: thesis: verum