let c1, c2 be complex number ; :: 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 Th104
.= c1 + c2 by FINSOP_1:12 ; :: thesis: verum