let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT holds L~ (f /^ n) c= L~ f
let n be Element of NAT ; :: thesis: L~ (f /^ n) c= L~ f
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ (f /^ n) or x in L~ f )
assume x in L~ (f /^ n) ; :: thesis: x in L~ f
then x in union { (LSeg (f /^ n),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ n) ) } by TOPREAL1:def 6;
then consider Y being set such that
A1: ( x in Y & Y in { (LSeg (f /^ n),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ n) ) } ) by TARSKI:def 4;
consider i being Element of NAT such that
A2: Y = LSeg (f /^ n),i and
A3: 1 <= i and
A4: i + 1 <= len (f /^ n) by A1;

now

per cases ( n <= len f or n > len f ) ;

case n <= len f ; :: thesis: x in L~ f

then LSeg (f /^ n),i = LSeg f,(n + i) by A3, SPPOL_2:4;
then Y c= L~ f by A2, TOPREAL3:26;
hence x in L~ f by A1; :: thesis: verum

end;

case n > len f ; :: thesis: contradiction

then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def 2;
hence contradiction by A4; :: thesis: verum

end;

end;

end;

hence x in L~ f ; :: thesis: verum