let i, j, n be Nat; :: thesis: ( i < j & i in Seg n & j in Seg n implies ex tr being Element of Permutations n st
( tr is being_transposition & tr . i = j ) )
assume that
A1: i < j and
A2: i in Seg n and
A3: j in Seg n ; :: thesis: ex tr being Element of Permutations n st
( tr is being_transposition & tr . i = j )
defpred S₁[ object , object ] means for k being Nat st k in Seg n & k = $1 holds
( ( k = i implies $2 = j ) & ( k = j implies $2 = i ) & ( k <> i & k <> j implies $2 = k ) );
A4: for x being object st x in Seg n holds
ex y being object st
( y in Seg n & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Seg n implies ex y being object st
( y in Seg n & S₁[x,y] ) )
assume A5: x in Seg n ; :: thesis: ex y being object st
( y in Seg n & S₁[x,y] )
reconsider m = x as Nat by A5;

now :: thesis: ex y being object st
( y in Seg n & S₁[x,y] )

per cases ( m = i or m = j or ( m <> i & m <> j ) ) ;

suppose m = i ; :: thesis: ex y being object st
( y in Seg n & S₁[x,y] )

then S₁[x,j] ;
hence ex y being object st
( y in Seg n & S₁[x,y] ) by A3; :: thesis: verum

end;

suppose m = j ; :: thesis: ex y being object st
( y in Seg n & S₁[x,y] )

then S₁[x,i] ;
hence ex y being object st
( y in Seg n & S₁[x,y] ) by A2; :: thesis: verum

end;

suppose ( m <> i & m <> j ) ; :: thesis: ex y being object st
( y in Seg n & S₁[x,y] )

then S₁[x,x] ;
hence ex y being object st
( y in Seg n & S₁[x,y] ) by A5; :: thesis: verum

end;

end;

end;

hence ex y being object st
( y in Seg n & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of (Seg n),(Seg n) such that
A6: for x being object st x in Seg n holds
S₁[x,f . x] from FUNCT_2:sch 1(A4);
for x1, x2 being object st x1 in Seg n & x2 in Seg n & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in Seg n & x2 in Seg n & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in Seg n and
A8: x2 in Seg n and
A9: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider k1 = x1 as Nat by A7;
( x1 = i or x1 = j or ( x1 <> i & x1 <> j ) ) ;
then A10: ( ( x1 = i & f . x1 = j ) or ( x1 = j & f . x1 = i ) or ( x1 <> i & x1 <> j & f . x1 = k1 ) ) by A6, A7;
( x2 = i or x2 = j or ( x2 <> i & x2 <> j ) ) ;
hence x1 = x2 by A6, A8, A9, A10; :: thesis: verum

end;

then A11: f is one-to-one by A2, FUNCT_2:19;
for y being object st y in Seg n holds
ex x being object st
( x in Seg n & y = f . x )

proof

let y be object ; :: thesis: ( y in Seg n implies ex x being object st
( x in Seg n & y = f . x ) )
assume A12: y in Seg n ; :: thesis: ex x being object st
( x in Seg n & y = f . x )
reconsider k = y as Nat by A12;
( ( k = i & f . j = i ) or ( k = j & f . i = j ) or ( k <> i & k <> j & f . k = k ) ) by A2, A3, A6, A12;
hence ex x being object st
( x in Seg n & y = f . x ) by A2, A3, A12; :: thesis: verum

end;

then rng f = Seg n by FUNCT_2:10;
then f is onto by FUNCT_2:def 3;
then reconsider P = f as Element of Permutations n by A11, MATRIX_1:def 12;
A13: P . j = i by A3, A6;
dom P = Seg n by A2, FUNCT_2:def 1;
then A14: for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k by A6;
take P ; :: thesis: ( P is being_transposition & P . i = j )
A15: i in dom P by A2, FUNCT_2:def 1;
A16: j in dom P by A3, FUNCT_2:def 1;
P . i = j by A2, A6;
hence ( P is being_transposition & P . i = j ) by A1, A15, A16, A13, A14; :: thesis: verum