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 3 :: 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