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