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