let N be with_zero set ; :: thesis:
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis:

hereby :: thesis:

assume A1: S is standard ; :: thesis:
let k be Nat; :: thesis:
k <= k + 1 by NAT_1:11;
then consider F being non empty FinSequence of NAT such that
A2: F /. 1 = k and
A3: F /. (len F) = k + 1 and
A4: for n being Nat st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S) by A1;
set F1 = F -| (k + 1);
set x = (k + 1) .. F;
A5: k + 1 in rng F by A3, FINSEQ_6:168;
then A6: len (F -| (k + 1)) = ((k + 1) .. F) - 1 by FINSEQ_4:34;
then A7: (len (F -| (k + 1))) + 1 = (k + 1) .. F ;
A8: (k + 1) .. F in dom F by A5, FINSEQ_4:20;
then A9: F /. ((len (F -| (k + 1))) + 1) = F . ((k + 1) .. F) by A6, PARTFUN1:def 6
.= k + 1 by A5, FINSEQ_4:19 ;
(k + 1) .. F <= len F by A8, FINSEQ_3:25;
then A10: len (F -| (k + 1)) < len F by A7, NAT_1:13;
1 <= len F by NAT_1:14;
then A11: 1 in dom F by FINSEQ_3:25;
then A12: F /. 1 = F . 1 by PARTFUN1:def 6;
A13: F . ((k + 1) .. F) = k + 1 by A5, FINSEQ_4:19;
A14: k <> k + 1 ;
then A15: len (F -| (k + 1)) <> 0 by A2, A13, A11, A6, PARTFUN1:def 6;
1 <= (k + 1) .. F by A8, FINSEQ_3:25;
then 1 < (k + 1) .. F by A2, A14, A13, A12, XXREAL_0:1;
then A16: 1 <= len (F -| (k + 1)) by A7, NAT_1:13;
reconsider F1 = F -| (k + 1) as non empty FinSequence of NAT by A15, A5, FINSEQ_4:41;
set m = F /. (len F1);
reconsider m = F /. (len F1) as Nat ;
A17: len F1 in dom F by A16, A10, FINSEQ_3:25;
A18: len F1 in dom F1 by A16, FINSEQ_3:25;
then A19: F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 6
.= F . (len F1) by A5, A18, FINSEQ_4:36
.= F /. (len F1) by A17, PARTFUN1:def 6 ;

A20: now :: thesis:

rng F1 misses {(k + 1)} by A5, FINSEQ_4:38;
then (rng F1) /\ {(k + 1)} = {} ;
then A21: ( not k + 1 in rng F1 or not k + 1 in {(k + 1)} ) by XBOOLE_0:def 4;
assume A22: m = k + 1 ; :: thesis:
A23: len F1 in dom F1 by A16, FINSEQ_3:25;
then F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 6;
hence contradiction by A19, A22, A21, A23, FUNCT_1:def 3, TARSKI:def 1; :: thesis:

end;

reconsider F2 = <*(F /. (len F1)),(F /. ((k + 1) .. F))*> as non empty FinSequence of NAT ;
A24: len F2 = 2 by FINSEQ_1:44;
then A25: 2 in dom F2 by FINSEQ_3:25;
then A26: F2 /. (len F2) = F2 . 2 by A24, PARTFUN1:def 6
.= F /. ((k + 1) .. F)
.= k + 1 by A13, A8, PARTFUN1:def 6 ;
A27: 1 in dom F2 by A24, FINSEQ_3:25;

A28: now :: thesis:

let n be 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 A29: n = 1 by NAT_1:25;
then A30: F2 /. n = F2 . 1 by A27, PARTFUN1:def 6
.= F /. (len F1) ;
F2 /. (n + 1) = F2 . 2 by A25, A29, PARTFUN1:def 6
.= F /. ((len F1) + 1) by A6 ;
hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A4, A16, A10, A30; :: thesis:

end;

A31: now :: thesis:

let n be Nat; :: thesis:
assume that
A32: 1 <= n and
A33: n < len F1 ; :: thesis:
A34: 1 <= n + 1 by A32, NAT_1:13;
A35: n + 1 <= len F1 by A33, NAT_1:13;
then n + 1 <= len F by A10, XXREAL_0:2;
then A36: n + 1 in dom F by A34, FINSEQ_3:25;
n <= len F by A10, A33, XXREAL_0:2;
then A37: n in dom F by A32, FINSEQ_3:25;
A38: n in dom F1 by A32, A33, FINSEQ_3:25;
then A39: F1 /. n = F1 . n by PARTFUN1:def 6
.= F . n by A5, A38, FINSEQ_4:36
.= F /. n by A37, PARTFUN1:def 6 ;
A40: n < len F by A10, A33, XXREAL_0:2;
A41: n + 1 in dom F1 by A34, A35, FINSEQ_3:25;
then F1 /. (n + 1) = F1 . (n + 1) by PARTFUN1:def 6
.= F . (n + 1) by A5, A41, FINSEQ_4:36
.= F /. (n + 1) by A36, PARTFUN1:def 6 ;
hence F1 /. (n + 1) in SUCC ((F1 /. n),S) by A4, A32, A39, A40; :: thesis:

end;

F2 /. 1 = F2 . 1 by A27, PARTFUN1:def 6
.= m ;
then A42: m <= k + 1 by A1, A26, A28;
A43: 1 in dom F1 by A16, FINSEQ_3:25;
then F1 /. 1 = F1 . 1 by PARTFUN1:def 6
.= F . 1 by A5, A43, FINSEQ_4:36
.= k by A2, A11, PARTFUN1:def 6 ;
then k <= m by A1, A19, A31;
then ( m = k or m = k + 1 ) by A42, NAT_1:9;
hence k + 1 in SUCC (k,S) by A4, A16, A10, A9, A20; :: thesis:
let j be Nat; :: thesis:
reconsider fk = k, fj = j as Element of NAT by ORDINAL1:def 12;
reconsider F = <*fk,fj*> as non empty FinSequence of NAT ;
A44: len F = 2 by FINSEQ_1:44;
then A45: 2 in dom F by FINSEQ_3:25;
A46: 1 in dom F by A44, FINSEQ_3:25;
then A47: F /. 1 = F . 1 by PARTFUN1:def 6
.= k ;
assume A48: j in SUCC (k,S) ; :: thesis:

A49: now :: thesis:

let n be 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 A50: n = 1 by NAT_1:25;
then A51: F /. n = F . 1 by A46, PARTFUN1:def 6
.= k ;
F /. (n + 1) = F . 2 by A45, A50, PARTFUN1:def 6
.= j ;
hence F /. (n + 1) in SUCC ((F /. n),S) by A48, A51; :: thesis:

end;

F /. (len F) = F . 2 by A44, A45, PARTFUN1:def 6
.= j ;
hence k <= j by A1, A47, A49; :: thesis:

end;

assume A52: for k being Nat holds
( k + 1 in SUCC (k,S) & ( for j being Nat st j in SUCC (k,S) holds
k <= j ) ) ; :: thesis:
thus S is standard :: thesis:

proof

let m, n be Nat; :: according to AMISTD_1:def 6 :: thesis:
thus ( m <= n implies ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for k being Nat st 1 <= k & k < len f holds
f /. (k + 1) in SUCC ((f /. k),S) ) ) ) :: thesis:

proof

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

per cases by A53, XXREAL_0:1;

suppose m = n ; :: thesis:

hence ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) by Lm2; :: thesis:

end;

suppose A54: m < n ; :: thesis:

thus ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) :: thesis:

proof

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

end;

given F being non empty FinSequence of NAT such that A67: F /. 1 = m and
A68: F /. (len F) = n and
A69: for n being Nat st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S) ; :: thesis:
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len F implies ex l being Nat st
( F /. $1 = l & m <= l ) );

A70: now :: thesis:

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

now :: thesis:

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

per cases ;

suppose k = 0 ; :: thesis:

hence ex l being Nat st
( F /. (k + 1) = l & m <= l ) by A67; :: thesis:

end;

suppose A73: k > 0 ; :: thesis:

set l1 = F /. (k + 1);
consider l being Nat such that
A74: F /. k = l and
A75: m <= l by A71, A72, A73, NAT_1:13, NAT_1:14;
reconsider l1 = F /. (k + 1) as Nat ;
k < len F by A72, NAT_1:13;
then F /. (k + 1) in SUCC ((F /. k),S) by A69, A73, NAT_1:14;
then l <= l1 by A52, A74;
hence ex l being Nat st
( F /. (k + 1) = l & m <= l ) by A75, XXREAL_0:2; :: thesis:

end;

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

end;

A76: 1 <= len F by NAT_1:14;
A77: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A77, A70);
then ex l being Nat st
( F /. (len F) = l & m <= l ) by A76;
hence m <= n by A68; :: thesis:

end;