theorem Th77: :: RVSUM_1:77

for r1, r2 being Real holds Sum <*r1,r2*> = r1 + r2