defpred S₁[ 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 Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ) );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
let N be finite Subset of NAT; :: thesis: ( card N = k + 1 implies ex F being Function of N,(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,(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₂[ set ] means $1 in N;
ex x being set st x in N by A3, CARD_1:27, XBOOLE_0:def 1;
then A4: ex n being Nat st S₂[n] ;
consider m9 being Nat such that
A5: for n being Nat st n in N holds
n <= m9 by Th66;
A6: for n being Nat st S₂[n] holds
n <= m9 by A5;
consider m being Nat such that
A7: ( S₂[m] & ( for n being Nat st S₂[n] holds
n <= m ) ) from NAT_1:sch 6(A6, A4);
set Nm = N \ {m};
consider F being Function of (N \ {m}),(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, Th65;
A10: card (N \ {m}) = k by A3, A7, Th65;
then A11: (card (N \ {m})) \/ {k} = card N by A3, 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, Th67;
N = (N \ {m}) \/ {m} by A7, ZFMISC_1:116;
then reconsider G9 = G as Function of N,(card N) by A3, A10, AFINSQ_1:2;
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, Th68;
hence G9 is bijective by A11; :: 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 )

proof

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₂[i] by A16, XBOOLE_0:def 5;
then A18: i <= m by A7;
i in dom F by A16, FUNCT_2:def 1;
then A19: F . i = G9 . i by A13, FUNCT_1:47;
card (N \ {m}) = k by A3, A7, Th65;
hence ( i < m & G9 . i < k ) by A16, A19, A18, A17, NAT_1:44, XXREAL_0:1; :: thesis: verum

end;

let i, j be Nat; :: thesis: ( i in dom G9 & j in dom G9 & i < j implies G9 . i < G9 . j )
assume that
A20: i in dom G9 and
A21: j in dom G9 and
A22: i < j ; :: thesis: G9 . i < G9 . j
A23: dom G9 = (N \ {m}) \/ {m} by FUNCT_2:def 1;

now

per 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 A20, A21, A23, XBOOLE_0:def 3;

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

then A25: j in dom F by FUNCT_2:def 1;
then A26: F . j = G9 . j by A13, FUNCT_1:47;
A27: i in dom F by A24, FUNCT_2:def 1;
then F . i = G9 . i by A13, FUNCT_1:47;
hence G9 . i < G9 . j by A9, A22, A27, A25, A26; :: thesis: verum

end;

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

then G9 . i < k by A15;
hence G9 . i < G9 . j by A14, A28, TARSKI:def 1; :: thesis: verum

end;

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

then i = m by TARSKI:def 1;
hence G9 . i < G9 . j by A22, A15, A29; :: thesis: verum

end;

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

then i = m by TARSKI:def 1;
hence G9 . i < G9 . j by A22, A30, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence G9 . i < G9 . j ; :: thesis: verum

end;

end;

A31: S₁[ 0 ]

proof

set P = {} ;
A32: rng {} = {} ;
A33: dom {} = {} ;
let N be finite Subset of NAT; :: thesis: ( card N = 0 implies ex F being Function of N,(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,(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,(card N) by A34, A32, 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;

for k being Nat holds S₁[k] from NAT_1:sch 2(A31, A1);
hence for N being finite Subset of NAT ex Order being Function of N,(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