let N be with_zero set ; :: thesis:
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis:
let f be sequence of NAT; :: 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,S ) ; :: thesis:
let k be Element of NAT ; :: thesis:
k <= k + 1 by NAT_1:11;
then f . k <= f . (k + 1),S by A2;
then consider F being non empty FinSequence of NAT such that
A3: F /. 1 = f . k and
A4: F /. (len F) = f . (k + 1) and
A5: for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S) ;
set F1 = F -| (f . (k + 1));
set x = (f . (k + 1)) .. F;
A6: f . (k + 1) in rng F by A4, FINSEQ_6:168;
then A7: len (F -| (f . (k + 1))) = ((f . (k + 1)) .. F) - 1 by FINSEQ_4:34;
then A8: (len (F -| (f . (k + 1)))) + 1 = (f . (k + 1)) .. F ;
A9: (f . (k + 1)) .. F in dom F by A6, FINSEQ_4:20;
then A10: F /. ((len (F -| (f . (k + 1)))) + 1) = F . ((f . (k + 1)) .. F) by A7, PARTFUN1:def 6
.= f . (k + 1) by A6, FINSEQ_4:19 ;
(f . (k + 1)) .. F <= len F by A9, FINSEQ_3:25;
then A11: len (F -| (f . (k + 1))) < len F by A8, NAT_1:13;
1 <= len F by NAT_1:14;
then A12: 1 in dom F by FINSEQ_3:25;
then A13: F /. 1 = F . 1 by PARTFUN1:def 6;
A14: F . ((f . (k + 1)) .. F) = f . (k + 1) by A6, FINSEQ_4:19;
A15: dom f = NAT by FUNCT_2:def 1;
A16: f . k <> f . (k + 1)

assume not f . k <> f . (k + 1) ; :: thesis:
then 0 + k = k + 1 by A1, A15, FUNCT_1:def 4;
hence contradiction ; :: thesis:

end;

then A17: len (F -| (f . (k + 1))) <> 0 by A3, A14, A12, A7, PARTFUN1:def 6;
1 <= (f . (k + 1)) .. F by A9, FINSEQ_3:25;
then 1 < (f . (k + 1)) .. F by A3, A16, A14, A13, XXREAL_0:1;
then A18: 1 <= len (F -| (f . (k + 1))) by A8, NAT_1:13;
reconsider F1 = F -| (f . (k + 1)) as non empty FinSequence of NAT by A17, A6, FINSEQ_4:41;
rng f = NAT by A1, FUNCT_2:def 3;
then consider m being object such that
A19: m in dom f and
A20: f . m = F /. (len F1) by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A19;
A21: len F1 in dom F by A18, A11, FINSEQ_3:25;
A22: len F1 in dom F1 by A18, FINSEQ_3:25;
then A23: F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 6
.= F . (len F1) by A6, A22, FINSEQ_4:36
.= F /. (len F1) by A21, PARTFUN1:def 6 ;

A24: now :: thesis:

rng F1 misses {(f . (k + 1))} by A6, FINSEQ_4:38;
then (rng F1) /\ {(f . (k + 1))} = {} ;
then A25: ( not f . (k + 1) in rng F1 or not f . (k + 1) in {(f . (k + 1))} ) by XBOOLE_0:def 4;
assume A26: m = k + 1 ; :: thesis:
A27: len F1 in dom F1 by A18, FINSEQ_3:25;
then F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 6;
hence contradiction by A20, A23, A26, A25, A27, FUNCT_1:def 3, TARSKI:def 1; :: thesis:

end;

reconsider F2 = <*(F /. (len F1)),(F /. ((f . (k + 1)) .. F))*> as non empty FinSequence of NAT ;
A28: len F2 = 2 by FINSEQ_1:44;
then A29: 2 in dom F2 by FINSEQ_3:25;
then A30: F2 /. (len F2) = F2 . 2 by A28, PARTFUN1:def 6
.= F /. ((f . (k + 1)) .. F)
.= f . (k + 1) by A14, A9, PARTFUN1:def 6 ;
A31: 1 in dom F2 by A28, FINSEQ_3:25;

A32: now :: thesis:

