let N be with_non-empty_elements set ; :: thesis:
let IL be non empty set ; :: thesis:
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis:
let f be IL-Function of NAT ,S; :: thesis:
assume A1: f is bijective ; :: thesis:

hereby :: thesis:

assume A2: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ; :: thesis:
let k be Element of NAT ; :: thesis:
k <= k + 1 by NAT_1:11;
then f . k <= f . (k + 1) by A2;
then consider F being non empty IL-FinSequence of S such that
A3: ( F /. 1 = f . k & F /. (len F) = f . (k + 1) ) and
A4: for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC (F /. n) by Def8;
A5: 1 <= len F by NAT_1:14;
A6: ( f is one-to-one & f is onto ) by A1;
A7: dom f = NAT by FUNCT_2:def 1;
A8: f . k <> f . (k + 1)

proof

assume not f . k <> f . (k + 1) ; :: thesis:
then 0 + k = k + 1 by A6, A7, FUNCT_1:def 8;
hence contradiction ; :: thesis:

end;

A9: f . (k + 1) in rng F by A3, REVROT_1:3;
set x = (f . (k + 1)) .. F;
A10: F . ((f . (k + 1)) .. F) = f . (k + 1) by A9, FINSEQ_4:29;
A11: (f . (k + 1)) .. F in dom F by A9, FINSEQ_4:30;
then A12: ( 1 <= (f . (k + 1)) .. F & (f . (k + 1)) .. F <= len F ) by FINSEQ_3:27;
A13: 1 in dom F by A5, FINSEQ_3:27;
then F /. 1 = F . 1 by PARTFUN1:def 8;
then A14: 1 < (f . (k + 1)) .. F by A3, A8, A10, A12, XXREAL_0:1;
set F1 = F -| (f . (k + 1));
A15: len (F -| (f . (k + 1))) = ((f . (k + 1)) .. F) - 1 by A9, FINSEQ_4:46;
then (len (F -| (f . (k + 1)))) + 1 = (f . (k + 1)) .. F ;
then A16: ( 1 <= len (F -| (f . (k + 1))) & len (F -| (f . (k + 1))) < len F ) by A12, A14, NAT_1:13;
A17: F /. ((len (F -| (f . (k + 1)))) + 1) = F . ((f . (k + 1)) .. F) by A11, A15, PARTFUN1:def 8
.= f . (k + 1) by A9, FINSEQ_4:29 ;
len (F -| (f . (k + 1))) <> 0 by A3, A8, A10, A13, A15, PARTFUN1:def 8;
then F -| (f . (k + 1)) is non empty FinSequence of IL by A9, FINSEQ_4:53;
then reconsider F1 = F -| (f . (k + 1)) as non empty IL-FinSequence of S by AMI_1:def 34;
rng f = IL by A6, FUNCT_2:def 3;
then consider m being set such that
A18: ( m in dom f & f . m = F /. (len F1) ) by FUNCT_1:def 5;
reconsider m = m as Element of NAT by A18;
A19: 1 in dom F1 by A16, FINSEQ_3:27;
then A20: F1 /. 1 = F1 . 1 by PARTFUN1:def 8
.= F . 1 by A9, A19, FINSEQ_4:48
.= f . k by A3, A13, PARTFUN1:def 8 ;
A21: len F1 in dom F by A16, FINSEQ_3:27;
A22: len F1 in dom F1 by A16, FINSEQ_3:27;
then A23: F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 8
.= F . (len F1) by A9, A22, FINSEQ_4:48
.= F /. (len F1) by A21, PARTFUN1:def 8 ;

now

let n be Element of NAT ; :: thesis:
assume A24: ( 1 <= n & n < len F1 ) ; :: thesis:
then A25: n in dom F1 by FINSEQ_3:27;
A26: ( 1 <= n + 1 & n + 1 <= len F1 ) by A24, NAT_1:13;
then A27: n + 1 in dom F1 by FINSEQ_3:27;
n <= len F by A16, A24, XXREAL_0:2;
then A28: n in dom F by A24, FINSEQ_3:27;
n + 1 <= len F by A16, A26, XXREAL_0:2;
then A29: n + 1 in dom F by A26, FINSEQ_3:27;
A30: F1 /. (n + 1) = F1 . (n + 1) by A27, PARTFUN1:def 8
.= F . (n + 1) by A9, A27, FINSEQ_4:48
.= F /. (n + 1) by A29, PARTFUN1:def 8 ;
A31: F1 /. n = F1 . n by A25, PARTFUN1:def 8
.= F . n by A9, A25, FINSEQ_4:48
.= F /. n by A28, PARTFUN1:def 8 ;
n < len F by A16, A24, XXREAL_0:2;
hence F1 /. (n + 1) in SUCC (F1 /. n) by A4, A24, A30, A31; :: thesis:

end;

then A32: f . k <= f . m by A18, A20, A23, Def8;
reconsider F2 = <*(F /. (len F1)),(F /. ((f . (k + 1)) .. F))*> as non empty IL-FinSequence of S ;
A33: len F2 = 2 by FINSEQ_1:61;
then A34: ( 1 in dom F2 & 2 in dom F2 ) by FINSEQ_3:27;
then A35: F2 /. 1 = F2 . 1 by PARTFUN1:def 8
.= f . m by A18, FINSEQ_1:61 ;
A36: F2 /. (len F2) = F2 . 2 by A33, A34, PARTFUN1:def 8
.= F /. ((f . (k + 1)) .. F) by FINSEQ_1:61
.= f . (k + 1) by A10, A11, PARTFUN1:def 8 ;

now

let n be Element of NAT ; :: thesis:
assume ( 1 <= n & n < len F2 ) ; :: thesis:
then ( n <> 0 & n < 2 ) by FINSEQ_1:61;
then A37: n = 1 by NAT_1:27;
then A38: F2 /. (n + 1) = F2 . 2 by A34, PARTFUN1:def 8
.= F /. ((len F1) + 1) by A15, FINSEQ_1:61 ;
F2 /. n = F2 . 1 by A34, A37, PARTFUN1:def 8
.= F /. (len F1) by FINSEQ_1:61 ;
hence F2 /. (n + 1) in SUCC (F2 /. n) by A4, A16, A38; :: thesis:

end;

then f . m <= f . (k + 1) by A35, A36, Def8;
then ( k <= m & m <= k + 1 ) by A2, A32;
then A39: ( m = k or m = k + 1 ) by NAT_1:9;

now

assume A40: m = k + 1 ; :: thesis:
rng F1 misses {(f . (k + 1))} by A9, FINSEQ_4:50;
then (rng F1) /\ {(f . (k + 1))} = {} by XBOOLE_0:def 7;
then A41: ( not f . (k + 1) in rng F1 or not f . (k + 1) in {(f . (k + 1))} ) by XBOOLE_0:def 4;
A42: len F1 in dom F1 by A16, FINSEQ_3:27;
then F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 8;
hence contradiction by A18, A23, A40, A41, A42, FUNCT_1:def 5, TARSKI:def 1; :: thesis:

end;

hence f . (k + 1) in SUCC (f . k) by A4, A16, A17, A18, A39; :: thesis:
let j be Element of NAT ; :: thesis:
assume A43: f . j in SUCC (f . k) ; :: thesis:
reconsider F = <*(f . k),(f . j)*> as non empty IL-FinSequence of S ;
A44: len F = 2 by FINSEQ_1:61;
then A45: ( 1 in dom F & 2 in dom F ) by FINSEQ_3:27;
then A46: F /. 1 = F . 1 by PARTFUN1:def 8
.= f . k by FINSEQ_1:61 ;
A47: F /. (len F) = F . 2 by A44, A45, PARTFUN1:def 8
.= f . j by FINSEQ_1:61 ;

now

let n be Element of NAT ; :: thesis:
assume ( 1 <= n & n < len F ) ; :: thesis:
then ( n <> 0 & n < 2 ) by FINSEQ_1:61;
then A48: n = 1 by NAT_1:27;
then A49: F /. (n + 1) = F . 2 by A45, PARTFUN1:def 8
.= f . j by FINSEQ_1:61 ;
F /. n = F . 1 by A45, A48, PARTFUN1:def 8
.= f . k by FINSEQ_1:61 ;
hence F /. (n + 1) in SUCC (F /. n) by A43, A49; :: thesis:

end;

then f . k <= f . j by A46, A47, Def8;
hence k <= j by A2; :: thesis:

end;

assume A50: for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ; :: thesis:
let m, n be Element of NAT ; :: thesis:

hereby :: thesis:

assume A51: m <= n ; :: thesis:

per cases by A51, XXREAL_0:1;

suppose m = n ; :: thesis:

