let z be Complex; :: thesis: (z ") *' = (z *') "
A1: ( Re z = Re (z *') & - (Im z) = Im (z *') ) by Th27;
thus Re ((z ") *') = Re (z ") by Th27
.= (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20
.= (Re (z *')) / (((Re (z *')) ^2) + ((Im (z *')) ^2)) by A1
.= Re ((z *') ") by Th20 ; :: according to COMPLEX1:def 3 :: thesis: Im ((z ") *') = Im ((z *') ")
thus Im ((z ") *') = - (Im (z ")) by Th27
.= - ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) by Th20
.= (- (Im (z *'))) / (((Re (z *')) ^2) + ((Im (z *')) ^2)) by A1, XCMPLX_1:187
.= Im ((z *') ") by Th20 ; :: thesis: verum