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 ( 1 <= i & i + 1 <= len f ) ; :: thesis: ( f /. i in LSeg f,i & f /. (i + 1) in LSeg f,i )
then LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by Def5;
hence ( f /. i in LSeg f,i & f /. (i + 1) in LSeg f,i ) by RLTOPSP1:69; :: thesis: verum