hence f . m <= f . n ; :: thesis:

end;

suppose A52: m < n ; :: thesis:

thus f . m <= f . n :: thesis:

proof

set mn = n -' m;
reconsider f' = f as Function of NAT ,IL ;
deffunc H₁( Nat) -> Element of IL = f' . ((m + $1) -' 1);
consider F being FinSequence of IL such that
A53: len F = (n -' m) + 1 and
A54: for j being Nat st j in dom F holds
F . j = H₁(j) from FINSEQ_2:sch 1();
reconsider F = F as non empty IL-FinSequence of S by A53, AMI_1:def 34;
take F ; :: according to AMISTD_1:def 8 :: thesis:
m + 1 <= n by A52, INT_1:20;
then 1 <= n - m by XREAL_1:21;
then 0 <= n - m by XXREAL_0:2;
then A55: n -' m = n - m by XREAL_0:def 2;
1 <= (n -' m) + 1 by NAT_1:11;
then A56: ( 1 in dom F & len F in dom F ) by A53, FINSEQ_3:27;
thus F /. 1 = F . 1 by A56, PARTFUN1:def 8
.= f . ((m + 1) -' 1) by A54, A56
.= f . m by NAT_D:34 ; :: thesis:
thus F /. (len F) = F . (len F) by A56, PARTFUN1:def 8
.= f . ((m + ((n -' m) + 1)) -' 1) by A53, A54, A56
.= f . (((m + (n -' m)) + 1) -' 1)
.= f . n by A55, NAT_D:34 ; :: thesis:
let p be Element of NAT ; :: thesis:
assume A58: ( 1 <= p & p < len F ) ; :: thesis:
then ( 1 <= p + 1 & p + 1 <= len F ) by NAT_1:13;
then A59: ( p in dom F & p + 1 in dom F ) by A58, FINSEQ_3:27;
A61: p <= m + p by NAT_1:11;
A62: F /. (p + 1) = F . (p + 1) by A59, PARTFUN1:def 8
.= f . ((m + (p + 1)) -' 1) by A54, A59
.= f . (((m + p) + 1) -' 1)
.= f . (((m + p) -' 1) + 1) by A58, A61, NAT_D:38, XXREAL_0:2 ;
F /. p = F . p by A59, PARTFUN1:def 8
.= f . ((m + p) -' 1) by A54, A59 ;
hence F /. (p + 1) in SUCC (F /. p) by A50, A62; :: thesis:

end;

assume A63: f . m <= f . n ; :: thesis:
A64: ( f is one-to-one & f is onto ) by A1;
A65: dom f = NAT by FUNCT_2:def 1;
consider F being non empty IL-FinSequence of S such that
A66: ( F /. 1 = f . m & F /. (len F) = f . n ) and
A67: for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC (F /. n) by A63, Def8;
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= len F implies ex l being Element of NAT st
( F /. $1 = f . l & m <= l ) );
A68: S₁[ 0 ] ;

A69: now

let k be Element of NAT ; :: thesis:
assume A70: S₁[k] ; :: thesis:

now

assume A71: ( 1 <= k + 1 & k + 1 <= len F ) ; :: thesis:

per cases by NAT_1:3;

suppose k = 0 ; :: thesis:

hence ex l being Element of NAT st
( F /. (k + 1) = f . l & m <= l ) by A66; :: thesis:

end;

suppose A72: k > 0 ; :: thesis:

k < len F by A71, NAT_1:13;
then A73: F /. (k + 1) in SUCC (F /. k) by A67, A72, NAT_1:14;
consider l being Element of NAT such that
A74: ( F /. k = f . l & m <= l ) by A70, A71, A72, NAT_1:13, NAT_1:14;
rng f = IL by A64, FUNCT_2:def 3;
then consider l1 being set such that
A75: ( l1 in dom f & f . l1 = F /. (k + 1) ) by FUNCT_1:def 5;
reconsider l1 = l1 as Element of NAT by A75;
l <= l1 by A50, A73, A74, A75;
hence ex l being Element of NAT st
( F /. (k + 1) = f . l & m <= l ) by A74, A75, XXREAL_0:2; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A76: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A68, A69);
1 <= len F by NAT_1:14;
then ex l being Element of NAT st
( F /. (len F) = f . l & m <= l ) by A76;
hence m <= n by A64, A65, A66, FUNCT_1:def 8; :: thesis: