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) )
assume i + 1 <= (len f) - n ; :: thesis: LSeg (f /^ n),i = LSeg f,(n + i)
then A2: (i + 1) + n <= len f by XREAL_1:21;
n <= (i + 1) + n by NAT_1:11;
then n <= len f by A2, XXREAL_0:2;
hence LSeg (f /^ n),i = LSeg f,(n + i) by A1, Th4; :: thesis: verum