let z be complex number ; :: thesis: |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]|
|[(Re (- z)),(Im (- z))]| `2 = Im (- z) by EUCLID:56;
then A1: |[(Re (- z)),(Im (- z))]| `2 = - (Im z) by COMPLEX1:34;
|[(Re (- z)),(Im (- z))]| `1 = Re (- z) by EUCLID:56;
then |[(Re (- z)),(Im (- z))]| `1 = - (Re z) by COMPLEX1:34;
hence |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]| by A1, EUCLID:57; :: thesis: verum