let r1, r2 be Real; :: 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 Th74
.= r1 + r2 by FINSOP_1:11 ; :: thesis: verum