let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds
( S is standard iff for k being Nat holds
( k + 1 in SUCC (k,S) & ( for j being Nat st j in SUCC (k,S) holds
k <= j ) ) )

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: ( S is standard iff for k being Nat holds
( k + 1 in SUCC (k,S) & ( for j being Nat st j in SUCC (k,S) holds
k <= j ) ) )

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

let k be Nat; :: thesis: ( k + 1 in SUCC (k,S) & ( for j being Nat st j in SUCC (k,S) holds
k <= j ) )

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 ;
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 ;
then A9: F /. ((len (F -| (k + 1))) + 1) = F . ((k + 1) .. F) by
.= k + 1 by ;
(k + 1) .. F <= len F by ;
then A10: len (F -| (k + 1)) < len F by ;
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 ;
A14: k <> k + 1 ;
then A15: len (F -| (k + 1)) <> 0 by ;
1 <= (k + 1) .. F by ;
then 1 < (k + 1) .. F by ;
then A16: 1 <= len (F -| (k + 1)) by ;
reconsider F1 = F -| (k + 1) as non empty FinSequence of NAT by ;
set m = F /. (len F1);
reconsider m = F /. (len F1) as Nat ;
A17: len F1 in dom F by ;
A18: len F1 in dom F1 by ;
then A19: F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def 6
.= F . (len F1) by
.= F /. (len F1) by ;
A20: now :: thesis: not m = k + 1
rng F1 misses {(k + 1)} by ;
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: contradiction
A23: len F1 in dom F1 by ;
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: verum
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
.= F /. ((k + 1) .. F) by FINSEQ_1:44
.= k + 1 by ;
A27: 1 in dom F2 by ;
A28: now :: thesis: for n being Nat st 1 <= n & n < len F2 holds
F2 /. (n + 1) in SUCC ((F2 /. n),S)
let n be Nat; :: thesis: ( 1 <= n & n < len F2 implies F2 /. (n + 1) in SUCC ((F2 /. n),S) )
assume ( 1 <= n & n < len F2 ) ; :: thesis: F2 /. (n + 1) in SUCC ((F2 /. n),S)
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
.= F /. (len F1) by FINSEQ_1:44 ;
F2 /. (n + 1) = F2 . 2 by
.= F /. ((len F1) + 1) by ;
hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A4, A16, A10, A30; :: thesis: verum
end;
A31: now :: thesis: for n being Nat st 1 <= n & n < len F1 holds
F1 /. (n + 1) in SUCC ((F1 /. n),S)
let n be Nat; :: thesis: ( 1 <= n & n < len F1 implies F1 /. (n + 1) in SUCC ((F1 /. n),S) )
assume that
A32: 1 <= n and
A33: n < len F1 ; :: thesis: F1 /. (n + 1) in SUCC ((F1 /. n),S)
A34: 1 <= n + 1 by ;
A35: n + 1 <= len F1 by ;
then n + 1 <= len F by ;
then A36: n + 1 in dom F by ;
n <= len F by ;
then A37: n in dom F by ;
A38: n in dom F1 by ;
then A39: F1 /. n = F1 . n by PARTFUN1:def 6
.= F . n by
.= F /. n by ;
A40: n < len F by ;
A41: n + 1 in dom F1 by ;
then F1 /. (n + 1) = F1 . (n + 1) by PARTFUN1:def 6
.= F . (n + 1) by
.= F /. (n + 1) by ;
hence F1 /. (n + 1) in SUCC ((F1 /. n),S) by A4, A32, A39, A40; :: thesis: verum
end;
F2 /. 1 = F2 . 1 by
.= m by FINSEQ_1:44 ;
then A42: m <= k + 1 by A1, A26, A28;
A43: 1 in dom F1 by ;
then F1 /. 1 = F1 . 1 by PARTFUN1:def 6
.= F . 1 by
.= k by ;
then k <= m by A1, A19, A31;
then ( m = k or m = k + 1 ) by ;
hence k + 1 in SUCC (k,S) by A4, A16, A10, A9, A20; :: thesis: for j being Nat st j in SUCC (k,S) holds
k <= j

