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 ) ) )

( 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

( 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 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 ) ) ) 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 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 ;

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) by FINSEQ_1:44

.= k + 1 by A13, A8, PARTFUN1:def 6 ;

A27: 1 in dom F2 by A24, FINSEQ_3:25;

.= m by FINSEQ_1:44 ;

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: 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 A44, FINSEQ_3:25;

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

.= j by FINSEQ_1:44 ;

hence k <= j by A1, A47, A49; :: thesis: verum

end;( 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 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: not m = k + 1

reconsider F2 = <*(F /. (len F1)),(F /. ((k + 1) .. F))*> as non empty FinSequence of NAT ;
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: contradiction

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: verum

end;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 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: verum

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) by FINSEQ_1:44

.= k + 1 by A13, A8, PARTFUN1:def 6 ;

A27: 1 in dom F2 by A24, FINSEQ_3:25;

A28: now :: thesis: for n being Nat st 1 <= n & n < len F2 holds

F2 /. (n + 1) in SUCC ((F2 /. n),S)

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 A27, PARTFUN1:def 6

.= F /. (len F1) by FINSEQ_1:44 ;

F2 /. (n + 1) = F2 . 2 by A25, A29, PARTFUN1:def 6

.= F /. ((len F1) + 1) by A6, FINSEQ_1:44 ;

hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A4, A16, A10, A30; :: thesis: verum

end;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 A27, PARTFUN1:def 6

.= F /. (len F1) by FINSEQ_1:44 ;

F2 /. (n + 1) = F2 . 2 by A25, A29, PARTFUN1:def 6

.= F /. ((len F1) + 1) by A6, FINSEQ_1:44 ;

hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A4, A16, A10, A30; :: thesis: verum

A31: now :: thesis: for n being Nat st 1 <= n & n < len F1 holds

F1 /. (n + 1) in SUCC ((F1 /. n),S)

F2 /. 1 =
F2 . 1
by A27, PARTFUN1:def 6
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 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: verum

end;assume that

A32: 1 <= n and

A33: n < len F1 ; :: thesis: F1 /. (n + 1) in SUCC ((F1 /. n),S)

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: verum

.= m by FINSEQ_1:44 ;

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: 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 A44, FINSEQ_3:25;

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)

F /. (len F) =
F . 2
by A44, A45, PARTFUN1:def 6
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 A46, PARTFUN1:def 6

.= k by FINSEQ_1:44 ;

F /. (n + 1) = F . 2 by A45, A50, PARTFUN1:def 6

.= j by FINSEQ_1:44 ;

hence F /. (n + 1) in SUCC ((F /. n),S) by A48, A51; :: thesis: verum

end;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 A46, PARTFUN1:def 6

.= k by FINSEQ_1:44 ;

F /. (n + 1) = F . 2 by A45, A50, PARTFUN1:def 6

.= j by FINSEQ_1:44 ;

hence F /. (n + 1) in SUCC ((F /. n),S) by A48, A51; :: thesis: verum

.= j by FINSEQ_1:44 ;

hence k <= j by A1, A47, A49; :: thesis: verum

( 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 )

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 S_{1}[ Nat] means ( 1 <= $1 & $1 <= len F implies ex l being Nat st

( F /. $1 = l & m <= l ) );

A77: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[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: verum

end;( 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

given F being non empty FinSequence of NAT such that A67:
F /. 1 = m
and
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) ) )

end;( 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 A53, XXREAL_0:1;

end;

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) ) )

( 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;( 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

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) ) )

( 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

end;( 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 H_{1}( 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_{1}(j)
from FINSEQ_2:sch 1();

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 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: ( 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 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: 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 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: verum

end;deffunc H

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

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 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: ( 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 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: 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 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: verum

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 S

( F /. $1 = l & m <= l ) );

A70: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A76:
1 <= len F
by NAT_1:14;S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A71: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A71: S

now :: thesis: ( 1 <= k + 1 & k + 1 <= len F implies ex l being Nat st

( F /. (k + 1) = l & m <= l ) )

hence
S( 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 )

end;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 )
;

end;

suppose A73:
k > 0
; :: thesis: ex l being Nat st

( F /. (k + 1) = l & m <= l )

( 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 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: verum

end;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: verum

A77: S

for k being Nat holds S

then ex l being Nat st

( F /. (len F) = l & m <= l ) by A76;

hence m <= n by A68; :: thesis: verum