let c be complex number ; :: thesis: Sum <*c*> = c
reconsider c = c as Element of COMPLEX by XCMPLX_0:def 2;
Sum <*c*> = c by FINSOP_1:12;
hence Sum <*c*> = c ; :: thesis: verum