let f be FinSequence of (TOP-REAL 2); :: thesis: for i, n being Nat st n <= len f & 1 <= i holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))
let i, n be Nat; :: thesis: ( n <= len f & 1 <= i implies LSeg ((f /^ n),i) = LSeg (f,(n + i)) )
assume that
A1: n <= len f and
A2: 1 <= i ; :: thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))

per cases ( i + 1 <= (len f) - n or i + 1 > (len f) - n ) ;

suppose A3: i + 1 <= (len f) - n ; :: thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))

1 <= i + 1 by NAT_1:11;
then 1 <= (len f) - n by A3, XXREAL_0:2;
then A4: 1 + n <= len f by XREAL_1:19;
n <= 1 + n by NAT_1:11;
then n <= len f by A4, XXREAL_0:2;
then A5: len (f /^ n) = (len f) - n by RFINSEQ:def 1;
then A6: i in dom (f /^ n) by A2, A3, SEQ_4:134;
A7: (i + 1) + n <= len f by A3, XREAL_1:19;
i <= i + n by NAT_1:11;
then A8: 1 <= i + n by A2, XXREAL_0:2;
A9: i + 1 in dom (f /^ n) by A2, A3, A5, SEQ_4:134;
thus LSeg ((f /^ n),i) = LSeg (((f /^ n) /. i),((f /^ n) /. (i + 1))) by A2, A3, A5, TOPREAL1:def 3
.= LSeg ((f /. (i + n)),((f /^ n) /. (i + 1))) by A6, FINSEQ_5:27
.= LSeg ((f /. (i + n)),(f /. ((i + 1) + n))) by A9, FINSEQ_5:27
.= LSeg ((f /. (i + n)),(f /. ((i + n) + 1)))
.= LSeg (f,(n + i)) by A8, A7, TOPREAL1:def 3 ; :: thesis: verum

end;

suppose A10: i + 1 > (len f) - n ; :: thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))

then n + (i + 1) > len f by XREAL_1:19;
then A11: (n + i) + 1 > len f ;
i + 1 > len (f /^ n) by A1, A10, RFINSEQ:def 1;
hence LSeg ((f /^ n),i) = {} by TOPREAL1:def 3
.= LSeg (f,(n + i)) by A11, TOPREAL1:def 3 ;
:: thesis: verum

end;

end;