let j be Nat; :: thesis: ( j in SUCC (k,S) implies k <= j )
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 ;
then A47: F /. 1 = F . 1 by PARTFUN1:def 6
.= k by FINSEQ_1:44 ;
assume A48: j in SUCC (k,S) ; :: thesis: k <= j
A49: now :: thesis: for n being Nat st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S)
let n be Nat; :: thesis: ( 1 <= n & n < len F implies F /. (n + 1) in SUCC ((F /. n),S) )
assume ( 1 <= n & n < len F ) ; :: thesis: F /. (n + 1) in SUCC ((F /. n),S)
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
.= k by FINSEQ_1:44 ;
F /. (n + 1) = F . 2 by
.= j by FINSEQ_1:44 ;
hence F /. (n + 1) in SUCC ((F /. n),S) by ; :: thesis: verum
end;
F /. (len F) = F . 2 by
.= j by FINSEQ_1:44 ;
hence k <= j by A1, A47, A49; :: thesis: verum
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: S is standard
thus S is standard :: thesis: verum
proof
let m, n be Nat; :: according to AMISTD_1:def 6 :: thesis: ( m <= n iff 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) ) ) )

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: ( 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) ) ) implies m <= n )
proof
assume A53: m <= n ; :: thesis: 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) ) )

per cases ( m = n or m < n ) by ;
suppose m = n ; :: thesis: 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) ) )

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: verum
end;
suppose A54: m < n ; :: thesis: 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) ) )

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: verum
proof
set mn = n -' m;
deffunc H1( 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 = H1(j) from reconsider F = F as non empty FinSequence of NAT by A55;
take F ; :: thesis: ( 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) ) )

A57: 1 <= (n -' m) + 1 by NAT_1:11;
then A58: 1 in dom F by ;
hence F /. 1 = F . 1 by PARTFUN1:def 6
.= (m + 1) -' 1 by
.= m by NAT_D:34 ;
:: thesis: ( F /. (len F) = n & ( for n being Nat st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S) ) )

m + 1 <= n by ;
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 ;
hence F /. (len F) = F . (len F) by PARTFUN1:def 6
.= (m + ((n -' m) + 1)) -' 1 by
.= ((m + (n -' m)) + 1) -' 1
.= n by ;
:: thesis: for n being Nat st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S)

let p be Nat; :: thesis: ( 1 <= p & p < len F implies F /. (p + 1) in SUCC ((F /. p),S) )
assume that
A61: 1 <= p and
A62: p < len F ; :: thesis: F /. (p + 1) in SUCC ((F /. p),S)
A63: p in dom F by ;
then A64: F /. p = F . p by PARTFUN1:def 6
.= (m + p) -' 1 by ;
A65: p <= m + p by NAT_1:11;
( 1 <= p + 1 & p + 1 <= len F ) by ;
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
.= ((m + p) + 1) -' 1
.= ((m + p) -' 1) + 1 by ;
hence F /. (p + 1) in SUCC ((F /. p),S) by ; :: thesis: verum
end;
end;
end;
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: m <= n
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len F implies ex l being Nat st
( F /. \$1 = l & m <= l ) );
A70: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A71: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( 1 <= k + 1 & k + 1 <= len F implies ex l being Nat st
( F /. (k + 1) = l & m <= l ) )
assume that
1 <= k + 1 and
A72: k + 1 <= len F ; :: thesis: ex l being Nat st
( F /. (k + 1) = l & m <= l )

per cases ( k = 0 or k > 0 ) ;
suppose k = 0 ; :: thesis: ex l being Nat st
( F /. (k + 1) = l & m <= l )

hence ex l being Nat st
( F /. (k + 1) = l & m <= l ) by A67; :: thesis: verum
end;
suppose A73: k > 0 ; :: thesis: ex l being Nat st
( F /. (k + 1) = l & m <= l )

set l1 = F /. (k + 1);
consider l being Nat such that
A74: F /. k = l and
A75: m <= l by ;
reconsider l1 = F /. (k + 1) as Nat ;
k < len F by ;
then F /. (k + 1) in SUCC ((F /. k),S) by ;
then l <= l1 by ;
hence ex l being Nat st
( F /. (k + 1) = l & m <= l ) by ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A76: 1 <= len F by NAT_1:14;
A77: S1[ 0 ] ;
for k being Nat holds S1[k] from then ex l being Nat st
( F /. (len F) = l & m <= l ) by A76;
hence m <= n by A68; :: thesis: verum
end;