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