let f, g be real-valued FinSequence; :: thesis: for P being Permutation of (dom g) st f = g * P & len g >= 1 holds
- f = (- g) * P
let P be Permutation of (dom g); :: thesis: ( f = g * P & len g >= 1 implies - f = (- g) * P )
assume that
A1: f = g * P and
A2: len g >= 1 ; :: thesis: - f = (- g) * P
A3: rng P = dom g by FUNCT_2:def 3;
A4: dom (- g) = dom g by VALUED_1:8;
then A5: rng ((- g) * P) = rng (- g) by A3, RELAT_1:28;
A6: dom (- f) = dom (g * P) by A1, VALUED_1:8;
then A7: dom (- f) = dom P by A3, RELAT_1:27;
then A8: dom (- f) = dom ((- g) * P) by A3, A4, RELAT_1:27;
A9: dom g = Seg (len g) by FINSEQ_1:def 3;
then dom P = dom g by A2, FUNCT_2:def 1;
then (- g) * P is FinSequence by A9, A7, A8, FINSEQ_1:def 2;
then reconsider k = (- g) * P as FinSequence of REAL by A5, FINSEQ_1:def 4;
for i being Nat st i in dom (- f) holds
(- f) . i = k . i

proof

let i be Nat; :: thesis: ( i in dom (- f) implies (- f) . i = k . i )
assume A10: i in dom (- f) ; :: thesis: (- f) . i = k . i
reconsider j = P . i as Nat ;
(- f) . i = - (f . i) by RVSUM_1:17
.= - (g . (P . i)) by A1, A6, A10, FUNCT_1:12
.= (- g) . j by RVSUM_1:17
.= ((- g) * P) . i by A8, A10, FUNCT_1:12 ;
hence (- f) . i = k . i ; :: thesis: verum

end;

hence - f = (- g) * P by A8, FINSEQ_1:13; :: thesis: verum