let r1, r2 be real number ; :: thesis: Sum <*r1,r2*> = r1 + r2
reconsider s1 = r1 as Element of REAL by XREAL_0:def 1;
thus Sum <*r1,r2*> = (Sum <*s1*>) + r2 by Th104
.= r1 + r2 by FINSOP_1:12 ; :: thesis: verum