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