let c1, c2 be Complex; :: thesis: Sum <*c1,c2*> = c1 + c2
reconsider s1 = c1 as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum <*c1,c2*> = (Sum <*s1*>) + c2 by Th31
.= c1 + c2 by FINSOP_1:11 ; :: thesis: verum