let r1, r2, r3, r4 be real number ; :: thesis: Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4
thus Sum <*r1,r2,r3,r4*> = (Sum <*r1,r2,r3*>) + r4 by Th104
.= ((r1 + r2) + r3) + r4 by Th108 ; :: thesis: verum