let z1, z2 be Complex; :: thesis: |[(Re (z1 + z2)),(Im (z1 + z2))]| = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]|
|[(Re (z1 + z2)),(Im (z1 + z2))]| `2 = Im (z1 + z2) by EUCLID:52;
then A1: |[(Re (z1 + z2)),(Im (z1 + z2))]| `2 = (Im z1) + (Im z2) by COMPLEX1:8;
|[(Re (z1 + z2)),(Im (z1 + z2))]| `1 = Re (z1 + z2) by EUCLID:52;
then |[(Re (z1 + z2)),(Im (z1 + z2))]| `1 = (Re z1) + (Re z2) by COMPLEX1:8;
hence |[(Re (z1 + z2)),(Im (z1 + z2))]| = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]| by A1, EUCLID:53; :: thesis: verum