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 object ; :: 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 Nat : ( 1 <= i & i + 1 <= len (f /^ n) ) } by TOPREAL1:def 4;
then consider Y being set such that
A1: ( x in Y & Y in { (LSeg ((f /^ n),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ n) ) } ) by TARSKI:def 4;
consider i being Nat such that
A2: Y = LSeg ((f /^ n),i) and
A3: 1 <= i and
A4: i + 1 <= len (f /^ n) by A1;
now :: thesis: ( ( n <= len f & x in L~ f ) or ( n > len f & contradiction ) )
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:19;
hence x in L~ f by A1; :: thesis: verum
end;
end;
end;
hence x in L~ f ; :: thesis: verum