theorem :: RVSUM_2:30

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