let n be Nat; :: thesis:
defpred S₁[ Nat] means for perm being Element of Permutations $1 ex P being FinSequence of (Group_of_Perm $1) st
( perm = Product P & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations $1 st
( P . i = trans & trans is being_transposition ) ) );
let perm be Element of Permutations n; :: thesis:
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A2: S₁[k] ; :: thesis:
set k1 = k + 1;
let p be Element of Permutations (k + 1); :: thesis:
reconsider p9 = p as Permutation of (Seg (k + 1)) by MATRIX_1:def 12;
set Gk1 = Group_of_Perm (k + 1);
A3: for p being Element of Permutations (k + 1) st p . (k + 1) = k + 1 holds
ex P being FinSequence of (Group_of_Perm (k + 1)) st
( p = Product P & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (k + 1) st
( P . i = trans & trans is being_transposition ) ) )

proof

set Ik = idseq k;
set Ik1 = idseq (k + 1);
set Gk1 = Group_of_Perm (k + 1);
set Gk = Group_of_Perm k;
let p be Element of Permutations (k + 1); :: thesis:
assume A4: p . (k + 1) = k + 1 ; :: thesis:
set mG1 = the multF of (Group_of_Perm (k + 1));
set mG = the multF of (Group_of_Perm k);
reconsider p9 = p as Permutation of (Seg (k + 1)) by MATRIX_1:def 12;
A5: Seg (k + 1) = (Seg k) \/ {(k + 1)} by FINSEQ_1:9;
then consider pk being Permutation of (Seg k) such that
A6: p9 | (Seg k) = pk by A4, Th18, FINSEQ_3:8;
reconsider pk9 = pk as Element of Permutations k by MATRIX_1:def 12;
consider P being FinSequence of (Group_of_Perm k) such that
A7: pk9 = Product P and
A8: for i being Nat st i in dom P holds
ex trans being Element of Permutations k st
( P . i = trans & trans is being_transposition ) by A2;
A9: pk9 = the multF of (Group_of_Perm k) "**" P by A7, GROUP_4:def 2;
defpred S₂[ set , set ] means for i being Nat
for tr being Element of Permutations k st i in dom P & P . i = tr & i = $1 holds
ex newtr being Element of Permutations (k + 1) st
( newtr = $2 & newtr is being_transposition & newtr . (k + 1) = k + 1 & tr = newtr | (Seg k) );
A10: not k + 1 in Seg k by FINSEQ_3:8;
A11: for m being Nat st m in Seg (len P) holds
ex x being Element of (Group_of_Perm (k + 1)) st S₂[m,x]

proof

let m be Nat; :: thesis:
assume m in Seg (len P) ; :: thesis:
then m in dom P by FINSEQ_1:def 3;
then consider tr being Element of Permutations k such that
A12: P . m = tr and
A13: tr is being_transposition by A8;
consider i9, j9 being Nat such that
A14: i9 in dom tr and
A15: j9 in dom tr and
A16: i9 <> j9 and
A17: tr . i9 = j9 and
A18: tr . j9 = i9 and
A19: for k being Nat st k <> i9 & k <> j9 & k in dom tr holds
tr . k = k by A13;
reconsider tr9 = tr as Permutation of (Seg k) by MATRIX_1:def 12;
consider newt being Function of (Seg (k + 1)),(Seg (k + 1)) such that
A20: newt | (Seg k) = tr9 and
A21: newt . (k + 1) = k + 1 by A5, A10, STIRL2_1:57;
A22: newt . j9 = tr . j9 by A20, A15, FUNCT_1:47;
A23: ( Seg k is empty implies Seg k is empty ) ;
then A24: newt is onto by A5, A20, A21, STIRL2_1:58;
newt is one-to-one by A5, A10, A23, A20, A21, STIRL2_1:58;
then reconsider NT = newt as Element of Permutations (k + 1) by A24, MATRIX_1:def 12;
reconsider NT9 = NT as Element of (Group_of_Perm (k + 1)) by MATRIX_1:def 13;
take NT9 ; :: thesis:
let I be Nat; :: thesis:
let TR be Element of Permutations k; :: thesis:
assume that
I in dom P and
A25: P . I = TR and
A26: I = m ; :: thesis:
take NT ; :: thesis:
A27: dom tr c= dom newt by A20, RELAT_1:60;
A28: for m being Nat st m <> i9 & m <> j9 & m in dom newt holds
newt . m = m

