let r1, r2, r3 be Real; :: thesis: Sum <*r1,r2,r3*> = (r1 + r2) + r3
thus Sum <*r1,r2,r3*> = (Sum <*r1,r2*>) + r3 by Th74
.= (r1 + r2) + r3 by Th77 ; :: thesis: verum