let z1, z2 be Complex; :: thesis: ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )
z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15;
hence ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) by Lm2; :: thesis: verum