let n be Element of NAT ; :: thesis:
let N be finite Subset of NAT; :: thesis:
let F be Function of N,(Segm (card N)); :: thesis:
assume that
A1: n in N and
A2: F is bijective and
A3: for n, k being Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ; :: thesis:
rng F = card N by A2, FUNCT_2:def 3;
then reconsider F9 = F " as Function of (card N),N by A2, FUNCT_2:25;
defpred S₁[ object , object ] means for k being Nat st k = $1 holds
( ( k < n implies $2 = (F ") . ((F . k) + 1) ) & ( k = n implies $2 = (F ") . 0 ) & ( k > n implies $2 = k ) );
A4: dom F = N by A1, FUNCT_2:def 1;
A5: dom F9 = card N by A1, FUNCT_2:def 1;
A6: for x being object st x in N holds
ex y being object st
( y in N & S₁[x,y] )

let x9 be object ; :: thesis:
assume A7: x9 in N ; :: thesis:
reconsider x = x9 as Element of NAT by A7;

per cases by XXREAL_0:1;

suppose A8: x < n ; :: thesis:

then F . x < F . n by A1, A3, A4, A7;
then A9: (F . x) + 1 <= F . n by NAT_1:13;
n in dom F by A1, A4;
then F . n in card N by FUNCT_2:5;
then F . n < card N by NAT_1:44;
then (F . x) + 1 < card N by A9, XXREAL_0:2;
then (F . x) + 1 in dom F9 by A5, NAT_1:44;
then A10: F9 . ((F . x) + 1) in rng F9 by FUNCT_1:def 3;
set FF = (F ") . ((F . x) + 1);
S₁[x9,(F ") . ((F . x) + 1)] by A8;
hence ex y being object st
( y in N & S₁[x9,y] ) by A10; :: thesis:

end;

suppose A11: x = n ; :: thesis:

0 in dom F9 by A1, A5, NAT_1:44;
then A12: F9 . 0 in rng F9 by FUNCT_1:def 3;
S₁[x9,(F ") . 0] by A11;
hence ex y being object st
( y in N & S₁[x9,y] ) by A12; :: thesis:

end;

suppose x > n ; :: thesis:

then S₁[x,x] ;
hence ex y being object st
( y in N & S₁[x9,y] ) by A7; :: thesis:

end;

end;

end;

hence ex y being object st
( y in N & S₁[x9,y] ) ; :: thesis:

end;

consider P being Function of N,N such that
A13: for x being object st x in N holds
S₁[x,P . x] from FUNCT_2:sch 1(A6);
N c= rng P

let Px9 be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: Px9 in N ; :: thesis:
reconsider Px = Px9 as Element of NAT by A14;

suppose A15: Px <= n ; :: thesis:

rng F9 = N by A2, A4, FUNCT_1:33;
then consider x being object such that
A16: x in dom F9 and
A17: F9 . x = Px by A14, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A5, A16;

suppose A18: x = 0 ; :: thesis:

A19: dom P = N by A1, FUNCT_2:def 1;
P . n = (F ") . 0 by A1, A13;
hence Px9 in rng P by A1, A17, A18, A19, FUNCT_1:def 3; :: thesis:

end;

suppose x > 0 ; :: thesis:

then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
A20: x1 < x1 + 1 by NAT_1:13;
x < card N by A16, NAT_1:44;
then x1 < card N by A20, XXREAL_0:2;
then A21: x1 in Segm (card N) by NAT_1:44;
card N = rng F by A2, FUNCT_2:def 3;
then consider y being object such that
A22: y in dom F and
A23: F . y = x1 by A21, FUNCT_1:def 3;
reconsider y = y as Element of NAT by A4, A22;
A24: y in dom P by A4, A22, FUNCT_2:def 1;
A25: y < n

assume y >= n ; :: thesis:
then ( y > n or y = n ) by XXREAL_0:1;
then A26: x1 >= F . n by A1, A3, A4, A22, A23;
x in rng F by A2, A16, FUNCT_1:33;
then A27: F . Px = x by A2, A17, FUNCT_1:32;
( Px < n or Px = n ) by A15, XXREAL_0:1;
then A28: F . Px <= F . n by A1, A3, A4, A14;
x1 + 1 > x1 by NAT_1:13;
hence contradiction by A26, A27, A28, XXREAL_0:2; :: thesis:

end;

(F ") . ((F . y) + 1) = Px by A17, A23;
then P . y = Px by A13, A22, A25;
hence Px9 in rng P by A24, FUNCT_1:def 3; :: thesis:

end;

end;

end;

hence Px9 in rng P ; :: thesis:

end;

suppose A29: Px > n ; :: thesis:

A30: Px in dom P by A14, FUNCT_2:def 1;
Px = P . Px by A13, A14, A29;
hence Px9 in rng P by A30, FUNCT_1:def 3; :: thesis:

end;

end;

end;

hence Px9 in rng P ; :: thesis:

end;

then N = rng P ;
then A31: P is onto by FUNCT_2:def 3;
card N = card N ;
then ( P is onto & P is one-to-one ) by A31, Th60;
then reconsider P = P as Permutation of N ;
take P ; :: thesis:
thus for k being Nat st k in N holds
( ( k < n implies P . k = (F ") . ((F . k) + 1) ) & ( k = n implies P . k = (F ") . 0 ) & ( k > n implies P . k = k ) ) by A13; :: thesis: