let F be FinSequence of COMPLEX ; :: thesis: Sum (- F) = - (Sum F)
thus Sum (- F) = addcomplex $$ (compcomplex * F) by COMPLSP1:def 9
.= compcomplex . (addcomplex $$ F) by COMPLSP1:7, COMPLSP1:8, SETWOP_2:42
.= - (Sum F) by BINOP_2:def 1 ; :: thesis: verum