let z be Complex; :: thesis: |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]|
|[(Re (- z)),(Im (- z))]| `2 = Im (- z) by EUCLID:52;
then A1: |[(Re (- z)),(Im (- z))]| `2 = - (Im z) by COMPLEX1:17;
|[(Re (- z)),(Im (- z))]| `1 = Re (- z) by EUCLID:52;
then |[(Re (- z)),(Im (- z))]| `1 = - (Re z) by COMPLEX1:17;
hence |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]| by A1, EUCLID:53; :: thesis: verum