let c be Complex; :: thesis: Sum <%c%> = c
c in COMPLEX by XCMPLX_0:def 2;
hence Sum <%c%> = c by Th37; :: thesis: verum