let f, g be FinSequence of (TOP-REAL 2); :: thesis: L~ f c= L~ (f ^ g)
set f1 = f ^ g;
set lf = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
set l1 = { (LSeg ((f ^ g),j)) where j is Nat : ( 1 <= j & j + 1 <= len (f ^ g) ) } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ (f ^ g) )
assume x in L~ f ; :: thesis: x in L~ (f ^ g)
then consider X being set such that
A1: x in X and
A2: X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def 4;
consider n being Nat such that
A3: X = LSeg (f,n) and
A4: 1 <= n and
A5: n + 1 <= len f by A2;
n <= n + 1 by NAT_1:11;
then n <= len f by A5, XXREAL_0:2;
then A6: n in dom f by A4, FINSEQ_3:25;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then len f <= len (f ^ g) by XREAL_1:31;
then A7: n + 1 <= len (f ^ g) by A5, XXREAL_0:2;
1 <= n + 1 by XREAL_1:31;
then n + 1 in dom f by A5, FINSEQ_3:25;
then X = LSeg ((f ^ g),n) by A3, A6, TOPREAL3:18;
then X in { (LSeg ((f ^ g),j)) where j is Nat : ( 1 <= j & j + 1 <= len (f ^ g) ) } by A4, A7;
hence x in L~ (f ^ g) by A1, TARSKI:def 4; :: thesis: verum