let f, g be FinSequence of REAL ; :: 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 A1: ( f = g * P & len g >= 1 ) ; :: thesis: - f = (- g) * P
A2: rng P = dom g by FUNCT_2:def 3;
A3: dom g = Seg (len g) by FINSEQ_1:def 3;
then 1 in dom g by A1, FINSEQ_1:3;
then A4: dom P = dom g by FUNCT_2:def 1;
A5: dom (- g) = dom g by VALUED_1:8;
A6: dom (- f) = dom (g * P) by A1, VALUED_1:8;
then A7: dom (- f) = dom P by A2, RELAT_1:46;
then A8: dom (- f) = dom ((- g) * P) by A2, A5, RELAT_1:46;
A9: rng ((- g) * P) = rng (- g) by A2, A5, RELAT_1:47;
(- g) * P is FinSequence by A3, A4, A7, A8, FINSEQ_1:def 2;
then reconsider k = (- g) * P as FinSequence of REAL by A9, 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
then P . i in rng P by A7, FUNCT_1:12;
then reconsider j = P . i as Element of NAT by A2;
(- f) . i = - (f . i) by RVSUM_1:35
.= - (g . (P . i)) by A1, A6, A10, FUNCT_1:22
.= (- g) . j by RVSUM_1:35
.= ((- g) * P) . i by A8, A10, FUNCT_1:22 ;
hence (- f) . i = k . i ; :: thesis: verum

end;

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