let f be FinSequence of (); :: 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;
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 ;
A11: i in NAT by ORDINAL1:def 12;
A12: i <= len f by ;
then Seg i c= dom f by ;
then dom (f | i) = Seg i by ;
then len (f | i) <= len f by ;
then A13: k + 1 <= len f by ;
k <= k + 1 by NAT_1:12;
then k <= len (f | i) by ;
then A14: k in dom (f | i) by ;
1 <= k + 1 by NAT_1:12;
then k + 1 in dom (f | i) by ;
then X = LSeg (f,k) by ;
then X in { (LSeg (f,m)) where m is Nat : ( 1 <= m & m + 1 <= len f ) } by ;
hence x in L~ f by ; :: 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 ;
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 ;
then f | i = f by ;
hence x in L~ f by ; :: thesis: verum
end;
end;
end;
hence x in L~ f ; :: thesis: verum
end;
end;