let f, g be FinSequence of REAL ; 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); ( f = g * P & len g >= 1 implies - f = (- g) * P )
assume that
A1:
f = g * P
and
A2:
len g >= 1
; - 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
hence
- f = (- g) * P
by A8, FINSEQ_1:13; verum