let f be FinSequence of (TOP-REAL 2); for m being Nat st f is being_S-Seq & f /. (len f) in LSeg (f,m) & 1 <= m & m + 1 <= len f holds
m + 1 = len f
let m be Nat; ( f is being_S-Seq & f /. (len f) in LSeg (f,m) & 1 <= m & m + 1 <= len f implies m + 1 = len f )
assume that
A1:
f is being_S-Seq
and
A2:
f /. (len f) in LSeg (f,m)
and
A3:
1 <= m
and
A4:
m + 1 <= len f
; m + 1 = len f
A5:
f is s.n.c.
by A1;
A6:
f is one-to-one
by A1;
A7:
f is unfolded
by A1;
set q = f /. (len f);
A8:
(m + 1) + 1 = m + (1 + 1)
;
A9:
len f >= 2
by A1;
then reconsider k = (len f) - 1 as Element of NAT by INT_1:5, XXREAL_0:2;
A10:
k + 1 = len f
;
assume
m + 1 <> len f
; contradiction
then A11:
m + 1 <= k
by A4, A10, NAT_1:8;
1 <= len f
by A9, XXREAL_0:2;
then A12:
len f in dom f
by FINSEQ_3:25;
per cases
( m + 1 = k or m + 1 < k )
by A11, XXREAL_0:1;
suppose A13:
m + 1
= k
;
contradictionA14:
1
<= m + 1
by NAT_1:11;
(m + 1) + 1
<= len f
by A13;
then A15:
f /. (m + 2) in LSeg (
f,
(m + 1))
by A14, TOPREAL1:21;
(LSeg (f,m)) /\ (LSeg (f,(m + 1))) = {(f /. (m + 1))}
by A3, A7, A8, A13;
then
f /. (len f) in {(f /. (m + 1))}
by A2, A13, A15, XBOOLE_0:def 4;
then A16:
f /. (len f) = f /. (m + 1)
by TARSKI:def 1;
m + 1
<= len f
by A10, A13, NAT_1:11;
then
m + 1
in dom f
by A14, FINSEQ_3:25;
then
len f = (len f) - 1
by A6, A12, A13, A16, PARTFUN2:10;
hence
contradiction
;
verum end;