let n be Nat; :: thesis: for f, g being FinSequence st f ^ g in Permutations n holds

f ^ (Rev g) in Permutations n

let f, g be FinSequence; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

f ^ (Rev g) in Permutations n

let f, g be FinSequence; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum