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