theorem Th34: :: RVSUM_2:34
for c1, c2 being Complex holds Sum <*c1,c2*> = c1 + c2