let f be FinSequence of (); :: thesis: for i being 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 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 and
A4: f /. (len f) in LSeg (f,i) and
A5: i in dom f and
A6: i + 1 in dom f and
A7: i + 1 <> len f ; :: thesis: contradiction
A8: 1 <= i by ;
A9: i <= len f by ;
then reconsider l = (len f) - 1 as Element of NAT by ;
1 <= len f by ;
then A10: l + 1 in dom f by FINSEQ_3:25;
A11: i + 1 <= len f by ;
then i + 1 < len f by ;
then A12: (i + 1) + 1 <= len f by NAT_1:13;
then A13: i + 1 <= (len f) - 1 by XREAL_1:19;
i <= l by ;
then A14: 1 <= l by ;
then A15: f /. (l + 1) in LSeg (f,l) by TOPREAL1:21;
1 <= i + 1 by ;
then A16: f /. (i + 2) in LSeg (f,(i + 1)) by ;
l <= len f by XREAL_1:43;
then A17: l in dom f by ;
l <> l + 1 ;
then A18: f /. l <> f /. (l + 1) by ;
(i + 1) + 1 = i + (1 + 1) ;
then A19: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A1, A8, A12;
now :: thesis: contradiction
per cases ( l = i + 1 or l <> i + 1 ) ;
suppose A20: l = i + 1 ; :: thesis: contradiction
then f /. (len f) in (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by ;
hence contradiction by A18, A19, A20, TARSKI:def 1; :: thesis: verum
end;
suppose l <> i + 1 ; :: thesis: contradiction
then i + 1 < l by ;
then LSeg (f,i) misses LSeg (f,l) by A2;
then (LSeg (f,i)) /\ (LSeg (f,l)) = {} ;
hence contradiction by A4, A15, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum