let F be complex-valued FinSequence; :: thesis: Sum (- F) = - (Sum F)
reconsider F1 = F as FinSequence of COMPLEX by Lm2;
thus Sum (- F) = compcomplex . (addcomplex $$ F1) by SEQ_4:51, SEQ_4:52, SETWOP_2:31
.= - (Sum F1) by BINOP_2:def 1
.= - (Sum F) ; :: thesis: verum