theorem Th24: :: RFINSEQ2:26

for f, g being real-valued FinSequence
for P being Permutation of (dom g) st f = g * P & len g >= 1 holds
- f = (- g) * P