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: n is Element of NAT by ORDINAL1:def 12;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A3: 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_2:def 9;
set Gk1 = Group_of_Perm (k + 1);
A4: 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 A5: 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_2:def 9;
A6: Seg (k + 1) = (Seg k) \/ {(k + 1)} by FINSEQ_1:9;
then consider pk being Permutation of (Seg k) such that
A7: p9 | (Seg k) = pk by A5, Th18, FINSEQ_3:8;
reconsider pk9 = pk as Element of Permutations k by MATRIX_2:def 9;
consider P being FinSequence of (Group_of_Perm k) such that
A8: pk9 = Product P and
A9: 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 A3;
A10: pk9 = the multF of (Group_of_Perm k) "**" P by A8, 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) );
A11: not k + 1 in Seg k by FINSEQ_3:8;
A12: 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
A13: P . m = tr and
A14: tr is being_transposition by A9;
consider i9, j9 being Nat such that
A15: i9 in dom tr and
A16: j9 in dom tr and
A17: i9 <> j9 and
A18: tr . i9 = j9 and
A19: tr . j9 = i9 and
A20: for k being Nat st k <> i9 & k <> j9 & k in dom tr holds
tr . k = k by A14, MATRIX_2:def 11;
reconsider tr9 = tr as Permutation of (Seg k) by MATRIX_2:def 9;
consider newt being Function of (Seg (k + 1)),(Seg (k + 1)) such that
A21: newt | (Seg k) = tr9 and
A22: newt . (k + 1) = k + 1 by A6, A11, STIRL2_1:57;
A23: newt . j9 = tr . j9 by A21, A16, FUNCT_1:47;
A24: ( Seg k is empty implies Seg k is empty ) ;
then A25: newt is onto by A6, A21, A22, STIRL2_1:58;
newt is one-to-one by A6, A11, A24, A21, A22, STIRL2_1:58;
then reconsider NT = newt as Element of Permutations (k + 1) by A25, MATRIX_2:def 9;
reconsider NT9 = NT as Element of (Group_of_Perm (k + 1)) by MATRIX_2:def 10;
take NT9 ; :: thesis:
let I be Nat; :: thesis:
let TR be Element of Permutations k; :: thesis:
assume that
I in dom P and
A26: P . I = TR and
A27: I = m ; :: thesis:
take NT ; :: thesis:
A28: dom tr c= dom newt by A21, RELAT_1:60;
A29: for m being Nat st m <> i9 & m <> j9 & m in dom newt holds
newt . m = m

proof

A30: dom tr9 = Seg k by FUNCT_2:52;
let m be Nat; :: thesis:
assume that
A31: m <> i9 and
A32: m <> j9 and
A33: 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 A6, A33, XBOOLE_0:def 3;
then ( m in dom tr or m = k + 1 ) by A30, TARSKI:def 1;
then ( ( tr . m = newt . m & tr . m = m ) or newt . m = m ) by A21, A22, A20, A31, A32, FUNCT_1:47;
hence newt . m = m ; :: thesis:

end;

newt . i9 = tr . i9 by A21, A15, FUNCT_1:47;
hence ( NT = NT9 & NT is being_transposition & NT . (k + 1) = k + 1 & TR = NT | (Seg k) ) by A13, A21, A22, A26, A27, A15, A16, A17, A18, A19, A28, A23, A29, MATRIX_2:def 11; :: thesis:

end;

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

now

per cases ;

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

then A38: Seg (len Pr) = 0 ;
A39: Product Pr = the_unity_wrt the multF of (Group_of_Perm (k + 1)) by A36, A37, 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 A40: Product Pr = idseq (k + 1) by A39, MATRIX_2:24;
len P = 0 by A34, A37, FINSEQ_1:def 3;
then A42: pk9 = the_unity_wrt the multF of (Group_of_Perm k) by A10, FINSOP_1:def 1;
A43: dom p9 = Seg (k + 1) by FUNCT_2:52;
A44: the_unity_wrt the multF of (Group_of_Perm k) = 1_ (Group_of_Perm k) by GROUP_1:22;
A45: for y being set st y in dom p holds
p . y = (idseq (k + 1)) . y

proof

let y be set ; :: thesis:
assume A46: y in dom p ; :: thesis:
reconsider y9 = y as Nat by A43, A46;
A47: (idseq (k + 1)) . y9 = y9 by A43, A46, FUNCT_1:18;
A48: dom pk = Seg k by FUNCT_2:52;
( y in Seg k or y in {(k + 1)} ) by A6, A43, A46, XBOOLE_0:def 3;
then ( ( pk . y = p . y & (idseq k) . y9 = y9 ) or ( p . (k + 1) = k + 1 & y = k + 1 ) ) by A5, A7, A48, FUNCT_1:18, FUNCT_1:47, TARSKI:def 1;
hence p . y = (idseq (k + 1)) . y by A42, A44, A47, MATRIX_2:24; :: thesis:

end;

dom (idseq (k + 1)) = Seg (k + 1) by FUNCT_2:52;
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 A40, A43, A45, A38, FINSEQ_1:def 3, FUNCT_1:2; :: thesis:

end;

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

consider fPr being Function of NAT,(Group_of_Perm (k + 1)) such that
A50: fPr . 1 = Pr . 1 and
A51: for n being Element of 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
A52: Product Pr = fPr . (len Pr) by A36, A49, FINSOP_1:def 1;
len P > 0 by A34, A49, FINSEQ_1:def 3;
then consider fP being Function of NAT,(Group_of_Perm k) such that
A54: fP . 1 = P . 1 and
A55: for n being Element of NAT st 0 <> n & n < len P holds
fP . (n + 1) = the multF of (Group_of_Perm k) . ((fP . n),(P . (n + 1))) and
A56: pk = fP . (len P) by A10, FINSOP_1:def 1;
A57: len P = len Pr by A34, 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 ) );
A58: for m being Element of NAT st S₃[m] holds
S₃[m + 1]

proof

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

now

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 A54, A50, A63, A64, A65, A66; :: thesis:

end;

suppose A67: m > 0 ; :: thesis:

A68: 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
A69: Q1 = fPr . m and
A70: fP . m = Q and
A71: Q1 | (Seg k) = Q and
A72: Q1 . (k + 1) = k + 1 by A59, A60, A67, XXREAL_0:2;
reconsider Q = Q, tr = tr as Permutation of (Seg k) by MATRIX_2:def 9;
reconsider trQ = tr * Q as Element of Permutations k by MATRIX_2:def 9;
A73: m < len P by A60, A68, XXREAL_0:2;
then A74: fP . (m + 1) = the multF of (Group_of_Perm k) . (Q,tr) by A55, A63, A67, A70;
then A75: fP . (m + 1) = trQ by MATRIX_2:def 10;
reconsider Q1 = Q1, tr1 = tr1 as Permutation of (Seg (k + 1)) by MATRIX_2:def 9;
reconsider trQ1 = tr1 * Q1 as Element of Permutations (k + 1) by MATRIX_2:def 9;
A76: trQ1 | (Seg k) = trQ by A6, A65, A66, A71, A72, Th19;
len P = len Pr by A34, FINSEQ_1:def 3;
then fPr . (m + 1) = the multF of (Group_of_Perm (k + 1)) . (Q1,tr1) by A51, A64, A67, A69, A73;
then A77: fPr . (m + 1) = trQ1 by MATRIX_2:def 10;
trQ1 . (k + 1) = k + 1 by A6, A65, A66, A71, A72, A74, 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 A75, A77, A76; :: 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;

A78: S₃[ 0 ] ;
for m being Element of NAT holds S₃[m] from NAT_1:sch 1(A78, A58);
then consider Prod1 being Element of Permutations (k + 1), Prod being Element of Permutations k such that
A79: Prod1 = fPr . (len P) and
A80: fP . (len P) = Prod and
A81: Prod1 | (Seg k) = Prod and
A82: Prod1 . (k + 1) = k + 1 by A49, A57;
reconsider Prod1 = Prod1 as Permutation of (Seg (k + 1)) by MATRIX_2:def 9;
A83: dom p9 = Seg (k + 1) by FUNCT_2:52;
A84: for y being set st y in dom p holds
p . y = Prod1 . y

proof

let y be set ; :: thesis:
assume y in dom p ; :: thesis:
then A85: ( y in Seg k or y in {(k + 1)} ) by A6, A83, 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 A5, A7, A56, A80, A81, A82, A85, 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 A52, A57, A79, A83, A84, 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

A86: Seg (len P) = dom P by FINSEQ_1:def 3;
let m be Nat; :: thesis:
assume A87: m in dom Pr ; :: thesis:
consider t being Element of Permutations k such that
A88: P . m = t and
t is being_transposition by A9, A34, A87, A86;
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 A34, A35, A87, A86, A88;
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

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 A4; :: thesis:

end;

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

A90: rng p9 = Seg (k + 1) by FUNCT_2:def 3;
consider tr being Element of Permutations (k + 1) such that
A91: tr is being_transposition and
tr . (p . (k + 1)) = k + 1 and
A92: (tr * p) . (k + 1) = k + 1 by A89, Th17;
reconsider tr9 = tr as Permutation of (Seg (k + 1)) by MATRIX_2:def 9;
reconsider trp = tr9 * p9 as Element of Permutations (k + 1) by MATRIX_2:def 9;
consider P being FinSequence of (Group_of_Perm (k + 1)) such that
A93: trp = Product P and
A94: 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 A4, A92;
reconsider TRP = trp as Element of (Group_of_Perm (k + 1)) by MATRIX_2:def 10;
reconsider T = tr as Element of (Group_of_Perm (k + 1)) by MATRIX_2:def 10;
take PT = P ^ <*T*>; :: thesis:
Product PT = TRP * T by A93, GROUP_4:6;
hence Product PT = tr * (tr * p) by MATRIX_2:def 10
.= (tr * tr) * p by RELAT_1:36
.= (idseq (k + 1)) * p by A91, Th20
.= p by A90, 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;
A95: Seg ((len P) + 1) = (Seg (len P)) \/ {((len P) + 1)} by FINSEQ_1:9;
len PT = (len P) + 1 by FINSEQ_2:16;
then A96: dom PT = Seg ((len P) + 1) by FINSEQ_1:def 3;
let m be Nat; :: thesis:
assume A97: m in dom PT ; :: thesis:

now

per cases by A97, A96, A95, XBOOLE_0:def 3;

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

then A98: 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 A94, A98; :: 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 A91, FINSEQ_1:42; :: thesis:

end;

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

end;

A99: 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_2:def 9;
then perm = idseq 0 ;
then perm = 1_ (Group_of_Perm 0) by MATRIX_2:24;
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 Element of NAT holds S₁[n] from NAT_1:sch 1(A99, A2);
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 ) ) ) by A1; :: thesis: