:: deftheorem Def3 defines LSeg TOPREAL1:def 3 :
for n being Nat
for f being FinSequence of (TOP-REAL n)
for i being Nat holds
( ( 1 <= i & i + 1 <= len f implies LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies LSeg (f,i) = {} ) );