theorem :: AFINSQ_2:53

for c being Complex holds Sum <%c%> = c