let z1, z2 be Complex; :: thesis: z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>)
z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15;
hence z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>) by Lm21; :: thesis: verum