let cF1, cF2 be complex-valued XFinSequence; :: thesis: Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2)
A1: ( cF1 is COMPLEX -valued & cF2 is COMPLEX -valued ) by Lm2;
thus Sum (cF1 ^ cF2) = addcomplex . ((Sum cF1),(Sum cF2)) by Th41, A1
.= (Sum cF1) + (Sum cF2) by BINOP_2:def 3 ; :: thesis: verum