theorem :: RVSUM_2:35
for c1, c2, c3 being Complex holds Sum <*c1,c2,c3*> = (c1 + c2) + c3