let z1, z2 be complex number ; :: thesis: (z1 * z2) *' = (z1 *' ) * (z2 *' )
A1: ( Re (z1 *' ) = Re z1 & Re (z2 *' ) = Re z2 ) by Th112;
A2: ( Im (z1 *' ) = - (Im z1) & Im (z2 *' ) = - (Im z2) ) by Th112;
thus Re ((z1 * z2) *' ) = Re (z1 * z2) by Th112
.= ((Re (z1 *' )) * (Re (z2 *' ))) - ((- (Im (z1 *' ))) * (- (Im (z2 *' )))) by A1, A2, Th24
.= ((Re (z1 *' )) * (Re (z2 *' ))) - (- (- ((Im (z1 *' )) * (Im (z2 *' )))))
.= Re ((z1 *' ) * (z2 *' )) by Th24 ; :: according to COMPLEX1:def 5 :: thesis: Im ((z1 * z2) *' ) = Im ((z1 *' ) * (z2 *' ))
thus Im ((z1 * z2) *' ) = - (Im (z1 * z2)) by Th112
.= - (((Re (z1 *' )) * (- (Im (z2 *' )))) + ((Re (z2 *' )) * (- (Im (z1 *' ))))) by A1, A2, Th24
.= ((Re (z2 *' )) * (Im (z1 *' ))) + (- (- ((Re (z1 *' )) * (Im (z2 *' )))))
.= Im ((z1 *' ) * (z2 *' )) by Th24 ; :: thesis: verum