reconsider N = n as Element of NAT by ORDINAL1:def 13;
set n1 = n + 1;
set p = perm;
set P = Permutations n;
set j = perm . i;
reconsider p' = perm as Permutation of (Seg (n + 1)) by MATRIX_2:def 11;
A2: ( dom p' = Seg (n + 1) & rng p' = Seg (n + 1) ) by FUNCT_2:67, FUNCT_2:def 3;
then A3: perm . i in Seg (n + 1) by A1, FUNCT_1:def 5;
defpred S₁[ set , set ] means for k being Nat st k in Seg n & $1 = k holds
( ( k < i implies ( ( perm . k < perm . i implies $2 = perm . k ) & ( perm . k >= perm . i implies $2 = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies $2 = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies $2 = (perm . (k + 1)) - 1 ) ) ) );
A4: for k' being set st k' in Seg n holds
ex y being set st
( y in Seg n & S₁[k',y] )

proof

let k' be set ; :: thesis: ( k' in Seg n implies ex y being set st
( y in Seg n & S₁[k',y] ) )
assume A5: k' in Seg n ; :: thesis: ex y being set st
( y in Seg n & S₁[k',y] )
consider k being Element of NAT such that
A6: ( k' = k & 1 <= k & k <= n ) by A5;
A7: k < n + 1 by A6, NAT_1:13;
then ( k + 1 <= n + 1 & 1 + 0 <= k + 1 ) by NAT_1:13;
then A8: ( k in Seg (n + 1) & k + 1 in Seg (n + 1) ) by A6, A7;
then A9: ( perm . k in Seg (n + 1) & perm . (k + 1) in Seg (n + 1) ) by A2, FUNCT_1:def 5;
set k1 = k + 1;

per cases ( ( k < i & perm . k < perm . i ) or ( k < i & perm . k >= perm . i ) or ( k >= i & perm . (k + 1) < perm . i ) or ( k >= i & perm . (k + 1) >= perm . i ) ) ;

suppose A10: ( k < i & perm . k < perm . i ) ; :: thesis: ex y being set st
( y in Seg n & S₁[k',y] )

perm . i <= n + 1 by A3, FINSEQ_1:3;
then perm . k < n + 1 by A10, XXREAL_0:2;
then ( 1 <= perm . k & perm . k <= n ) by A9, FINSEQ_1:3, NAT_1:13;
then ( perm . k in Seg n & S₁[k',perm . k] ) by A6, A10, FINSEQ_1:3;
hence ex y being set st
( y in Seg n & S₁[k',y] ) ; :: thesis: verum

end;

suppose A11: ( k < i & perm . k >= perm . i ) ; :: thesis: ex y being set st
( y in Seg n & S₁[k',y] )

then p' . k <> p' . i by A1, A8, FUNCT_2:25;
then A12: ( perm . k > perm . i & perm . i >= 1 ) by A3, A11, FINSEQ_1:3, XXREAL_0:1;
then reconsider pk1 = (perm . k) - 1 as Element of NAT by NAT_1:20;
( pk1 < pk1 + 1 & perm . k <= n + 1 ) by A9, FINSEQ_1:3, NAT_1:13;
then ( pk1 + 1 > 1 & pk1 < n + 1 ) by A12, XXREAL_0:2;
then ( pk1 >= 1 & pk1 <= n ) by NAT_1:13;
then ( pk1 in Seg n & S₁[k',pk1] ) by A6, A11;
hence ex y being set st
( y in Seg n & S₁[k',y] ) ; :: thesis: verum

end;

suppose A13: ( k >= i & perm . (k + 1) < perm . i ) ; :: thesis: ex y being set st
( y in Seg n & S₁[k',y] )

perm . i <= n + 1 by A3, FINSEQ_1:3;
then perm . (k + 1) < n + 1 by A13, XXREAL_0:2;
then ( 1 <= perm . (k + 1) & perm . (k + 1) <= n ) by A9, FINSEQ_1:3, NAT_1:13;
then ( perm . (k + 1) in Seg n & S₁[k',perm . (k + 1)] ) by A6, A13, FINSEQ_1:3;
hence ex y being set st
( y in Seg n & S₁[k',y] ) ; :: thesis: verum

end;

suppose A14: ( k >= i & perm . (k + 1) >= perm . i ) ; :: thesis: ex y being set st
( y in Seg n & S₁[k',y] )

then i < k + 1 by NAT_1:13;
then p' . (k + 1) <> p' . i by A1, A8, FUNCT_2:25;
then A15: ( perm . (k + 1) > perm . i & perm . i >= 1 ) by A3, A14, FINSEQ_1:3, XXREAL_0:1;
then reconsider pk1 = (perm . (k + 1)) - 1 as Element of NAT by NAT_1:20;
( pk1 < pk1 + 1 & perm . (k + 1) <= n + 1 ) by A9, FINSEQ_1:3, NAT_1:13;
then ( pk1 + 1 > 1 & pk1 < n + 1 ) by A15, XXREAL_0:2;
then ( pk1 >= 1 & pk1 <= n ) by NAT_1:13;
then ( pk1 in Seg n & S₁[k',pk1] ) by A6, A14;
hence ex y being set st
( y in Seg n & S₁[k',y] ) ; :: thesis: verum

end;

end;

end;

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

proof

let x1, x2 be set ; :: thesis: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 implies x1 = x2 )
assume A17: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 ) ; :: thesis: x1 = x2
A18: dom q = Seg n by FUNCT_2:67;
then consider k1 being Element of NAT such that
A19: ( x1 = k1 & 1 <= k1 & k1 <= n ) by A17;
consider k2 being Element of NAT such that
A20: ( x2 = k2 & 1 <= k2 & k2 <= n ) by A17, A18;
A21: ( k1 < n + 1 & k2 < n + 1 ) by A19, A20, NAT_1:13;
then ( k1 + 1 <= n + 1 & k2 + 1 <= n + 1 & 0 + 1 <= k1 + 1 & 0 + 1 <= k2 + 1 ) by NAT_1:13;
then A22: ( k1 in Seg (n + 1) & k2 in Seg (n + 1) & k1 + 1 in Seg (n + 1) & k2 + 1 in Seg (n + 1) ) by A19, A20, A21;

per cases ( ( k1 < i & perm . k1 < perm . i ) or ( k1 < i & perm . k1 >= perm . i ) or ( k1 >= i & perm . (k1 + 1) < perm . i ) or ( k1 >= i & perm . (k1 + 1) >= perm . i ) ) ;

suppose A23: ( k1 < i & perm . k1 < perm . i ) ; :: thesis: x1 = x2

then A24: q . k1 = p' . k1 by A16, A17, A19;

per cases ( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) ) ;

suppose ( k2 < i & perm . k2 < perm . i ) ; :: thesis: x1 = x2

then p' . k2 = p' . k1 by A16, A17, A19, A20, A24;
hence x1 = x2 by A2, A19, A20, A22, FUNCT_1:def 8; :: thesis: verum

end;

suppose A25: ( k2 < i & perm . k2 >= perm . i ) ; :: thesis: x1 = x2

then q . k2 = (perm . k2) - 1 by A16, A17, A20;
then (perm . k1) + 1 = perm . k2 by A17, A19, A20, A24;
then perm . k2 <= perm . i by A23, NAT_1:13;
then p' . k2 = p' . i by A25, XXREAL_0:1;
hence x1 = x2 by A1, A2, A22, A25, FUNCT_1:def 8; :: thesis: verum

end;

suppose A26: ( k2 >= i & perm . (k2 + 1) < perm . i ) ; :: thesis: x1 = x2

then p' . k1 = p' . (k2 + 1) by A16, A17, A19, A20, A24;
then k1 = k2 + 1 by A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A23, A26, NAT_1:13; :: thesis: verum

end;

suppose A27: ( k2 >= i & perm . (k2 + 1) >= perm . i ) ; :: thesis: x1 = x2

then perm . k1 = (perm . (k2 + 1)) - 1 by A16, A17, A19, A20, A24;
then (perm . k1) + 1 = perm . (k2 + 1) ;
then perm . (k2 + 1) <= perm . i by A23, NAT_1:13;
then p' . (k2 + 1) = perm . i by A27, XXREAL_0:1;
then k2 + 1 = i by A1, A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A27, NAT_1:13; :: thesis: verum

end;

end;

end;

suppose A28: ( k1 < i & perm . k1 >= perm . i ) ; :: thesis: x1 = x2

then A29: q . k1 = (perm . k1) - 1 by A16, A17, A19;

per cases ( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) ) ;

suppose A30: ( k2 < i & perm . k2 < perm . i ) ; :: thesis: x1 = x2

then q . k2 = p' . k2 by A16, A17, A20;
then perm . k1 = (perm . k2) + 1 by A17, A19, A20, A29;
then perm . k1 <= perm . i by A30, NAT_1:13;
then perm . k1 = perm . i by A28, XXREAL_0:1;
hence x1 = x2 by A1, A2, A22, A28, FUNCT_1:def 8; :: thesis: verum

end;

suppose ( k2 < i & perm . k2 >= perm . i ) ; :: thesis: x1 = x2

then (perm . k1) - 1 = (perm . k2) - 1 by A16, A17, A19, A20, A29;
hence x1 = x2 by A2, A19, A20, A22, FUNCT_1:def 8; :: thesis: verum

end;

suppose A31: ( k2 >= i & perm . (k2 + 1) < perm . i ) ; :: thesis: x1 = x2

then (perm . k1) - 1 = perm . (k2 + 1) by A16, A17, A19, A20, A29;
then (perm . (k2 + 1)) + 1 = perm . k1 ;
then perm . k1 <= perm . i by A31, NAT_1:13;
then p' . k1 = p' . i by A28, XXREAL_0:1;
hence x1 = x2 by A1, A2, A22, A28, FUNCT_1:def 8; :: thesis: verum

end;

suppose A32: ( k2 >= i & perm . (k2 + 1) >= perm . i ) ; :: thesis: x1 = x2

then (perm . k1) - 1 = (perm . (k2 + 1)) - 1 by A16, A17, A19, A20, A29;
then k1 = k2 + 1 by A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A28, A32, NAT_1:13; :: thesis: verum

end;

end;

end;

suppose A33: ( k1 >= i & perm . (k1 + 1) < perm . i ) ; :: thesis: x1 = x2

then A34: q . k1 = perm . (k1 + 1) by A16, A17, A19;

per cases ( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) ) ;

suppose A35: ( k2 < i & perm . k2 < perm . i ) ; :: thesis: x1 = x2

then p' . (k1 + 1) = p' . k2 by A16, A17, A19, A20, A34;
then k1 + 1 = k2 by A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A33, A35, NAT_1:13; :: thesis: verum

end;

suppose A36: ( k2 < i & perm . k2 >= perm . i ) ; :: thesis: x1 = x2

then perm . (k1 + 1) = (perm . k2) - 1 by A16, A17, A19, A20, A34;
then perm . k2 = (perm . (k1 + 1)) + 1 ;
then perm . k2 <= perm . i by A33, NAT_1:13;
then p' . k2 = p' . i by A36, XXREAL_0:1;
hence x1 = x2 by A1, A2, A22, A36, FUNCT_1:def 8; :: thesis: verum

end;

suppose ( k2 >= i & perm . (k2 + 1) < perm . i ) ; :: thesis: x1 = x2

then q . k2 = perm . (k2 + 1) by A16, A17, A20;
then k1 + 1 = k2 + 1 by A2, A17, A19, A20, A22, A34, FUNCT_1:def 8;
hence x1 = x2 by A19, A20; :: thesis: verum

end;

suppose A37: ( k2 >= i & perm . (k2 + 1) >= perm . i ) ; :: thesis: x1 = x2

then perm . (k1 + 1) = (perm . (k2 + 1)) - 1 by A16, A17, A19, A20, A34;
then perm . (k2 + 1) = (perm . (k1 + 1)) + 1 ;
then perm . (k2 + 1) <= perm . i by A33, NAT_1:13;
then p' . (k2 + 1) = p' . i by A37, XXREAL_0:1;
then k2 + 1 = i by A1, A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A37, NAT_1:13; :: thesis: verum

end;

end;

end;

suppose A38: ( k1 >= i & perm . (k1 + 1) >= perm . i ) ; :: thesis: x1 = x2

then A39: q . k1 = (perm . (k1 + 1)) - 1 by A16, A17, A19;

per cases ( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) ) ;

suppose A40: ( k2 < i & perm . k2 < perm . i ) ; :: thesis: x1 = x2

then (perm . (k1 + 1)) - 1 = perm . k2 by A16, A17, A19, A20, A39;
then perm . (k1 + 1) = (perm . k2) + 1 ;
then perm . (k1 + 1) <= perm . i by A40, NAT_1:13;
then p' . (k1 + 1) = p' . i by A38, XXREAL_0:1;
then k1 + 1 = i by A1, A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A38, NAT_1:13; :: thesis: verum

end;

suppose A41: ( k2 < i & perm . k2 >= perm . i ) ; :: thesis: x1 = x2

then (perm . (k1 + 1)) - 1 = (perm . k2) - 1 by A16, A17, A19, A20, A39;
then k1 + 1 = k2 by A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A38, A41, NAT_1:13; :: thesis: verum

end;

suppose A42: ( k2 >= i & perm . (k2 + 1) < perm . i ) ; :: thesis: x1 = x2

then (perm . (k1 + 1)) - 1 = perm . (k2 + 1) by A16, A17, A19, A20, A39;
then perm . (k1 + 1) = (perm . (k2 + 1)) + 1 ;
then perm . (k1 + 1) <= perm . i by A42, NAT_1:13;
then p' . (k1 + 1) = p' . i by A38, XXREAL_0:1;
then k1 + 1 = i by A1, A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A38, NAT_1:13; :: thesis: verum

end;

suppose ( k2 >= i & perm . (k2 + 1) >= perm . i ) ; :: thesis: x1 = x2

then (perm . (k1 + 1)) - 1 = (perm . (k2 + 1)) - 1 by A16, A17, A19, A20, A39;
then k1 + 1 = k2 + 1 by A2, A22, FUNCT_1:def 8;
hence x1 = x2 by A19, A20; :: thesis: verum

end;

end;

end;

end;

end;

then ( q is one-to-one & card (finSeg N) = card (finSeg N) ) by FUNCT_1:def 8;
then ( q is one-to-one & q is onto ) by STIRL2_1:70;
then q is Permutation of (Seg n) ;
then reconsider q = q as Element of Permutations n by MATRIX_2:def 11;
take q ; :: thesis: for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies q . k = perm . k ) & ( perm . k >= perm . i implies q . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q . k = (perm . (k + 1)) - 1 ) ) ) )
thus for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies q . k = perm . k ) & ( perm . k >= perm . i implies q . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q . k = (perm . (k + 1)) - 1 ) ) ) ) by A16; :: thesis: verum