let n be Element of NAT ; :: thesis:
assume ( 1 <= n & n < len F2 ) ; :: thesis:
then ( n <> 0 & n < 1 + 1 ) by FINSEQ_1:44;
then ( n <> 0 & n <= 1 ) by NAT_1:13;
then A33: n = 1 by NAT_1:25;
then A34: F2 /. n = F2 . 1 by A31, PARTFUN1:def 6
.= F /. (len F1) ;
F2 /. (n + 1) = F2 . 2 by A29, A33, PARTFUN1:def 6
.= F /. ((len F1) + 1) by A7 ;
hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A5, A18, A11, A34; :: thesis:

end;

A35: now :: thesis:

let n be Element of NAT ; :: thesis:
assume that
A36: 1 <= n and
A37: n < len F1 ; :: thesis:
A38: 1 <= n + 1 by A36, NAT_1:13;
A39: n + 1 <= len F1 by A37, NAT_1:13;
then n + 1 <= len F by A11, XXREAL_0:2;
then A40: n + 1 in dom F by A38, FINSEQ_3:25;
n <= len F by A11, A37, XXREAL_0:2;
then A41: n in dom F by A36, FINSEQ_3:25;
A42: n in dom F1 by A36, A37, FINSEQ_3:25;
then A43: F1 /. n = F1 . n by PARTFUN1:def 6
.= F . n by A6, A42, FINSEQ_4:36
.= F /. n by A41, PARTFUN1:def 6 ;
A44: n < len F by A11, A37, XXREAL_0:2;
A45: n + 1 in dom F1 by A38, A39, FINSEQ_3:25;
then F1 /. (n + 1) = F1 . (n + 1) by PARTFUN1:def 6
.= F . (n + 1) by A6, A45, FINSEQ_4:36
.= F /. (n + 1) by A40, PARTFUN1:def 6 ;
hence F1 /. (n + 1) in SUCC ((F1 /. n),S) by A5, A36, A43, A44; :: thesis:

end;

F2 /. 1 = F2 . 1 by A31, PARTFUN1:def 6
.= f . m by A20 ;
then f . m <= f . (k + 1),S by A30, A32;
then A46: m <= k + 1 by A2;
A47: 1 in dom F1 by A18, FINSEQ_3:25;
then F1 /. 1 = F1 . 1 by PARTFUN1:def 6
.= F . 1 by A6, A47, FINSEQ_4:36
.= f . k by A3, A12, PARTFUN1:def 6 ;
then f . k <= f . m,S by A20, A23, A35;
then k <= m by A2;
then ( m = k or m = k + 1 ) by A46, NAT_1:9;
hence f . (k + 1) in SUCC ((f . k),S) by A5, A18, A11, A10, A20, A24; :: thesis:
let j be Element of NAT ; :: thesis:
reconsider fk = f . k, fj = f . j as Element of NAT ;
reconsider F = <*fk,fj*> as non empty FinSequence of NAT ;
A48: len F = 2 by FINSEQ_1:44;
then A49: 2 in dom F by FINSEQ_3:25;
A50: 1 in dom F by A48, FINSEQ_3:25;
then A51: F /. 1 = F . 1 by PARTFUN1:def 6
.= f . k ;
assume A52: f . j in SUCC ((f . k),S) ; :: thesis:

A53: now :: thesis:

let n be Element of NAT ; :: thesis:
assume ( 1 <= n & n < len F ) ; :: thesis:
then ( n <> 0 & n < 1 + 1 ) by FINSEQ_1:44;
then ( n <> 0 & n <= 1 ) by NAT_1:13;
then A54: n = 1 by NAT_1:25;
then A55: F /. n = F . 1 by A50, PARTFUN1:def 6
.= f . k ;
F /. (n + 1) = F . 2 by A49, A54, PARTFUN1:def 6
.= f . j ;
hence F /. (n + 1) in SUCC ((F /. n),S) by A52, A55; :: thesis:

end;

F /. (len F) = F . 2 by A48, A49, PARTFUN1:def 6
.= f . j ;
then f . k <= f . j,S by A51, A53;
hence k <= j by A2; :: thesis:

end;

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

hereby :: thesis:

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

per cases by A57, XXREAL_0:1;

suppose m = n ; :: thesis:

hence f . m <= f . n,S by Lm1; :: thesis:

end;

suppose A58: m < n ; :: thesis:

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

proof

reconsider f9 = f as sequence of NAT ;
set mn = n -' m;
deffunc H₁( Nat) -> Element of NAT = f9 . ((m + $1) -' 1);
consider F being FinSequence of NAT such that
A59: len F = (n -' m) + 1 and
A60: 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 FinSequence of NAT by A59;
take F ; :: according to AMI_WSTD:def 1 :: thesis:
A61: 1 <= (n -' m) + 1 by NAT_1:11;
then A62: 1 in dom F by A59, FINSEQ_3:25;
hence F /. 1 = F . 1 by PARTFUN1:def 6
.= f . ((m + 1) -' 1) by A60, A62
.= f . m by NAT_D:34 ;
:: thesis:
m + 1 <= n by A58, INT_1:7;
then 1 <= n - m by XREAL_1:19;
then 0 <= n - m ;
then A63: n -' m = n - m by XREAL_0:def 2;
A64: len F in dom F by A59, A61, FINSEQ_3:25;
hence F /. (len F) = F . (len F) by PARTFUN1:def 6
.= f . ((m + ((n -' m) + 1)) -' 1) by A59, A60, A64
.= f . (((m + (n -' m)) + 1) -' 1)
.= f . n by A63, NAT_D:34 ;
:: thesis:
let p be Element of NAT ; :: thesis:
assume that
A65: 1 <= p and
A66: p < len F ; :: thesis:
A67: p in dom F by A65, A66, FINSEQ_3:25;
then A68: F /. p = F . p by PARTFUN1:def 6
.= f . ((m + p) -' 1) by A60, A67 ;
A69: p <= m + p by NAT_1:11;
( 1 <= p + 1 & p + 1 <= len F ) by A65, A66, NAT_1:13;
then A70: p + 1 in dom F by FINSEQ_3:25;
then F /. (p + 1) = F . (p + 1) by PARTFUN1:def 6
.= f . ((m + (p + 1)) -' 1) by A60, A70
.= f . (((m + p) + 1) -' 1)
.= f . (((m + p) -' 1) + 1) by A65, A69, NAT_D:38, XXREAL_0:2 ;
hence F /. (p + 1) in SUCC ((F /. p),S) by A56, A68; :: thesis:

end;

assume f . m <= f . n,S ; :: thesis:
then consider F being non empty FinSequence of NAT such that
A71: F /. 1 = f . m and
A72: F /. (len F) = f . n and
A73: for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S) ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len F implies ex l being Element of NAT st
( F /. $1 = f . l & m <= l ) );

A74: now :: thesis:

let k be Nat; :: thesis:
assume A75: S₁[k] ; :: thesis:

now :: thesis:

assume that
1 <= k + 1 and
A76: k + 1 <= len F ; :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

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

end;

suppose A77: k > 0 ; :: thesis:

rng f = NAT by A1, FUNCT_2:def 3;
then consider l1 being object such that
A78: l1 in dom f and
A79: f . l1 = F /. (k + 1) by FUNCT_1:def 3;
consider l being Element of NAT such that
A80: F /. k = f . l and
A81: m <= l by A75, A76, A77, NAT_1:13, NAT_1:14;
reconsider l1 = l1 as Element of NAT by A78;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
k < len F by A76, NAT_1:13;
then F /. (kk + 1) in SUCC ((F /. kk),S) by A73, A77, NAT_1:14;
then l <= l1 by A56, A80, A79;
hence ex l being Element of NAT st
( F /. (k + 1) = f . l & m <= l ) by A81, A79, XXREAL_0:2; :: thesis:

end;

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

end;

A82: 1 <= len F by NAT_1:14;
A83: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A83, A74);
then ( dom f = NAT & ex l being Element of NAT st
( F /. (len F) = f . l & m <= l ) ) by A82, FUNCT_2:def 1;
hence m <= n by A1, A72, FUNCT_1:def 4; :: thesis: