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

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