let N be non empty with_non-empty_elements set ; :: thesis:
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis:

hereby :: thesis:

assume A2: S is standard ; :: thesis:
let k be Element of NAT ; :: thesis:
k <= k + 1 by NAT_1:11;
then consider F being non empty FinSequence of NAT such that
A3: F /. 1 = k and
A4: F /. (len 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) by A2, Def10;
set F1 = F -| (k + 1);
set x = (k + 1) .. F;
A6: k + 1 in rng F by A4, REVROT_1:3;
then A7: len (F -| (k + 1)) = ((k + 1) .. F) - 1 by FINSEQ_4:46;
then A8: (len (F -| (k + 1))) + 1 = (k + 1) .. F ;
A9: (k + 1) .. F in dom F by A6, FINSEQ_4:30;
then A10: F /. ((len (F -| (k + 1))) + 1) = F . ((k + 1) .. F) by A7, PARTFUN1:def 8
.= k + 1 by A6, FINSEQ_4:29 ;
(k + 1) .. F <= len F by A9, FINSEQ_3:27;
then A11: len (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:27;
then A13: F /. 1 = F . 1 by PARTFUN1:def 8;
A14: F . ((k + 1) .. F) = k + 1 by A6, FINSEQ_4:29;
A16: k <> k + 1 ;
then B17: len (F -| (k + 1)) <> 0 by A3, A14, A12, A7, PARTFUN1:def 8;
1 <= (k + 1) .. F by A9, FINSEQ_3:27;
then 1 < (k + 1) .. F by A3, A16, A14, A13, XXREAL_0:1;
then A18: 1 <= len (F -| (k + 1)) by A8, NAT_1:13;
reconsider F1 = F -| (k + 1) as non empty FinSequence of NAT by B17, A6, FINSEQ_4:53;
set m = F /. (len F1);
reconsider m = F /. (len F1) as Element of NAT ;
A21: len F1 in dom F by A18, A11, FINSEQ_3:27;
A22: len F1 in dom F1 by A18, FINSEQ_3:27;
then A23: F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 8
.= F . (len F1) by A6, A22, FINSEQ_4:48
.= F /. (len F1) by A21, PARTFUN1:def 8 ;

A24: now

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

end;

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

A32: 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 A33: n = 1 by NAT_1:27;
then A34: F2 /. n = F2 . 1 by A31, PARTFUN1:def 8
.= F /. (len F1) by FINSEQ_1:61 ;
F2 /. (n + 1) = F2 . 2 by A29, A33, PARTFUN1:def 8
.= F /. ((len F1) + 1) by A7, FINSEQ_1:61 ;
hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A5, A18, A11, A34; :: thesis:

end;

A35: now

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:27;
n <= len F by A11, A37, XXREAL_0:2;
then A41: n in dom F by A36, FINSEQ_3:27;
A42: n in dom F1 by A36, A37, FINSEQ_3:27;
then A43: F1 /. n = F1 . n by PARTFUN1:def 8
.= F . n by A6, A42, FINSEQ_4:48
.= F /. n by A41, PARTFUN1:def 8 ;
A44: n < len F by A11, A37, XXREAL_0:2;
A45: n + 1 in dom F1 by A38, A39, FINSEQ_3:27;
then F1 /. (n + 1) = F1 . (n + 1) by PARTFUN1:def 8
.= F . (n + 1) by A6, A45, FINSEQ_4:48
.= F /. (n + 1) by A40, PARTFUN1:def 8 ;
hence F1 /. (n + 1) in SUCC ((F1 /. n),S) by A5, A36, A43, A44; :: thesis:

end;

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

A53: 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 A54: n = 1 by NAT_1:27;
then A55: F /. n = F . 1 by A50, PARTFUN1:def 8
.= k by FINSEQ_1:61 ;
F /. (n + 1) = F . 2 by A49, A54, PARTFUN1:def 8
.= j by FINSEQ_1:61 ;
hence F /. (n + 1) in SUCC ((F /. n),S) by A52, A55; :: thesis:

end;

F /. (len F) = F . 2 by A48, A49, PARTFUN1:def 8
.= j by FINSEQ_1:61 ;
hence k <= j by A2, A51, A53, Def10; :: thesis:

end;

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

proof

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

proof

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

per cases by A57, 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 Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) by LemRefle; :: thesis:

end;

suppose A58: m < n ; :: thesis:

thus ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Element of 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
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 ; :: thesis:
A61: 1 <= (n -' m) + 1 by NAT_1:11;
then A62: 1 in dom F by A59, FINSEQ_3:27;
hence F /. 1 = F . 1 by PARTFUN1:def 8
.= (m + 1) -' 1 by A60, A62
.= m by NAT_D:34 ;
:: thesis:
m + 1 <= n by A58, INT_1:20;
then 1 <= n - m by XREAL_1:21;
then 0 <= n - m by XXREAL_0:2;
then A63: n -' m = n - m by XREAL_0:def 2;
A64: len F in dom F by A59, A61, FINSEQ_3:27;
hence F /. (len F) = F . (len F) by PARTFUN1:def 8
.= (m + ((n -' m) + 1)) -' 1 by A59, A60, A64
.= ((m + (n -' m)) + 1) -' 1
.= 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:27;
then A68: F /. p = F . p by PARTFUN1:def 8
.= (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:27;
then F /. (p + 1) = F . (p + 1) by PARTFUN1:def 8
.= (m + (p + 1)) -' 1 by A60, A70
.= ((m + p) + 1) -' 1
.= ((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;

given F being non empty FinSequence of NAT such that A71: F /. 1 = m and
A72: F /. (len 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) ; :: thesis:
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= len F implies ex l being Element of NAT st
( F /. $1 = l & m <= l ) );

A74: now

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

now

assume that
1 <= k + 1 and
A76: 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) = l & m <= l ) by A71; :: thesis:

end;

suppose A77: k > 0 ; :: thesis:

set l1 = F /. (k + 1);
consider l being Element of NAT such that
A80: F /. k = l and
A81: m <= l by A75, A76, A77, NAT_1:13, NAT_1:14;
reconsider l1 = F /. (k + 1) as Element of NAT ;
k < len F by A76, NAT_1:13;
then F /. (k + 1) in SUCC ((F /. k),S) by A73, A77, NAT_1:14;
then l <= l1 by A56, A80;
hence ex l being Element of NAT st
( F /. (k + 1) = l & m <= l ) by A81, 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 Element of NAT holds S₁[k] from NAT_1:sch 1(A83, A74);
then ex l being Element of NAT st
( F /. (len F) = l & m <= l ) by A82;
hence m <= n by A72; :: thesis:

end;