let n be Element of NAT ; :: thesis: for N being finite Subset of NAT
for F being Function of N,(Segm (card N)) st n in N & F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ) holds
ex P being Permutation of N st
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 ) )

let N be finite Subset of NAT; :: thesis: for F being Function of N,(Segm (card N)) st n in N & F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ) holds
ex P being Permutation of N st
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 ) )

let F be Function of N,(Segm (card N)); :: thesis: ( n in N & F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ) implies ex P being Permutation of N st
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 ) ) )

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: ex P being Permutation of N st
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 ) )

rng F = card N by ;
then reconsider F9 = F " as Function of (card N),N by ;
defpred S1[ 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 ;
A5: dom F9 = card N by ;
A6: for x being object st x in N holds
ex y being object st
( y in N & S1[x,y] )
proof
let x9 be object ; :: thesis: ( x9 in N implies ex y being object st
( y in N & S1[x9,y] ) )

assume A7: x9 in N ; :: thesis: ex y being object st
( y in N & S1[x9,y] )

reconsider x = x9 as Element of NAT by A7;
now :: thesis: ex y being object st
( y in N & S1[x9,y] )
per cases ( x < n or x = n or x > n ) by XXREAL_0:1;
suppose A8: x < n ; :: thesis: ex y being object st
( y in N & S1[x9,y] )

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 ;
then (F . x) + 1 in dom F9 by ;
then A10: F9 . ((F . x) + 1) in rng F9 by FUNCT_1:def 3;
set FF = (F ") . ((F . x) + 1);
S1[x9,(F ") . ((F . x) + 1)] by A8;
hence ex y being object st
( y in N & S1[x9,y] ) by A10; :: thesis: verum
end;
suppose A11: x = n ; :: thesis: ex y being object st
( y in N & S1[x9,y] )

0 in dom F9 by ;
then A12: F9 . 0 in rng F9 by FUNCT_1:def 3;
S1[x9,(F ") . 0] by A11;
hence ex y being object st
( y in N & S1[x9,y] ) by A12; :: thesis: verum
end;
suppose x > n ; :: thesis: ex y being object st
( y in N & S1[x9,y] )

end;
end;
end;
hence ex y being object st
( y in N & S1[x9,y] ) ; :: thesis: verum
end;
consider P being Function of N,N such that
A13: for x being object st x in N holds
S1[x,P . x] from N c= rng P
proof
let Px9 be object ; :: according to TARSKI:def 3 :: thesis: ( not Px9 in N or Px9 in rng P )
assume A14: Px9 in N ; :: thesis: Px9 in rng P
reconsider Px = Px9 as Element of NAT by A14;
now :: thesis: Px9 in rng P
per cases ( Px <= n or Px > n ) ;
suppose A15: Px <= n ; :: thesis: Px9 in rng P
rng F9 = N by ;
then consider x being object such that
A16: x in dom F9 and
A17: F9 . x = Px by ;
reconsider x = x as Element of NAT by ;
now :: thesis: Px9 in rng P
per cases ( x = 0 or x > 0 ) ;
suppose A18: x = 0 ; :: thesis: Px9 in rng P
A19: dom P = N by ;
P . n = (F ") . 0 by ;
hence Px9 in rng P by ; :: thesis: verum
end;
suppose x > 0 ; :: thesis: Px9 in rng P
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 ;
then x1 < card N by ;
then A21: x1 in Segm (card N) by NAT_1:44;
card N = rng F by ;
then consider y being object such that
A22: y in dom F and
A23: F . y = x1 by ;
reconsider y = y as Element of NAT by ;
A24: y in dom P by ;
A25: y < n
proof
assume y >= n ; :: thesis: contradiction
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 ;
then A27: F . Px = x by ;
( Px < n or Px = n ) by ;
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: verum
end;
(F ") . ((F . y) + 1) = Px by ;
then P . y = Px by ;
hence Px9 in rng P by ; :: thesis: verum
end;
end;
end;
hence Px9 in rng P ; :: thesis: verum
end;
suppose A29: Px > n ; :: thesis: Px9 in rng P
A30: Px in dom P by ;
Px = P . Px by ;
hence Px9 in rng P by ; :: thesis: verum
end;
end;
end;
hence Px9 in rng P ; :: thesis: verum
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 ;
then reconsider P = P as Permutation of N ;
take P ; :: thesis: 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 ) )

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: verum