let F1, F2 be FinSequence of COMPLEX ; :: thesis: Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
thus Sum (F1 ^ F2) = addcomplex . ((addcomplex $$ F1),(addcomplex $$ F2)) by FINSOP_1:5
.= (Sum F1) + (Sum F2) by BINOP_2:def 3 ; :: thesis: verum