let n be Nat; :: thesis:
let K be Field; :: thesis:
set n2 = n + 2;
set G = Group_of_Perm (n + 2);
defpred S₁[ Nat] means for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P & len P = $1 & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ) holds
( ( (len P) mod 2 = 0 implies sgn p2,K = 1_ K ) & ( (len P) mod 2 = 1 implies sgn p2,K = - (1_ K) ) );
A1: S₁[ 0 ]

let P be FinSequence of (Group_of_Perm (n + 2)); :: thesis:
let p2 be Element of Permutations (n + 2); :: thesis:
assume that
A2: ( p2 = Product P & len P = 0 ) and
for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ; :: thesis:
( dom P = Seg 0 & Seg 0 = 0 ) by A2, FINSEQ_1:def 3;
then P = <*> the carrier of (Group_of_Perm (n + 2)) ;
then Product P = 1_ (Group_of_Perm (n + 2)) by GROUP_4:11;
then Product P = idseq (n + 2) by MATRIX_2:28;
hence ( ( (len P) mod 2 = 0 implies sgn p2,K = 1_ K ) & ( (len P) mod 2 = 1 implies sgn p2,K = - (1_ K) ) ) by A2, Th12, NAT_D:26; :: thesis:

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume A4: S₁[k] ; :: thesis:
set k1 = k + 1;
let P be FinSequence of (Group_of_Perm (n + 2)); :: thesis:
let p2 be Element of Permutations (n + 2); :: thesis:
assume that
A5: ( p2 = Product P & len P = k + 1 ) and
A6: for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ; :: thesis:
( len P in Seg (len P) & Seg (len P) = dom P ) by A5, FINSEQ_1:5, FINSEQ_1:def 3;
then consider x being set , Q being FinSequence such that
A7: ( P = <*x*> ^ Q & len P = (len Q) + 1 ) by RELAT_1:60, REWRITE1:5;
reconsider X = <*x*>, Q = Q as FinSequence of (Group_of_Perm (n + 2)) by A7, FINSEQ_1:50;
reconsider PQ = Product Q as Element of Permutations (n + 2) by MATRIX_2:def 13;
A8: for i being Nat st i in dom Q holds
ex trans being Element of Permutations (n + 2) st
( Q . i = trans & trans is being_transposition )

let i be Nat; :: thesis:
assume A9: i in dom Q ; :: thesis:
( Q . i = P . ((len X) + i) & (len X) + i in dom P ) by A7, A9, FINSEQ_1:41, FINSEQ_1:def 7;
hence ex trans being Element of Permutations (n + 2) st
( Q . i = trans & trans is being_transposition ) by A6; :: thesis:

end;

1 + 0 <= k + 1 by XREAL_1:9;
then 1 in Seg (k + 1) ;
then ( 1 in dom P & P . 1 = x ) by A5, A7, FINSEQ_1:58, FINSEQ_1:def 3;
then consider tr being Element of Permutations (n + 2) such that
A10: ( x = tr & tr is being_transposition ) by A6;
reconsider Tr = tr as Element of (Group_of_Perm (n + 2)) by MATRIX_2:def 13;
A11: p2 = Tr * (Product Q) by A5, A7, A10, GROUP_4:10
.= PQ * tr by MATRIX_2:def 13 ;
then A12: sgn p2,K = - (sgn PQ,K) by A10, Th13;

per cases ) mod 2 = 0 or (len Q) mod 2 = 1 ) by NAT_D:12;

suppose A13: (len Q) mod 2 = 0 ; :: thesis:

then ( sgn PQ,K = 1_ K & 0 < 2 - 1 ) by A4, A5, A7, A8;
then ( sgn p2,K = - (1_ K) & (len P) mod 2 = 0 + 1 ) by A7, A10, A11, A13, Th13, RADIX_1:3;
hence ( ( (len P) mod 2 = 0 implies sgn p2,K = 1_ K ) & ( (len P) mod 2 = 1 implies sgn p2,K = - (1_ K) ) ) ; :: thesis:

end;

suppose A14: (len Q) mod 2 = 1 ; :: thesis:

then ( sgn PQ,K = - (1_ K) & 2 - 1 = 1 ) by A4, A5, A7, A8;
hence ( ( (len P) mod 2 = 0 implies sgn p2,K = 1_ K ) & ( (len P) mod 2 = 1 implies sgn p2,K = - (1_ K) ) ) by A7, A12, A14, RADIX_1:2, RLVECT_1:30; :: thesis:

end;

hence ( ( (len P) mod 2 = 0 implies sgn p2,K = 1_ K ) & ( (len P) mod 2 = 1 implies sgn p2,K = - (1_ K) ) ) ; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A3);
hence for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ) holds
( ( (len P) mod 2 = 0 implies sgn p2,K = 1_ K ) & ( (len P) mod 2 = 1 implies sgn p2,K = - (1_ K) ) ) ; :: thesis: