let i, n 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, Def3;
hence ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) by RLTOPSP1:68; :: thesis: verum