let f be FinSequence of (TOP-REAL 2); :: 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 A5, FINSEQ_3:25;
A9: i <= len f by A5, FINSEQ_3:25;
then reconsider l = (len f) - 1 as Element of NAT by A8, INT_1:5, XXREAL_0:2;
1 <= len f by A8, A9, XXREAL_0:2;
then A10: l + 1 in dom f by FINSEQ_3:25;
A11: i + 1 <= len f by A6, FINSEQ_3:25;
then i + 1 < len f by A7, XXREAL_0:1;
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 A11, XREAL_1:19;
then A14: 1 <= l by A8, XXREAL_0:2;
then A15: f /. (l + 1) in LSeg (f,l) by TOPREAL1:21;
1 <= i + 1 by A6, FINSEQ_3:25;
then A16: f /. (i + 2) in LSeg (f,(i + 1)) by A12, TOPREAL1:21;
l <= len f by XREAL_1:43;
then A17: l in dom f by A14, FINSEQ_3:25;
l <> l + 1 ;
then A18: f /. l <> f /. (l + 1) by A3, A17, A10, PARTFUN2:10;
(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 A4, A16, XBOOLE_0:def 4;
hence contradiction by A18, A19, A20, TARSKI:def 1; :: thesis: verum
end;
suppose l <> i + 1 ; :: thesis: contradiction
then i + 1 < l by A13, XXREAL_0:1;
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