proof

A29: dom tr9 = Seg k by FUNCT_2:52;
let m be Nat; :: thesis:
assume that
A30: m <> i9 and
A31: m <> j9 and
A32: m in dom newt ; :: thesis:
dom newt = Seg (k + 1) by FUNCT_2:52;
then ( m in Seg k or m in {(k + 1)} ) by A5, A32, XBOOLE_0:def 3;
then ( m in dom tr or m = k + 1 ) by A29, TARSKI:def 1;
then ( ( tr . m = newt . m & tr . m = m ) or newt . m = m ) by A20, A21, A19, A30, A31, FUNCT_1:47;
hence newt . m = m ; :: thesis:

end;

newt . i9 = tr . i9 by A20, A14, FUNCT_1:47;
hence ( NT = NT9 & NT is being_transposition & NT . (k + 1) = k + 1 & TR = NT | (Seg k) ) by A12, A20, A21, A25, A26, A14, A15, A16, A17, A18, A27, A22, A28; :: thesis:

end;

consider Pr being FinSequence of (Group_of_Perm (k + 1)) such that
A33: dom Pr = Seg (len P) and
A34: for m being Nat st m in Seg (len P) holds
S₂[m,Pr . m] from FINSEQ_1:sch 5(A11);
take Pr ; :: thesis:
A35: Product Pr = the multF of (Group_of_Perm (k + 1)) "**" Pr by GROUP_4:def 2;

now :: thesis:

per cases ;

suppose A36: len Pr = 0 ; :: thesis:

then A37: Seg (len Pr) = 0 ;
A38: Product Pr = the_unity_wrt the multF of (Group_of_Perm (k + 1)) by A35, A36, FINSOP_1:def 1;
the_unity_wrt the multF of (Group_of_Perm (k + 1)) = 1_ (Group_of_Perm (k + 1)) by GROUP_1:22;
then A39: Product Pr = idseq (k + 1) by A38, MATRIX_1:15;
len P = 0 by A33, A36, FINSEQ_1:def 3;
then A40: pk9 = the_unity_wrt the multF of (Group_of_Perm k) by A9, FINSOP_1:def 1;
A41: dom p9 = Seg (k + 1) by FUNCT_2:52;
A42: the_unity_wrt the multF of (Group_of_Perm k) = 1_ (Group_of_Perm k) by GROUP_1:22;
A43: for y being object st y in dom p holds
p . y = (idseq (k + 1)) . y

proof

let y be object ; :: thesis:
assume A44: y in dom p ; :: thesis:
reconsider y9 = y as Nat by A41, A44;
A45: (idseq (k + 1)) . y9 = y9 by A41, A44, FUNCT_1:18;
A46: dom pk = Seg k by FUNCT_2:52;
( y in Seg k or y in {(k + 1)} ) by A5, A41, A44, XBOOLE_0:def 3;
then ( ( pk . y = p . y & (idseq k) . y9 = y9 ) or ( p . (k + 1) = k + 1 & y = k + 1 ) ) by A4, A6, A46, FUNCT_1:18, FUNCT_1:47, TARSKI:def 1;
hence p . y = (idseq (k + 1)) . y by A40, A42, A45, MATRIX_1:15; :: thesis:

end;

dom (idseq (k + 1)) = Seg (k + 1) ;
hence ( p = Product Pr & ( for i being Nat st i in dom Pr holds
ex trans being Element of Permutations (k + 1) st
( Pr . i = trans & trans is being_transposition ) ) ) by A39, A41, A43, A37, FINSEQ_1:def 3, FUNCT_1:2; :: thesis:

end;

suppose A47: len Pr > 0 ; :: thesis:

consider fPr being sequence of (Group_of_Perm (k + 1)) such that
A48: fPr . 1 = Pr . 1 and
A49: for n being Nat st 0 <> n & n < len Pr holds
fPr . (n + 1) = the multF of (Group_of_Perm (k + 1)) . ((fPr . n),(Pr . (n + 1))) and
A50: Product Pr = fPr . (len Pr) by A35, A47, FINSOP_1:def 1;
len P > 0 by A33, A47, FINSEQ_1:def 3;
then consider fP being sequence of (Group_of_Perm k) such that
A51: fP . 1 = P . 1 and
A52: for n being Nat st 0 <> n & n < len P holds
fP . (n + 1) = the multF of (Group_of_Perm k) . ((fP . n),(P . (n + 1))) and
A53: pk = fP . (len P) by A9, FINSOP_1:def 1;
A54: len P = len Pr by A33, FINSEQ_1:def 3;
defpred S₃[ Nat] means ( $1 > 0 & $1 <= len P implies ex Prod1 being Element of Permutations (k + 1) ex Prod being Element of Permutations k st
( Prod1 = fPr . $1 & fP . $1 = Prod & Prod1 | (Seg k) = Prod & Prod1 . (k + 1) = k + 1 ) );
A55: for m being Nat st S₃[m] holds
S₃[m + 1]

proof

let m be Nat; :: thesis:
assume A56: S₃[m] ; :: thesis:
set m1 = m + 1;
assume that
m + 1 > 0 and
A57: m + 1 <= len P ; :: thesis:
(m + 1) + 0 > 0 ;
then m + 1 >= 1 by NAT_1:19;
then A58: m + 1 in Seg (len P) by A57;
A59: dom P = Seg (len P) by FINSEQ_1:def 3;
then consider tr being Element of Permutations k such that
A60: P . (m + 1) = tr and
tr is being_transposition by A8, A58;
consider tr1 being Element of Permutations (k + 1) such that
A61: tr1 = Pr . (m + 1) and
tr1 is being_transposition and
A62: tr1 . (k + 1) = k + 1 and
A63: tr = tr1 | (Seg k) by A34, A58, A59, A60;

now :: thesis:

per cases ;

suppose m = 0 ; :: thesis:

hence ex Prod1 being Element of Permutations (k + 1) ex Prod being Element of Permutations k st
( Prod1 = fPr . (m + 1) & fP . (m + 1) = Prod & Prod1 | (Seg k) = Prod & Prod1 . (k + 1) = k + 1 ) by A51, A48, A60, A61, A62, A63; :: thesis:

end;

suppose A64: m > 0 ; :: thesis:

A65: m + 0 < m + 1 by XREAL_1:6;
then consider Q1 being Element of Permutations (k + 1), Q being Element of Permutations k such that
A66: Q1 = fPr . m and
A67: fP . m = Q and
A68: Q1 | (Seg k) = Q and
A69: Q1 . (k + 1) = k + 1 by A56, A57, A64, XXREAL_0:2;
reconsider Q = Q, tr = tr as Permutation of (Seg k) by MATRIX_1:def 12;
reconsider trQ = tr * Q as Element of Permutations k by MATRIX_1:def 12;
A70: m < len P by A57, A65, XXREAL_0:2;
then A71: fP . (m + 1) = the multF of (Group_of_Perm k) . (Q,tr) by A52, A60, A64, A67;
then A72: fP . (m + 1) = trQ by MATRIX_1:def 13;
reconsider Q1 = Q1, tr1 = tr1 as Permutation of (Seg (k + 1)) by MATRIX_1:def 12;
reconsider trQ1 = tr1 * Q1 as Element of Permutations (k + 1) by MATRIX_1:def 12;
A73: trQ1 | (Seg k) = trQ by A5, A62, A63, A68, A69, Th19;
len P = len Pr by A33, FINSEQ_1:def 3;
then fPr . (m + 1) = the multF of (Group_of_Perm (k + 1)) . (Q1,tr1) by A49, A61, A64, A66, A70;
then A74: fPr . (m + 1) = trQ1 by MATRIX_1:def 13;
trQ1 . (k + 1) = k + 1 by A5, A62, A63, A68, A69, A71, Th19;
hence ex Prod1 being Element of Permutations (k + 1) ex Prod being Element of Permutations k st
( Prod1 = fPr . (m + 1) & fP . (m + 1) = Prod & Prod1 | (Seg k) = Prod & Prod1 . (k + 1) = k + 1 ) by A72, A74, A73; :: thesis:

end;

hence ex Prod1 being Element of Permutations (k + 1) ex Prod being Element of Permutations k st
( Prod1 = fPr . (m + 1) & fP . (m + 1) = Prod & Prod1 | (Seg k) = Prod & Prod1 . (k + 1) = k + 1 ) ; :: thesis:

end;

A75: S₃[ 0 ] ;
for m being Nat holds S₃[m] from NAT_1:sch 2(A75, A55);
then consider Prod1 being Element of Permutations (k + 1), Prod being Element of Permutations k such that
A76: Prod1 = fPr . (len P) and
A77: fP . (len P) = Prod and
A78: Prod1 | (Seg k) = Prod and
A79: Prod1 . (k + 1) = k + 1 by A47, A54;
reconsider Prod1 = Prod1 as Permutation of (Seg (k + 1)) by MATRIX_1:def 12;
A80: dom p9 = Seg (k + 1) by FUNCT_2:52;
A81: for y being object st y in dom p holds
p . y = Prod1 . y

proof

let y be object ; :: thesis:
assume y in dom p ; :: thesis:
then A82: ( y in Seg k or y in {(k + 1)} ) by A5, A80, XBOOLE_0:def 3;
dom pk = Seg k by FUNCT_2:52;
then ( ( Prod . y = p . y & Prod . y = Prod1 . y ) or ( y = k + 1 & p . (k + 1) = Prod1 . (k + 1) ) ) by A4, A6, A53, A77, A78, A79, A82, FUNCT_1:47, TARSKI:def 1;
hence p . y = Prod1 . y ; :: thesis:

end;

dom Prod1 = Seg (k + 1) by FUNCT_2:52;
hence p = Product Pr by A50, A54, A76, A80, A81, FUNCT_1:2; :: thesis:
thus for i being Nat st i in dom Pr holds
ex trans being Element of Permutations (k + 1) st
( Pr . i = trans & trans is being_transposition ) :: thesis:

proof

A83: Seg (len P) = dom P by FINSEQ_1:def 3;
let m be Nat; :: thesis:
assume A84: m in dom Pr ; :: thesis:
consider t being Element of Permutations k such that
A85: P . m = t and
t is being_transposition by A8, A33, A84, A83;
reconsider m9 = m as Element of NAT by ORDINAL1:def 12;
ex T being Element of Permutations (k + 1) st
( T = Pr . m9 & T is being_transposition & T . (k + 1) = k + 1 & t = T | (Seg k) ) by A33, A34, A84, A83, A85;
hence ex trans being Element of Permutations (k + 1) st
( Pr . m = trans & trans is being_transposition ) ; :: thesis:

end;

hence ( p = Product Pr & ( for i being Nat st i in dom Pr holds
ex trans being Element of Permutations (k + 1) st
( Pr . i = trans & trans is being_transposition ) ) ) ; :: thesis:

end;

now :: thesis:

per cases ;

suppose p . (k + 1) = k + 1 ; :: thesis:

