let z be complex number ; :: thesis: (- z) *' = - (z *')
thus Re ((- z) *') = Re (- z) by Th112
.= - (Re z) by Th34
.= - (Re (z *')) by Th112
.= Re (- (z *')) by Th34 ; :: according to COMPLEX1:def 3 :: thesis: Im ((- z) *') = Im (- (z *'))
thus Im ((- z) *') = - (Im (- z)) by Th112
.= - (- (Im z)) by Th34
.= - (Im (z *')) by Th112
.= Im (- (z *')) by Th34 ; :: thesis: verum