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 )
assume f ^ g in Permutations n ; :: thesis: g ^ f in Permutations n
then A1: f ^ g is Permutation of (Seg n) by MATRIX_2:def 11;
then A2: ( f ^ g is Function of (Seg n),(Seg n) & rng (f ^ g) = Seg n ) by FUNCT_2:def 3;
A3: dom (f ^ g) = Seg n by A1, FUNCT_2:67;
A4: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35
.= len (g ^ f) by FINSEQ_1:35 ;
Seg (len (f ^ g)) = dom (f ^ g) by FINSEQ_1:def 3;
then A5: dom (f ^ g) = dom (g ^ f) by A4, FINSEQ_1:def 3;
A6: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:44
.= rng (g ^ f) by FINSEQ_1:44 ;
A7: ( rng f misses rng g & f is one-to-one & g is one-to-one ) by A1, FINSEQ_3:98;
reconsider h = g ^ f as FinSequence-like Function of (Seg n),(Seg n) by A2, A3, A5, A6, FUNCT_2:4;
A8: h is onto by A2, A6, FUNCT_2:def 3;
h is one-to-one by A7, FINSEQ_3:98;
then h is bijective by A8;
hence g ^ f in Permutations n by MATRIX_2:def 11; :: thesis: verum