hence ex P being FinSequence of (Group_of_Perm (k + 1)) st
( p = Product P & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (k + 1) st
( P . i = trans & trans is being_transposition ) ) ) by A3; :: thesis:

end;

suppose A86: p . (k + 1) <> k + 1 ; :: thesis:

A87: rng p9 = Seg (k + 1) by FUNCT_2:def 3;
consider tr being Element of Permutations (k + 1) such that
A88: tr is being_transposition and
tr . (p . (k + 1)) = k + 1 and
A89: (tr * p) . (k + 1) = k + 1 by A86, Th17;
reconsider tr9 = tr as Permutation of (Seg (k + 1)) by MATRIX_1:def 12;
reconsider trp = tr9 * p9 as Element of Permutations (k + 1) by MATRIX_1:def 12;
consider P being FinSequence of (Group_of_Perm (k + 1)) such that
A90: trp = Product P and
A91: for i being Nat st i in dom P holds
ex trans being Element of Permutations (k + 1) st
( P . i = trans & trans is being_transposition ) by A3, A89;
reconsider TRP = trp as Element of (Group_of_Perm (k + 1)) by MATRIX_1:def 13;
reconsider T = tr as Element of (Group_of_Perm (k + 1)) by MATRIX_1:def 13;
take PT = P ^ <*T*>; :: thesis:
Product PT = TRP * T by A90, GROUP_4:6;
hence Product PT = tr * (tr * p) by MATRIX_1:def 13
.= (tr * tr) * p by RELAT_1:36
.= (idseq (k + 1)) * p by A88, Th20
.= p by A87, RELAT_1:54 ;
:: thesis:
thus for m being Nat st m in dom PT holds
ex trans being Element of Permutations (k + 1) st
( PT . m = trans & trans is being_transposition ) :: thesis:

proof

set L = len P;
set L1 = (len P) + 1;
A92: Seg ((len P) + 1) = (Seg (len P)) \/ {((len P) + 1)} by FINSEQ_1:9;
len PT = (len P) + 1 by FINSEQ_2:16;
then A93: dom PT = Seg ((len P) + 1) by FINSEQ_1:def 3;
let m be Nat; :: thesis:
assume A94: m in dom PT ; :: thesis:

now :: thesis:

per cases by A94, A93, A92, XBOOLE_0:def 3;

suppose m in Seg (len P) ; :: thesis:

then A95: m in dom P by FINSEQ_1:def 3;
then PT . m = P . m by FINSEQ_1:def 7;
hence ex trans being Element of Permutations (k + 1) st
( PT . m = trans & trans is being_transposition ) by A91, A95; :: thesis:

end;

suppose m in {((len P) + 1)} ; :: thesis:

then m = (len P) + 1 by TARSKI:def 1;
hence ex trans being Element of Permutations (k + 1) st
( PT . m = trans & trans is being_transposition ) by A88, FINSEQ_1:42; :: thesis:

end;

hence ex trans being Element of Permutations (k + 1) st
( PT . m = trans & trans is being_transposition ) ; :: thesis:

end;

A96: S₁[ 0 ]

proof

let perm be Element of Permutations 0; :: thesis:
take <*> the carrier of (Group_of_Perm 0) ; :: thesis:
perm is Permutation of (Seg 0) by MATRIX_1:def 12;
then perm = idseq 0 ;
then perm = 1_ (Group_of_Perm 0) by MATRIX_1:15;
hence ( perm = Product (<*> the carrier of (Group_of_Perm 0)) & ( for i being Nat st i in dom (<*> the carrier of (Group_of_Perm 0)) holds
ex trans being Element of Permutations 0 st
( (<*> the carrier of (Group_of_Perm 0)) . i = trans & trans is being_transposition ) ) ) by GROUP_4:8; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A96, A1);
hence ex P being FinSequence of (Group_of_Perm n) st
( perm = Product P & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations n st
( P . i = trans & trans is being_transposition ) ) ) ; :: thesis: