let n, i be Nat; :: thesis: for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds
( f /. i in LSeg f,i & f /. (i + 1) in LSeg f,i )
let f be FinSequence of (TOP-REAL n); :: thesis: ( 1 <= i & i + 1 <= len f implies ( f /. i in LSeg f,i & f /. (i + 1) in LSeg f,i ) )
assume that
A1: 1 <= i and
A2: i + 1 <= len f ; :: thesis: ( f /. i in LSeg f,i & f /. (i + 1) in LSeg f,i )
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A1, A2, Def5;
hence ( f /. i in LSeg f,i & f /. (i + 1) in LSeg f,i ) by RLTOPSP1:69; :: thesis: verum