theorem :: RVSUM_1:54

for F being real-valued FinSequence holds (- 1) * F = - F ;