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 Lm4
.= a + b by Th5 ; :: thesis: verum