let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds
l1 <= l2,S
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; for l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds
l1 <= l2,S
let l1, l2 be Element of NAT ; ( SUCC (l1,S) = NAT implies l1 <= l2,S )
assume A1:
SUCC (l1,S) = NAT
; l1 <= l2,S
defpred S1[ set , set ] means ( ( $1 = 1 implies $2 = l1 ) & ( $1 = 2 implies $2 = l2 ) );
A2:
for n being Nat st n in Seg 2 holds
ex d being Element of NAT st S1[n,d]
consider f being FinSequence of NAT such that
A6:
len f = 2
and
A7:
for n being Nat st n in Seg 2 holds
S1[n,f /. n]
from FINSEQ_4:sch 1(A2);
A8:
1 in Seg 2
by FINSEQ_1:2, TARSKI:def 2;
then A9:
f /. 1 = l1
by A7;
reconsider f = f as non empty FinSequence of NAT by A6;
take
f
; AMI_WSTD:def 1 ( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
2 in Seg 2
by FINSEQ_1:2, TARSKI:def 2;
hence
( f /. 1 = l1 & f /. (len f) = l2 )
by A6, A7, A8; for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S)
let n be Element of NAT ; ( 1 <= n & n < len f implies f /. (n + 1) in SUCC ((f /. n),S) )
assume A10:
1 <= n
; ( not n < len f or f /. (n + 1) in SUCC ((f /. n),S) )
assume
n < len f
; f /. (n + 1) in SUCC ((f /. n),S)
then
n < 1 + 1
by A6;
then
n <= 1
by NAT_1:13;
then
n = 1
by A10, XXREAL_0:1;
hence
f /. (n + 1) in SUCC ((f /. n),S)
by A1, A9; verum