theorem Th78: :: RVSUM_1:78

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