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 Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set l1 = { (LSeg (f ^ g),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f ^ g) ) } ;
let x be set ; :: 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 & X in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) by TARSKI:def 4;
consider n being Element of NAT such that
A2: ( X = LSeg f,n & 1 <= n & n + 1 <= len f ) by A1;
A3: ( dom f = Seg (len f) & len (f ^ g) = (len f) + (len g) ) by FINSEQ_1:35, FINSEQ_1:def 3;
( n <= n + 1 & n + 1 <= len f & 0 <= len g ) by A2, NAT_1:11;
then ( 1 <= n + 1 & n <= len f & len f <= len (f ^ g) ) by A3, XREAL_1:33, XXREAL_0:2;
then ( n in dom f & n + 1 in dom f & len f <= len (f ^ g) ) by A2, FINSEQ_3:27;
then ( X = LSeg (f ^ g),n & n + 1 <= len (f ^ g) ) by A2, TOPREAL3:25, XXREAL_0:2;
then X in { (LSeg (f ^ g),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f ^ g) ) } by A2;
hence x in L~ (f ^ g) by A1, TARSKI:def 4; :: thesis: verum