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;

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;

end;

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

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