let f be FinSequence of (); :: 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 ;
A10: k + 1 = len f ;
assume m + 1 <> len f ; :: thesis: contradiction
then A11: m + 1 <= k by ;
1 <= len f by ;
then A12: len f in dom f by FINSEQ_3:25;
per cases ( m + 1 = k or m + 1 < k ) by ;
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 ;
(LSeg (f,m)) /\ (LSeg (f,(m + 1))) = {(f /. (m + 1))} by A3, A7, A8, A13;
then f /. (len f) in {(f /. (m + 1))} by ;
then A16: f /. (len f) = f /. (m + 1) by TARSKI:def 1;
m + 1 <= len f by ;
then m + 1 in dom f by ;
then len f = (len f) - 1 by ;
hence contradiction ; :: thesis: verum
end;
suppose A17: m + 1 < k ; :: thesis: contradiction
(1 + 1) - 1 = 1 ;
then ( k + 1 = len f & 1 <= k ) by ;
then A18: f /. (len f) in LSeg (f,k) by TOPREAL1:21;
LSeg (f,m) misses LSeg (f,k) by ;
then (LSeg (f,m)) /\ (LSeg (f,k)) = {} ;
hence contradiction by A2, A18, XBOOLE_0:def 4; :: thesis: verum
end;
end;