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

per cases ( i <> 0 or i = 0 ) ;

suppose i <> 0 ; :: thesis: LSeg (f | n),i = LSeg f,i

then A2: 1 <= i by NAT_1:14;
then A3: i in dom (f | n) by A1, GOBOARD2:3;
len (f | n) <= len f by FINSEQ_5:18;
then A4: i + 1 <= len f by A1, XXREAL_0:2;
A5: i + 1 in dom (f | n) by A1, A2, GOBOARD2:3;
thus LSeg (f | n),i = LSeg ((f | n) /. i),((f | n) /. (i + 1)) by A1, A2, TOPREAL1:def 5
.= LSeg (f /. i),((f | n) /. (i + 1)) by A3, FINSEQ_4:85
.= LSeg (f /. i),(f /. (i + 1)) by A5, FINSEQ_4:85
.= LSeg f,i by A2, A4, TOPREAL1:def 5 ; :: thesis: verum

end;

suppose A6: i = 0 ; :: thesis: LSeg (f | n),i = LSeg f,i

hence LSeg (f | n),i = {} by TOPREAL1:def 5
.= LSeg f,i by A6, TOPREAL1:def 5 ;
:: thesis: verum

end;

end;