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