let z be Complex; :: thesis: - z = (- (Re z)) + ((- (Im z)) * <i>)
reconsider zz = 0 as Element of REAL by XREAL_0:def 1;
set z9 = [*(- (Re z)),(- (Im z))*];
[*(- (Re z)),(- (Im z))*] + z = [*((Re [*(- (Re z)),(- (Im z))*]) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm15
.= [*((- (Re z)) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm2
.= [*zz,((- (Im z)) + (Im z))*] by Lm2
.= 0 by ARYTM_0:def 5 ;
hence - z = (- (Re z)) + ((- (Im z)) * <i>) by Lm21; :: thesis: verum