let a, b be R_eal; :: thesis: Sum <*a,b*> = a + b
thus Sum <*a,b*> = Sum (<*a*> ^ <*b*>) by FINSEQ_1:def 9
.= (Sum <*a*>) + b by Lm1
.= a + b by Th6 ; :: thesis: verum