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