let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg f,i & i in dom f & i + 1 in dom f holds
i + 1 = len f
let i be Element of NAT ; :: thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg f,i & i in dom f & i + 1 in dom f implies i + 1 = len f )
assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: ( f is one-to-one & f /. (len f) in LSeg f,i & i in dom f & i + 1 in dom f ) and
A4: i + 1 <> len f ; :: thesis: contradiction
A5: ( 1 <= i & i <= len f & 1 <= i + 1 & i + 1 <= len f ) by A3, FINSEQ_3:27;
then i + 1 < len f by A4, XXREAL_0:1;
then A6: ( (i + 1) + 1 <= len f & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:13;
then A7: ( i + 1 <= (len f) - 1 & 1 <= len f & i + 2 <= len f ) by A5, XREAL_1:21, XXREAL_0:2;
then reconsider l = (len f) - 1 as Element of NAT by INT_1:18;
( i <= l & 0 <= 1 ) by A5, XREAL_1:21;
then A8: ( 1 <= l & l <= len f & l + 1 = len f ) by A5, XREAL_1:45, XXREAL_0:2;
then A9: ( l in dom f & l + 1 in dom f ) by A7, FINSEQ_3:27;
A10: f /. (l + 1) in LSeg f,l by A8, TOPREAL1:27;
l <> l + 1 ;
then A11: f /. l <> f /. (l + 1) by A3, A9, PARTFUN2:17;
A12: ( (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} & i + 2 in dom f ) by A1, A5, A6, Th4, TOPREAL1:def 8;
A13: f /. (i + 2) in LSeg f,(i + 1) by A5, A6, TOPREAL1:27;

now

per cases ( l = i + 1 or l <> i + 1 ) ;

suppose A14: l = i + 1 ; :: thesis: contradiction

then f /. (len f) in (LSeg f,i) /\ (LSeg f,(i + 1)) by A3, A13, XBOOLE_0:def 4;
hence contradiction by A11, A12, A14, TARSKI:def 1; :: thesis: verum

end;

suppose l <> i + 1 ; :: thesis: contradiction

then i + 1 < l by A7, XXREAL_0:1;
then LSeg f,i misses LSeg f,l by A2, TOPREAL1:def 9;
then (LSeg f,i) /\ (LSeg f,l) = {} by XBOOLE_0:def 7;
hence contradiction by A3, A10, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum