let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat holds L~ (f | i) c= L~ f
let i be Nat; :: thesis: L~ (f | i) c= L~ f
set h = f | i;
set Mh = { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } ;
set Mf = { (LSeg (f,m)) where m is Nat : ( 1 <= m & m + 1 <= len f ) } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ (f | i) or x in L~ f )
A1: f | i = f | (Seg i) by FINSEQ_1:def 16;
A2: dom f = Seg (len f) by FINSEQ_1:def 3;
assume A3: x in L~ (f | i) ; :: thesis: x in L~ f
then consider X being set such that
A4: x in X and
A5: X in { (LSeg ((f | i),n)) where n is Nat : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def 4;
consider k being Nat such that
A6: X = LSeg ((f | i),k) and
A7: 1 <= k and
A8: k + 1 <= len (f | i) by A5;

per cases ( i in dom f or not i in dom f ) ;

suppose A9: i in dom f ; :: thesis: x in L~ f

A10: dom (f | i) = (dom f) /\ (Seg i) by A1, RELAT_1:61;
A11: i in NAT by ORDINAL1:def 12;
A12: i <= len f by A9, FINSEQ_3:25;
then Seg i c= dom f by A2, FINSEQ_1:5;
then dom (f | i) = Seg i by A10, XBOOLE_1:28;
then len (f | i) <= len f by A12, A11, FINSEQ_1:def 3;
then A13: k + 1 <= len f by A8, XXREAL_0:2;
k <= k + 1 by NAT_1:12;
then k <= len (f | i) by A8, XXREAL_0:2;
then A14: k in dom (f | i) by A7, FINSEQ_3:25;
1 <= k + 1 by NAT_1:12;
then k + 1 in dom (f | i) by A8, FINSEQ_3:25;
then X = LSeg (f,k) by A6, A14, Th17;
then X in { (LSeg (f,m)) where m is Nat : ( 1 <= m & m + 1 <= len f ) } by A7, A13;
hence x in L~ f by A4, TARSKI:def 4; :: thesis: verum

end;

suppose A15: not i in dom f ; :: thesis: x in L~ f

now :: thesis: ( ( i < 1 & contradiction ) or ( len f < i & x in L~ f ) )

per cases ( i < 1 or len f < i ) by A15, FINSEQ_3:25;

case i < 1 ; :: thesis: contradiction

then i < 0 + 1 ;
then i <= 0 by NAT_1:13;
then Seg i = {} ;
then dom (f | i) = (dom f) /\ {} by A1, RELAT_1:61;
then dom (f | i) = {} ;
then Seg (len (f | i)) = {} by FINSEQ_1:def 3;
then len (f | i) = 0 ;
hence contradiction by A3, TOPREAL1:22; :: thesis: verum

end;

case len f < i ; :: thesis: x in L~ f

then Seg (len f) c= Seg i by FINSEQ_1:5;
then dom f c= Seg i by FINSEQ_1:def 3;
then A16: dom f = (dom f) /\ (Seg i) by XBOOLE_1:28;
for x being object st x in dom (f | i) holds
(f | i) . x = f . x by A1, FUNCT_1:47;
then f | i = f by A1, A16, RELAT_1:61;
hence x in L~ f by A4, A5, TARSKI:def 4; :: thesis: verum

end;

end;

end;

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

end;

end;