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 A2, FUNCT_2:def 3;

then reconsider F9 = F " as Function of (card N),N by A2, FUNCT_2:25;

defpred S_{1}[ 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_{1}[x,y] )

A13: for x being object st x in N holds

S_{1}[x,P . x]
from FUNCT_2:sch 1(A6);

N c= 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: 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

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 A2, FUNCT_2:def 3;

then reconsider F9 = F " as Function of (card N),N by A2, FUNCT_2:25;

defpred S

( ( 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

proof

consider P being Function of N,N such that
let x9 be object ; :: thesis: ( x9 in N implies ex y being object st

( y in N & S_{1}[x9,y] ) )

assume A7: x9 in N ; :: thesis: ex y being object st

( y in N & S_{1}[x9,y] )

reconsider x = x9 as Element of NAT by A7;

( y in N & S_{1}[x9,y] )
; :: thesis: verum

end;( y in N & S

assume A7: x9 in N ; :: thesis: ex y being object st

( y in N & S

reconsider x = x9 as Element of NAT by A7;

now :: thesis: ex y being object st

( y in N & S_{1}[x9,y] )end;

hence
ex y being object st ( y in N & S

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

end;

suppose A8:
x < n
; :: thesis: ex y being object st

( y in N & S_{1}[x9,y] )

( y in N & S

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_{1}[x9,(F ") . ((F . x) + 1)]
by A8;

hence ex y being object st

( y in N & S_{1}[x9,y] )
by A10; :: thesis: verum

end;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

hence ex y being object st

( y in N & S

suppose A11:
x = n
; :: thesis: ex y being object st

( y in N & S_{1}[x9,y] )

( y in N & S

0 in dom F9
by A1, A5, NAT_1:44;

then A12: F9 . 0 in rng F9 by FUNCT_1:def 3;

S_{1}[x9,(F ") . 0]
by A11;

hence ex y being object st

( y in N & S_{1}[x9,y] )
by A12; :: thesis: verum

end;then A12: F9 . 0 in rng F9 by FUNCT_1:def 3;

S

hence ex y being object st

( y in N & S

( y in N & S

A13: for x being object st x in N holds

S

N c= rng P

proof

then
N = rng P
;
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;

end;assume A14: Px9 in N ; :: thesis: Px9 in rng P

reconsider Px = Px9 as Element of NAT by A14;

now :: thesis: Px9 in rng Pend;

hence
Px9 in rng P
; :: thesis: verumper cases
( Px <= n or Px > n )
;

end;

suppose A15:
Px <= n
; :: thesis: Px9 in rng P

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;

end;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;

now :: thesis: Px9 in rng Pend;

hence
Px9 in rng P
; :: thesis: verumper cases
( x = 0 or x > 0 )
;

end;

suppose A18:
x = 0
; :: thesis: Px9 in rng P

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

end;P . n = (F ") . 0 by A1, A13;

hence Px9 in rng P by A1, A17, A18, A19, FUNCT_1:def 3; :: thesis: verum

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

then P . y = Px by A13, A22, A25;

hence Px9 in rng P by A24, FUNCT_1:def 3; :: thesis: verum

end;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

proof

(F ") . ((F . y) + 1) = Px
by A17, A23;
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 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: verum

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

then P . y = Px by A13, A22, A25;

hence Px9 in rng P by A24, FUNCT_1:def 3; :: thesis: verum

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