let f be FinSequence of (TOP-REAL 2); for i being Nat holds L~ (f | i) c= L~ f
let i be Nat; 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 ; TARSKI:def 3 ( 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)
; 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
;
x in L~ fA10:
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;
verum end;