let f, g be complex-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:def 7;
then A5: rng ((g ") * P) = rng (g ") by A3, RELAT_1:28;
A6: dom (f ") = dom (g * P) by A1, VALUED_1:def 7;
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 A7, A8, A9, FINSEQ_1:def 2;
then reconsider k = (g ") * P as FinSequence of COMPLEX 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 VALUED_1:10
.= (g . (P . i)) " by A1, A6, A10, FUNCT_1:12
.= (g ") . j by VALUED_1:10
.= ((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