let z1, z2 be Complex; :: thesis: z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]
set z = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*];
reconsider z9 = z1 + z2 as Element of COMPLEX by XCMPLX_0:def 2;
A1: Im [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] = (Im z1) + (Im z2) by Lm2
.= Im z9 by Lm12 ;
Re [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] = (Re z1) + (Re z2) by Lm2
.= Re z9 by Lm11 ;
hence z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by A1; :: thesis: verum