let f be FinSequence of (TOP-REAL 2); :: thesis: for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))
let i, n be Nat; :: thesis: ( 1 <= i & i + 1 <= (len f) - n implies LSeg ((f /^ n),i) = LSeg (f,(n + i)) )
assume A1: 1 <= i ; :: thesis: ( not i + 1 <= (len f) - n or LSeg ((f /^ n),i) = LSeg (f,(n + i)) )
A2: n <= (i + 1) + n by NAT_1:11;
assume i + 1 <= (len f) - n ; :: thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))
then (i + 1) + n <= len f by XREAL_1:19;
then n <= len f by A2, XXREAL_0:2;
hence LSeg ((f /^ n),i) = LSeg (f,(n + i)) by A1, Th4; :: thesis: verum