defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[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 S2[ set ] means \$1 in N;
ex x being object st x in N by ;
then A4: ex n being Nat st S2[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 S2[n] holds
n <= m9 by A5;
consider m being Nat such that
A7: ( S2[m] & ( for n being Nat st S2[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 ;
N = (N \ {m}) \/ {m} by ;
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 )
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 ;
then A17: i <> m by TARSKI:def 1;
S2[i] by A16, XBOOLE_0:def 5;
then i <= m by A7;
hence i < m by ; :: thesis: G9 . i < k
A18: i in dom F by ;
then A19: F . i = G9 . i by ;
A20: F . i in card (N \ {m}) by ;
card (N \ {m}) = k by A3, A7, Th55;
hence G9 . i < k by ; :: 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
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 . j
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 ;
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 ;
A28: i in dom F by ;
then F . i = G9 . i by ;
hence G9 . i < G9 . j by A9, A23, A28, A26, A27; :: thesis: verum
end;
suppose A29: ( i in N \ {m} & j in {m} ) ; :: thesis: G9 . i < G9 . j
then G9 . i < k by A15;
hence G9 . i < G9 . j by ; :: thesis: verum
end;
suppose A30: ( 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 ; :: thesis: verum
end;
suppose A31: ( i in {m} & j in {m} ) ; :: thesis: G9 . i < G9 . j
then i = m by TARSKI:def 1;
hence G9 . i < G9 . j by ; :: thesis: verum
end;
end;
end;
hence G9 . i < G9 . j ; :: thesis: verum
end;
end;
A32: S1[ 0 ]
proof
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 ;
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 ;
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 S1[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