let f be FinSequence of (TOP-REAL 2); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: contradiction

A14: 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 ; :: thesis: verum

end;

suppose A17: m + 1 < k ; :: thesis: contradiction

(1 + 1) - 1 = 1 ;
then ( k + 1 = len f & 1 <= k ) by A9, XREAL_1:13;
then A18: f /. (len f) in LSeg (f,k) by TOPREAL1:21;
LSeg (f,m) misses LSeg (f,k) by A5, A17;
then (LSeg (f,m)) /\ (LSeg (f,k)) = {} ;
hence contradiction by A2, A18, XBOOLE_0:def 4; :: thesis: verum

end;

end;