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 15;

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;

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 15;

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

end;

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

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

end;

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

hence
x in L~ f
; :: thesis: verumper cases
( i < 1 or len f < i )
by A15, FINSEQ_3:25;

end;

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

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