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