defpred S₁[ Element of NAT ] means for N being finite Subset of NAT st card N = $1 holds
ex F being Function of N,(card N) st
( 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 ) );
A1: S₁[ 0 ]

proof

let N be finite Subset of NAT ; :: thesis:
assume A2: card N = 0 ; :: thesis:
set P = {} ;
( rng {} = {} & dom {} = {} & N is empty ) by A2;
then reconsider P = {} as Function of N,(card N) by A2, FUNCT_2:3;
take P ; :: thesis:
( dom P = {} & rng P = {} ) ;
then ( P is one-to-one & P is onto ) by A2, FUNCT_2:def 3;
hence P is bijective ; :: thesis:
thus for n, k being Element of NAT st n in dom P & k in dom P & n < k holds
P . n < P . k ; :: thesis:

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A4: S₁[k] ; :: thesis:
let N be finite Subset of NAT ; :: thesis:
assume A5: card N = k + 1 ; :: thesis:
defpred S₂[ set ] means $1 in N;
consider m' being Element of NAT such that
A6: for n being Element of NAT st n in N holds
n <= m' by Th66;
A7: for n being Nat st S₂[n] holds
n <= m' by A6;
consider x being set such that
A8: x in N by A5, CARD_1:47, XBOOLE_0:def 1;
A9: ex n being Nat st S₂[n] by A8;
consider m being Nat such that
A10: ( S₂[m] & ( for n being Nat st S₂[n] holds
n <= m ) ) from NAT_1:sch 6(A7, A9);
set Nm = N \ {m};
consider F being Function of (N \ {m}),(card (N \ {m})) such that
A11: F is bijective and
A12: for n, k being Element of NAT st n in dom F & k in dom F & n < k holds
F . n < F . k by A4, A5, A10, Th65;
m in {m} by TARSKI:def 1;
then A13: ( not m in N \ {m} & ( card (N \ {m}) is empty implies N \ {m} is empty ) ) by XBOOLE_0:def 5;
then consider G being Function of ((N \ {m}) \/ {m}),((card (N \ {m})) \/ {k}) such that
A14: ( G | (N \ {m}) = F & G . m = k ) by Th67;
card (N \ {m}) = k by A5, A10, Th65;
then ( F is one-to-one & F is onto & not k in card (N \ {m}) & (card (N \ {m})) \/ {k} = k + 1 ) by A11, AFINSQ_1:4;
then A15: ( G is one-to-one & G is onto & N = (N \ {m}) \/ {m} & (card (N \ {m})) \/ {k} = card N ) by A5, A10, A13, A14, Th68, ZFMISC_1:140;
then reconsider G' = G as Function of N,(card N) ;
take G' ; :: thesis:
thus G' is bijective by A15; :: thesis:
thus for n, k being Element of NAT st n in dom G' & k in dom G' & n < k holds
G' . n < G' . k :: thesis:

proof

let i, j be Element of NAT ; :: thesis:
assume A16: ( i in dom G' & j in dom G' & i < j ) ; :: thesis:
A17: for i being Element of NAT st i in N \ {m} holds
( i < m & G' . i < k )

proof

let i be Element of NAT ; :: thesis:
assume A18: i in N \ {m} ; :: thesis:
i in dom F by A18, FUNCT_2:def 1;
then ( S₂[i] & not i in {m} & F . i = G' . i & F . i in rng F & card (N \ {m}) = k ) by A5, A10, A14, Th65, FUNCT_1:70, FUNCT_1:def 5, XBOOLE_0:def 5;
then ( i <= m & i <> m & G' . i in k ) by A10, TARSKI:def 1;
hence ( i < m & G' . i < k ) by NAT_1:45, XXREAL_0:1; :: thesis:

end;

A19: dom G' = (N \ {m}) \/ {m} by FUNCT_2:def 1;

now

per cases by A16, A19, XBOOLE_0:def 3;

suppose A20: ( i in N \ {m} & j in N \ {m} ) ; :: thesis:

A21: ( i in dom F & j in dom F ) by A20, FUNCT_2:def 1;
then ( F . i = G' . i & F . j = G' . j ) by A14, FUNCT_1:70;
hence G' . i < G' . j by A12, A16, A21; :: thesis:

end;

suppose ( i in N \ {m} & j in {m} ) ; :: thesis:

then ( G' . i < k & G' . j = k ) by A14, A17, TARSKI:def 1;
hence G' . i < G' . j ; :: thesis:

end;

suppose ( i in {m} & j in N \ {m} ) ; :: thesis:

then ( i = m & j < m ) by A17, TARSKI:def 1;
hence G' . i < G' . j by A16; :: thesis:

end;

suppose ( i in {m} & j in {m} ) ; :: thesis:

then ( i = m & j = m ) by TARSKI:def 1;
hence G' . i < G' . j by A16; :: thesis:

end;

hence G' . i < G' . j ; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A3);
hence for N being finite Subset of NAT ex Order being Function of N,(card N) st
( Order is bijective & ( for n, k being Element of NAT st n in dom Order & k in dom Order & n < k holds
Order . n < Order . k ) ) ; :: thesis: