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