theorem :: COMPLEX1:83

for z being Complex holds - z = (- (Re z)) + ((- (Im z)) * <i>) by Lm22;