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