let F1, F2 be real-valued FinSequence; :: thesis: Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
thus Sum (F1 ^ F2) = Sum (F3 ^ F4)
.= addreal . ((addreal $$ F3),(addreal $$ F4)) by FINSOP_1:5
.= (Sum F3) + (Sum F4) by BINOP_2:def 9
.= (Sum F1) + (Sum F2) ; :: thesis: verum