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

g ^ f in Permutations n

let f, g be FinSequence; :: thesis: ( f ^ g in Permutations n implies g ^ f in Permutations n )

A1: Seg (len (f ^ g)) = dom (f ^ g) by FINSEQ_1:def 3;

len (f ^ g) = (len f) + (len g) by FINSEQ_1:22

.= len (g ^ f) by FINSEQ_1:22 ;

then A2: dom (f ^ g) = dom (g ^ f) by A1, FINSEQ_1:def 3;

A3: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31

.= rng (g ^ f) by FINSEQ_1:31 ;

assume f ^ g in Permutations n ; :: thesis: g ^ f in Permutations n

then A4: f ^ g is Permutation of (Seg n) by MATRIX_1:def 12;

then A5: rng (f ^ g) = Seg n by FUNCT_2:def 3;

A6: g is one-to-one by A4, FINSEQ_3:91;

dom (f ^ g) = Seg n by A4, FUNCT_2:52;

then reconsider h = g ^ f as FinSequence-like Function of (Seg n),(Seg n) by A5, A2, A3, FUNCT_2:2;

( rng f misses rng g & f is one-to-one ) by A4, FINSEQ_3:91;

then A7: h is one-to-one by A6, FINSEQ_3:91;

h is onto by A5, A3, FUNCT_2:def 3;

hence g ^ f in Permutations n by A7, MATRIX_1:def 12; :: thesis: verum

g ^ f in Permutations n

let f, g be FinSequence; :: thesis: ( f ^ g in Permutations n implies g ^ f in Permutations n )

A1: Seg (len (f ^ g)) = dom (f ^ g) by FINSEQ_1:def 3;

len (f ^ g) = (len f) + (len g) by FINSEQ_1:22

.= len (g ^ f) by FINSEQ_1:22 ;

then A2: dom (f ^ g) = dom (g ^ f) by A1, FINSEQ_1:def 3;

A3: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31

.= rng (g ^ f) by FINSEQ_1:31 ;

assume f ^ g in Permutations n ; :: thesis: g ^ f in Permutations n

then A4: f ^ g is Permutation of (Seg n) by MATRIX_1:def 12;

then A5: rng (f ^ g) = Seg n by FUNCT_2:def 3;

A6: g is one-to-one by A4, FINSEQ_3:91;

dom (f ^ g) = Seg n by A4, FUNCT_2:52;

then reconsider h = g ^ f as FinSequence-like Function of (Seg n),(Seg n) by A5, A2, A3, FUNCT_2:2;

( rng f misses rng g & f is one-to-one ) by A4, FINSEQ_3:91;

then A7: h is one-to-one by A6, FINSEQ_3:91;

h is onto by A5, A3, FUNCT_2:def 3;

hence g ^ f in Permutations n by A7, MATRIX_1:def 12; :: thesis: verum