let n be Element of NAT ; :: thesis: for N being finite Subset of NAT
for F being Function of N,(card N) st n in N & F is bijective & ( for n, k being Element of 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 Element of 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,(card N) st n in N & F is bijective & ( for n, k being Element of 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 Element of 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,(card N); :: thesis: ( n in N & F is bijective & ( for n, k being Element of 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 Element of 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 Element of 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 Element of 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 ) )
defpred S₁[ set , set ] means for k being Element of NAT st k = $1 holds
( ( k < n implies $2 = (F " ) . ((F . k) + 1) ) & ( k = n implies $2 = (F " ) . 0 ) & ( k > n implies $2 = k ) );
( F is one-to-one & rng F = card N ) by A2, FUNCT_2:def 3;
then reconsider F' = F " as Function of (card N),N by FUNCT_2:31;
A4: ( dom F = N & dom F' = card N ) by A1, FUNCT_2:def 1;
A5: for x being set st x in N holds
ex y being set st
( y in N & S₁[x,y] )

proof

let x' be set ; :: thesis: ( x' in N implies ex y being set st
( y in N & S₁[x',y] ) )
assume A6: x' in N ; :: thesis: ex y being set st
( y in N & S₁[x',y] )
reconsider x = x' as Element of NAT by A6;

now

per cases ( x < n or x = n or x > n ) by XXREAL_0:1;

suppose A7: x < n ; :: thesis: ex y being set st
( y in N & S₁[x',y] )

set FF = (F " ) . ((F . x) + 1);
( F . x < F . n & F . n in rng F & F is onto ) by A1, A2, A3, A4, A6, A7, FUNCT_1:def 5;
then ( (F . x) + 1 <= F . n & F . n < card N ) by NAT_1:13, NAT_1:45;
then (F . x) + 1 < card N by XXREAL_0:2;
then (F . x) + 1 in dom F' by A4, NAT_1:45;
then ( F' . ((F . x) + 1) in rng F' & S₁[x',(F " ) . ((F . x) + 1)] ) by A7, FUNCT_1:def 5;
hence ex y being set st
( y in N & S₁[x',y] ) ; :: thesis: verum

end;

suppose A8: x = n ; :: thesis: ex y being set st
( y in N & S₁[x',y] )

0 < card N by A1;
then 0 in dom F' by A4, NAT_1:45;
then F' . 0 in rng F' by FUNCT_1:def 5;
then ( F' . 0 in N & S₁[x',(F " ) . 0 ] ) by A8;
hence ex y being set st
( y in N & S₁[x',y] ) ; :: thesis: verum

end;

suppose x > n ; :: thesis: ex y being set st
( y in N & S₁[x',y] )

then ( x in N & S₁[x,x] ) by A6;
hence ex y being set st
( y in N & S₁[x',y] ) ; :: thesis: verum

end;

end;

end;

hence ex y being set st
( y in N & S₁[x',y] ) ; :: thesis: verum

end;

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

proof

let Px' be set ; :: according to TARSKI:def 3 :: thesis: ( not Px' in N or Px' in rng P )
assume A10: Px' in N ; :: thesis: Px' in rng P
reconsider Px = Px' as Element of NAT by A10;

now

per cases ( Px <= n or Px > n ) ;

suppose A11: Px <= n ; :: thesis: Px' in rng P

rng F' = N by A4, A2, FUNCT_1:55;
then consider x being set such that
A12: ( x in dom F' & F' . x = Px ) by A10, FUNCT_1:def 5;
( card N is Subset of NAT & F is one-to-one ) by A2, Th8;
then reconsider x = x as Element of NAT by A4, A12;

now

per cases ( x = 0 or x > 0 ) ;

suppose A13: x = 0 ; :: thesis: Px' in rng P

dom P = N by A1, FUNCT_2:def 1;
then ( P . n = (F " ) . 0 & F' . 0 = Px & P . n in rng P ) by A1, A9, A12, A13, FUNCT_1:def 5;
hence Px' in rng P ; :: thesis: verum

end;

suppose x > 0 ; :: thesis: Px' in rng P

then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
( x1 < x1 + 1 & x < card N ) by A12, NAT_1:13, NAT_1:45;
then ( x1 < card N & F is onto ) by A2, XXREAL_0:2;
then ( x1 in card N & card N = rng F ) by FUNCT_2:def 3, NAT_1:45;
then consider y being set such that
A14: ( y in dom F & F . y = x1 ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A4, A14;
A15: y < n

proof

assume y >= n ; :: thesis: contradiction
then ( ( y > n or y = n ) & F is one-to-one ) by A2, XXREAL_0:1;
then ( x1 >= F . n & x1 + 1 > x1 & x in rng F & F is one-to-one & Px in dom F & n in dom F & ( Px < n or Px = n ) ) by A1, A3, A4, A10, A11, A12, A14, FUNCT_1:55, NAT_1:13, XXREAL_0:1;
then ( x > F . n & F . Px = x & F . Px <= F . n ) by A3, A12, FUNCT_1:54, XXREAL_0:2;
hence contradiction ; :: thesis: verum

end;

( (F " ) . ((F . y) + 1) = Px & y in dom P ) by A4, A12, A14, FUNCT_2:def 1;
then ( P . y = Px & P . y in rng P ) by A9, A15, FUNCT_1:def 5;
hence Px' in rng P ; :: thesis: verum

end;

end;

end;

hence Px' in rng P ; :: thesis: verum

end;

suppose Px > n ; :: thesis: Px' in rng P

then ( Px in dom P & Px = P . Px ) by A9, A10, FUNCT_2:def 1;
hence Px' in rng P by FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence Px' in rng P ; :: thesis: verum

end;

then N = rng P by XBOOLE_0:def 10;
then ( P is onto & card N = card N ) by FUNCT_2:def 3;
then ( P is onto & P is one-to-one ) by Th70;
then reconsider P = P as Permutation of N ;
take P ; :: thesis: for k being Element of 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 Element of 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 A9; :: thesis: verum