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;

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 ) )end;

hence
x in L~ f
; :: thesis: verumper cases
( n <= len f or n > len f )
;

end;

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;then Y c= L~ f by A2, TOPREAL3:19;

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

case
n > len f
; :: thesis: contradiction

then
f /^ n = <*> the carrier of (TOP-REAL 2)
by RFINSEQ:def 1;

hence contradiction by A4; :: thesis: verum

end;hence contradiction by A4; :: thesis: verum