let n be Nat; for f, g being FinSequence st f ^ g in Permutations n holds
f ^ (Rev g) in Permutations n
let f, g be FinSequence; ( f ^ g in Permutations n implies f ^ (Rev g) in Permutations n )
A1:
rng g = rng (Rev g)
by FINSEQ_5:57;
set h = f ^ (Rev g);
assume
f ^ g in Permutations n
; f ^ (Rev g) in Permutations n
then A2:
f ^ g is Permutation of (Seg n)
by MATRIX_1:def 12;
then A3:
g is one-to-one
by FINSEQ_3:91;
dom (f ^ g) = Seg n
by A2, FUNCT_2:52;
then A4:
Seg n = Seg ((len f) + (len g))
by FINSEQ_1:def 7;
len g = len (Rev g)
by FINSEQ_5:def 3;
then A5:
dom (f ^ (Rev g)) = Seg n
by A4, FINSEQ_1:def 7;
A6: rng (f ^ g) =
(rng f) \/ (rng g)
by FINSEQ_1:31
.=
rng (f ^ (Rev g))
by A1, FINSEQ_1:31
;
A7:
rng (f ^ g) = Seg n
by A2, FUNCT_2:def 3;
then reconsider h = f ^ (Rev g) as FinSequence-like Function of (Seg n),(Seg n) by A6, A5, FUNCT_2:2;
A8:
h is onto
by A7, A6, FUNCT_2:def 3;
( rng f misses rng g & f is one-to-one )
by A2, FINSEQ_3:91;
then
h is one-to-one
by A1, A3, FINSEQ_3:91;
hence
f ^ (Rev g) in Permutations n
by A8, MATRIX_1:def 12; verum