let z be Element of COMPLEX ; :: 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 5 :: 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