let z1, z2 be Complex; :: thesis: (z1 + z2) *' = (z1 *') + (z2 *')
thus Re ((z1 + z2) *') = Re (z1 + z2) by Th27
.= (Re z1) + (Re z2) by Th8
.= (Re (z1 *')) + (Re z2) by Th27
.= (Re (z1 *')) + (Re (z2 *')) by Th27
.= Re ((z1 *') + (z2 *')) by Th8 ; :: according to COMPLEX1:def 3 :: thesis: Im ((z1 + z2) *') = Im ((z1 *') + (z2 *'))
thus Im ((z1 + z2) *') = - (Im (z1 + z2)) by Th27
.= - ((Im z1) + (- (- (Im z2)))) by Th8
.= (- (Im z1)) + (- (Im z2))
.= (Im (z1 *')) + (- (Im z2)) by Th27
.= (Im (z1 *')) + (Im (z2 *')) by Th27
.= Im ((z1 *') + (z2 *')) by Th8 ; :: thesis: verum