theorem Th32: :: TOPREAL8:32

for f being non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i < len f holds
(LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))}