let f be non empty unfolded s.n.c. FinSequence of (TOP-REAL 2); :: thesis: for i being Element of NAT st 1 <= i & i < len f holds
(LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))}
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} )
assume that
A1: 1 <= i and
A2: i < len f ; :: thesis: (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))}
A3: i in dom f by A1, A2, FINSEQ_3:25;
then f /. i = f . i by PARTFUN1:def 6;
then A4: f /. i in rng f by A3, FUNCT_1:3;
assume A5: (LSeg (f,i)) /\ (rng f) <> {(f /. i),(f /. (i + 1))} ; :: thesis: contradiction
A6: i + 1 <= len f by A2, NAT_1:13;
then f /. i in LSeg (f,i) by A1, TOPREAL1:21;
then A7: f /. i in (LSeg (f,i)) /\ (rng f) by A4, XBOOLE_0:def 4;
A8: 1 < i + 1 by A1, XREAL_1:29;
then A9: i + 1 in dom f by A6, FINSEQ_3:25;
then f /. (i + 1) = f . (i + 1) by PARTFUN1:def 6;
then A10: f /. (i + 1) in rng f by A9, FUNCT_1:3;
f /. (i + 1) in LSeg (f,i) by A1, A6, TOPREAL1:21;
then f /. (i + 1) in (LSeg (f,i)) /\ (rng f) by A10, XBOOLE_0:def 4;
then {(f /. i),(f /. (i + 1))} c= (LSeg (f,i)) /\ (rng f) by A7, ZFMISC_1:32;
then not (LSeg (f,i)) /\ (rng f) c= {(f /. i),(f /. (i + 1))} by A5, XBOOLE_0:def 10;
then consider x being set such that
A11: x in (LSeg (f,i)) /\ (rng f) and
A12: not x in {(f /. i),(f /. (i + 1))} by TARSKI:def 3;
reconsider x = x as Point of (TOP-REAL 2) by A11;
A13: x in LSeg (f,i) by A11, XBOOLE_0:def 4;
x in rng f by A11, XBOOLE_0:def 4;
then consider j being set such that
A14: j in dom f and
A15: x = f . j by FUNCT_1:def 3;
A16: x = f /. j by A14, A15, PARTFUN1:def 6;
reconsider j = j as Element of NAT by A14;
A17: 1 <= j by A14, FINSEQ_3:25;
reconsider j = j as Element of NAT ;
A18: x <> f /. i by A12, TARSKI:def 2;
then A19: j <> i by A14, A15, PARTFUN1:def 6;
A20: x <> f /. (i + 1) by A12, TARSKI:def 2;
then A21: j <> i + 1 by A14, A15, PARTFUN1:def 6;

now

per cases ( j + 1 > len f or ( i < j & j + 1 <= len f ) or j < i ) by A19, XXREAL_0:1;

suppose A22: j + 1 > len f ; :: thesis: contradiction

A23: j <= len f by A14, FINSEQ_3:25;
len f <= j by A22, NAT_1:13;
then A24: j = len f by A23, XXREAL_0:1;
consider k being Nat such that
A25: len f = 1 + k by A6, A8, NAT_1:10, XXREAL_0:2;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
1 < len f by A6, A8, XXREAL_0:2;
then 1 <= k by A25, NAT_1:13;
then A26: x in LSeg (f,k) by A16, A24, A25, TOPREAL1:21;
i <= k by A2, A25, NAT_1:13;
then i < k by A20, A16, A24, A25, XXREAL_0:1;
then A27: i + 1 <= k by NAT_1:13;

now

per cases ( i + 1 = k or i + 1 < k ) by A27, XXREAL_0:1;

suppose A28: i + 1 = k ; :: thesis: contradiction

then i + (1 + 1) <= len f by A25;
then (LSeg (f,i)) /\ (LSeg (f,k)) = {(f /. (i + 1))} by A1, A28, TOPREAL1:def 6;
then x in {(f /. (i + 1))} by A13, A26, XBOOLE_0:def 4;
hence contradiction by A20, TARSKI:def 1; :: thesis: verum

end;

suppose i + 1 < k ; :: thesis: contradiction

then LSeg (f,i) misses LSeg (f,k) by TOPREAL1:def 7;
hence contradiction by A13, A26, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose that A29: i < j and
A30: j + 1 <= len f ; :: thesis: contradiction

i + 1 <= j by A29, NAT_1:13;
then i + 1 < j by A21, XXREAL_0:1;
then A31: LSeg (f,i) misses LSeg (f,j) by TOPREAL1:def 7;
x in LSeg (f,j) by A16, A17, A30, TOPREAL1:21;
hence contradiction by A13, A31, XBOOLE_0:3; :: thesis: verum

end;

suppose A32: j < i ; :: thesis: contradiction

then j + 1 <= i + 1 by XREAL_1:6;
then j + 1 <= len f by A6, XXREAL_0:2;
then x in LSeg (f,j) by A16, A17, TOPREAL1:21;
then A33: x in (LSeg (f,i)) /\ (LSeg (f,j)) by A13, XBOOLE_0:def 4;
A34: j + 1 <= i by A32, NAT_1:13;

now

per cases ( j + 1 = i or j + 1 < i ) by A34, XXREAL_0:1;

suppose A35: j + 1 = i ; :: thesis: contradiction

then (j + 1) + 1 <= len f by A2, NAT_1:13;
then j + (1 + 1) <= len f ;
then (LSeg (f,i)) /\ (LSeg (f,j)) = {(f /. i)} by A17, A35, TOPREAL1:def 6;
hence contradiction by A18, A33, TARSKI:def 1; :: thesis: verum

end;

suppose j + 1 < i ; :: thesis: contradiction

then LSeg (f,j) misses LSeg (f,i) by TOPREAL1:def 7;
hence contradiction by A33, XBOOLE_0:4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum