let F be real-valued FinSequence; :: thesis: Sum (- F) = - (Sum F)
reconsider F1 = F as FinSequence of REAL by Lm4;
thus Sum (- F) = compreal . (addreal $$ F1) by Th22, Th23, SETWOP_2:42
.= - (Sum F1) by BINOP_2:def 7
.= - (Sum F) ; :: thesis: verum