let i be Element of NAT ; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2) holds LSeg f,i is closed
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: LSeg f,i is closed

per cases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ;

suppose ( 1 <= i & i + 1 <= len f ) ; :: thesis: LSeg f,i is closed

then LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by TOPREAL1:def 5;
hence LSeg f,i is closed by Th28, COMPTS_1:16; :: thesis: verum

end;

suppose A1: ( not 1 <= i or not i + 1 <= len f ) ; :: thesis: LSeg f,i is closed

{} (TOP-REAL 2) is closed ;
hence LSeg f,i is closed by A1, TOPREAL1:def 5; :: thesis: verum

end;

end;