let z be Complex; :: thesis: (- z) *' = - (z *')
thus Re ((- z) *') = Re (- z) by Th27
.= - (Re z) by Th17
.= - (Re (z *')) by Th27
.= Re (- (z *')) by Th17 ; :: according to COMPLEX1:def 3 :: thesis: Im ((- z) *') = Im (- (z *'))
thus Im ((- z) *') = - (Im (- z)) by Th27
.= - (- (Im z)) by Th17
.= - (Im (z *')) by Th27
.= Im (- (z *')) by Th17 ; :: thesis: verum