let n, i, j be Nat; :: thesis:
assume A1: ( i in Seg n & j in Seg n & i < j ) ; :: thesis:
set P = Permutations n;
consider tr being Element of Permutations n such that
A2: ( tr is being_transposition & tr . i = j ) by A1, Th16;
consider PE being Permutation of (Permutations n) such that
A3: for p being Element of Permutations n holds PE . p = p * tr by Th44;
set EVEN = { p where p is Element of Permutations n : p is even } ;
set ODD = { q where q is Element of Permutations n : not q is even } ;
A4: { p where p is Element of Permutations n : p is even } c= Permutations n

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Element of Permutations n : p is even } ; :: thesis:
then ex p being Element of Permutations n st
( p = x & p is even ) ;
hence x in Permutations n ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in { q where q is Element of Permutations n : not q is even } ; :: thesis:
ex q being Element of Permutations n st
( q = x & not q is even ) by A6;
hence x in Permutations n ; :: thesis:

end;

then reconsider O = { q where q is Element of Permutations n : not q is even } , E = { p where p is Element of Permutations n : p is even } as finite set by A4, FINSET_1:13, MATRIX_2:30;
take O ; :: thesis:
take E ; :: thesis:
thus ( E = { p where p is Element of Permutations n : p is even } & O = { q where q is Element of Permutations n : not q is even } ) ; :: thesis:
thus E /\ O = {} :: thesis:

assume E /\ O <> {} ; :: thesis:
then consider x being set such that
A7: x in E /\ O by XBOOLE_0:def 1;
( x in E & x in O ) by A7, XBOOLE_0:def 4;
then ( ex p being Element of Permutations n st
( p = x & p is even ) & ex q being Element of Permutations n st
( q = x & not q is even ) ) ;
hence contradiction ; :: thesis:

end;

thus E \/ O = Permutations n :: thesis:

thus E \/ O c= Permutations n by A4, A5, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in Permutations n ; :: thesis:
reconsider p = x as Element of Permutations n by A8;
( p is even or not p is even ) ;
then ( p in E or p in O ) ;
hence x in E \/ O by XBOOLE_0:def 3; :: thesis:

end;

{i,j} in 2Set (Seg n) by A1, Th1;
then reconsider n2 = n - 2 as Nat by Th2, NAT_1:21, NAT_1:23;
tr is Element of Permutations (n2 + 2) ;
then not tr is even by A2, Th27;
then A9: PE .: E = O by A3, Th47;
set PERM = PE | E;
A10: dom PE = Permutations n by FUNCT_2:67;
then A11: ( dom (PE | E) = E & rng (PE | E) = O ) by A4, A9, RELAT_1:91, RELAT_1:148;
then reconsider PERM = PE | E as Function of E,O by FUNCT_2:3;
take PERM ; :: thesis:
take tr ; :: thesis:
( PERM is one-to-one & PERM is onto ) by A11, FUNCT_1:84, FUNCT_2:def 3;
hence ( tr is being_transposition & tr . i = j & dom PERM = E & PERM is bijective ) by A2, A4, A10, RELAT_1:91; :: thesis:
let p be Element of Permutations n; :: thesis:
assume A12: p in E ; :: thesis:
( PERM . p = PE . p & PE . p = p * tr ) by A3, A11, A12, FUNCT_1:70;
hence PERM . p = p * tr ; :: thesis: