defpred S_{1}[ Nat] means for N being finite Subset of NAT st card N = $1 holds

ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) );

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A32, A1);

hence for N being finite Subset of NAT ex Order being Function of N,(Segm (card N)) st

( Order is bijective & ( for n, k being Nat st n in dom Order & k in dom Order & n < k holds

Order . n < Order . k ) ) ; :: thesis: verum

ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) );

A1: for k being Nat st S

S

proof

A32:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let N be finite Subset of NAT; :: thesis: ( card N = k + 1 implies ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) ) )

assume A3: card N = k + 1 ; :: thesis: ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) )

defpred S_{2}[ set ] means $1 in N;

ex x being object st x in N by A3, CARD_1:27, XBOOLE_0:def 1;

then A4: ex n being Nat st S_{2}[n]
;

consider m9 being Nat such that

A5: for n being Nat st n in N holds

n <= m9 by Th56;

A6: for n being Nat st S_{2}[n] holds

n <= m9 by A5;

consider m being Nat such that

A7: ( S_{2}[m] & ( for n being Nat st S_{2}[n] holds

n <= m ) ) from NAT_1:sch 6(A6, A4);

set Nm = N \ {m};

consider F being Function of (N \ {m}),(Segm (card (N \ {m}))) such that

A8: F is bijective and

A9: for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k by A2, A3, A7, Th55;

A10: card (N \ {m}) = k by A3, A7, Th55;

A11: (Segm k) \/ {k} = Segm (k + 1) by AFINSQ_1:2;

A12: ( card (N \ {m}) is empty implies N \ {m} is empty ) ;

m in {m} by TARSKI:def 1;

then not m in N \ {m} by XBOOLE_0:def 5;

then consider G being Function of ((N \ {m}) \/ {m}),((card (N \ {m})) \/ {k}) such that

A13: G | (N \ {m}) = F and

A14: G . m = k by A12, Th57;

N = (N \ {m}) \/ {m} by A7, ZFMISC_1:116;

then reconsider G9 = G as Function of N,(Segm (card N)) by A3, A10, A11;

take G9 ; :: thesis: ( G9 is bijective & ( for n, k being Nat st n in dom G9 & k in dom G9 & n < k holds

G9 . n < G9 . k ) )

not k in card (N \ {m}) by A10;

then ( G is one-to-one & G is onto ) by A8, A12, A13, A14, Th58;

hence G9 is bijective by A11, A3, A10; :: thesis: for n, k being Nat st n in dom G9 & k in dom G9 & n < k holds

G9 . n < G9 . k

thus for n, k being Nat st n in dom G9 & k in dom G9 & n < k holds

G9 . n < G9 . k :: thesis: verum

end;assume A2: S

let N be finite Subset of NAT; :: thesis: ( card N = k + 1 implies ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) ) )

assume A3: card N = k + 1 ; :: thesis: ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) )

defpred S

ex x being object st x in N by A3, CARD_1:27, XBOOLE_0:def 1;

then A4: ex n being Nat st S

consider m9 being Nat such that

A5: for n being Nat st n in N holds

n <= m9 by Th56;

A6: for n being Nat st S

n <= m9 by A5;

consider m being Nat such that

A7: ( S

n <= m ) ) from NAT_1:sch 6(A6, A4);

set Nm = N \ {m};

consider F being Function of (N \ {m}),(Segm (card (N \ {m}))) such that

A8: F is bijective and

A9: for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k by A2, A3, A7, Th55;

A10: card (N \ {m}) = k by A3, A7, Th55;

A11: (Segm k) \/ {k} = Segm (k + 1) by AFINSQ_1:2;

A12: ( card (N \ {m}) is empty implies N \ {m} is empty ) ;

m in {m} by TARSKI:def 1;

then not m in N \ {m} by XBOOLE_0:def 5;

then consider G being Function of ((N \ {m}) \/ {m}),((card (N \ {m})) \/ {k}) such that

A13: G | (N \ {m}) = F and

A14: G . m = k by A12, Th57;

N = (N \ {m}) \/ {m} by A7, ZFMISC_1:116;

then reconsider G9 = G as Function of N,(Segm (card N)) by A3, A10, A11;

take G9 ; :: thesis: ( G9 is bijective & ( for n, k being Nat st n in dom G9 & k in dom G9 & n < k holds

G9 . n < G9 . k ) )

not k in card (N \ {m}) by A10;

then ( G is one-to-one & G is onto ) by A8, A12, A13, A14, Th58;

hence G9 is bijective by A11, A3, A10; :: thesis: for n, k being Nat st n in dom G9 & k in dom G9 & n < k holds

G9 . n < G9 . k

thus for n, k being Nat st n in dom G9 & k in dom G9 & n < k holds

G9 . n < G9 . k :: thesis: verum

proof

A15:
for i being Nat st i in N \ {m} holds

( i < m & G9 . i < k )

assume that

A21: i in dom G9 and

A22: j in dom G9 and

A23: i < j ; :: thesis: G9 . i < G9 . j

A24: dom G9 = (N \ {m}) \/ {m} by FUNCT_2:def 1;

end;( i < m & G9 . i < k )

proof

let i, j be Nat; :: thesis: ( i in dom G9 & j in dom G9 & i < j implies G9 . i < G9 . j )
let i be Nat; :: thesis: ( i in N \ {m} implies ( i < m & G9 . i < k ) )

assume A16: i in N \ {m} ; :: thesis: ( i < m & G9 . i < k )

not i in {m} by A16, XBOOLE_0:def 5;

then A17: i <> m by TARSKI:def 1;

S_{2}[i]
by A16, XBOOLE_0:def 5;

then i <= m by A7;

hence i < m by A17, XXREAL_0:1; :: thesis: G9 . i < k

A18: i in dom F by A16, FUNCT_2:def 1;

then A19: F . i = G9 . i by A13, FUNCT_1:47;

A20: F . i in card (N \ {m}) by A18, FUNCT_2:5;

card (N \ {m}) = k by A3, A7, Th55;

hence G9 . i < k by A19, NAT_1:44, A20; :: thesis: verum

end;assume A16: i in N \ {m} ; :: thesis: ( i < m & G9 . i < k )

not i in {m} by A16, XBOOLE_0:def 5;

then A17: i <> m by TARSKI:def 1;

S

then i <= m by A7;

hence i < m by A17, XXREAL_0:1; :: thesis: G9 . i < k

A18: i in dom F by A16, FUNCT_2:def 1;

then A19: F . i = G9 . i by A13, FUNCT_1:47;

A20: F . i in card (N \ {m}) by A18, FUNCT_2:5;

card (N \ {m}) = k by A3, A7, Th55;

hence G9 . i < k by A19, NAT_1:44, A20; :: thesis: verum

assume that

A21: i in dom G9 and

A22: j in dom G9 and

A23: i < j ; :: thesis: G9 . i < G9 . j

A24: dom G9 = (N \ {m}) \/ {m} by FUNCT_2:def 1;

now :: thesis: G9 . i < G9 . jend;

hence
G9 . i < G9 . j
; :: thesis: verumper cases
( ( i in N \ {m} & j in N \ {m} ) or ( i in N \ {m} & j in {m} ) or ( i in {m} & j in N \ {m} ) or ( i in {m} & j in {m} ) )
by A21, A22, A24, XBOOLE_0:def 3;

end;

suppose A25:
( i in N \ {m} & j in N \ {m} )
; :: thesis: G9 . i < G9 . j

then A26:
j in dom F
by FUNCT_2:def 1;

then A27: F . j = G9 . j by A13, FUNCT_1:47;

A28: i in dom F by A25, FUNCT_2:def 1;

then F . i = G9 . i by A13, FUNCT_1:47;

hence G9 . i < G9 . j by A9, A23, A28, A26, A27; :: thesis: verum

end;then A27: F . j = G9 . j by A13, FUNCT_1:47;

A28: i in dom F by A25, FUNCT_2:def 1;

then F . i = G9 . i by A13, FUNCT_1:47;

hence G9 . i < G9 . j by A9, A23, A28, A26, A27; :: thesis: verum

proof

for k being Nat holds S
set P = {} ;

A33: rng {} = {} ;

let N be finite Subset of NAT; :: thesis: ( card N = 0 implies ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) ) )

assume A34: card N = 0 ; :: thesis: ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) )

N is empty by A34;

then reconsider P = {} as Function of N,(Segm (card N)) by A33, FUNCT_2:1;

take P ; :: thesis: ( P is bijective & ( for n, k being Nat st n in dom P & k in dom P & n < k holds

P . n < P . k ) )

rng P = {} ;

then ( P is one-to-one & P is onto ) by A34, FUNCT_2:def 3;

hence P is bijective ; :: thesis: for n, k being Nat st n in dom P & k in dom P & n < k holds

P . n < P . k

thus for n, k being Nat st n in dom P & k in dom P & n < k holds

P . n < P . k ; :: thesis: verum

end;A33: rng {} = {} ;

let N be finite Subset of NAT; :: thesis: ( card N = 0 implies ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) ) )

assume A34: card N = 0 ; :: thesis: ex F being Function of N,(Segm (card N)) st

( F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds

F . n < F . k ) )

N is empty by A34;

then reconsider P = {} as Function of N,(Segm (card N)) by A33, FUNCT_2:1;

take P ; :: thesis: ( P is bijective & ( for n, k being Nat st n in dom P & k in dom P & n < k holds

P . n < P . k ) )

rng P = {} ;

then ( P is one-to-one & P is onto ) by A34, FUNCT_2:def 3;

hence P is bijective ; :: thesis: for n, k being Nat st n in dom P & k in dom P & n < k holds

P . n < P . k

thus for n, k being Nat st n in dom P & k in dom P & n < k holds

P . n < P . k ; :: thesis: verum

hence for N being finite Subset of NAT ex Order being Function of N,(Segm (card N)) st

( Order is bijective & ( for n, k being Nat st n in dom Order & k in dom Order & n < k holds

Order . n < Order . k ) ) ; :: thesis: verum