theorem :: RVSUM_1:18

for s being set
for F being real-valued FinSequence holds (- F) . s = - (F . s) by VALUED_1:8;