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