let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st 1 <= i & i + 1 <= len f holds
LSeg ((f /. i),(f /. (i + 1))) c= L~ f
let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) c= L~ f )
assume that
A1: 1 <= i and
A2: i + 1 <= len f ; :: thesis: LSeg ((f /. i),(f /. (i + 1))) c= L~ f
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def 3;
hence LSeg ((f /. i),(f /. (i + 1))) c= L~ f by TOPREAL3:19; :: thesis: verum