let z be complex number ; :: thesis: ( Re (- z) = - (Re z) & Im (- z) = - (Im z) )
z in COMPLEX by XCMPLX_0:def 2;
then - z = (- (Re z)) + ((- (Im z)) * <i> ) by Def11;
hence ( Re (- z) = - (Re z) & Im (- z) = - (Im z) ) by Th28; :: thesis: verum