let g1, g2 be FinSequence of (TOP-REAL 2); :: thesis: L~ g1 c= L~ (g1 ^' g2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ g1 or x in L~ (g1 ^' g2) )

assume x in L~ g1 ; :: thesis: x in L~ (g1 ^' g2)

then consider a being set such that

A1: ( x in a & a in { (LSeg (g1,i)) where i is Nat : ( 1 <= i & i + 1 <= len g1 ) } ) by TARSKI:def 4;

consider j being Nat such that

A2: a = LSeg (g1,j) and

A3: 1 <= j and

A4: j + 1 <= len g1 by A1;

j < len g1 by A4, NAT_1:13;

then A5: a = LSeg ((g1 ^' g2),j) by A2, TOPREAL8:28;

len g1 <= len (g1 ^' g2) by TOPREAL8:7;

then j + 1 <= len (g1 ^' g2) by A4, XXREAL_0:2;

then a in { (LSeg ((g1 ^' g2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (g1 ^' g2) ) } by A3, A5;

hence x in L~ (g1 ^' g2) by A1, TARSKI:def 4; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ g1 or x in L~ (g1 ^' g2) )

assume x in L~ g1 ; :: thesis: x in L~ (g1 ^' g2)

then consider a being set such that

A1: ( x in a & a in { (LSeg (g1,i)) where i is Nat : ( 1 <= i & i + 1 <= len g1 ) } ) by TARSKI:def 4;

consider j being Nat such that

A2: a = LSeg (g1,j) and

A3: 1 <= j and

A4: j + 1 <= len g1 by A1;

j < len g1 by A4, NAT_1:13;

then A5: a = LSeg ((g1 ^' g2),j) by A2, TOPREAL8:28;

len g1 <= len (g1 ^' g2) by TOPREAL8:7;

then j + 1 <= len (g1 ^' g2) by A4, XXREAL_0:2;

then a in { (LSeg ((g1 ^' g2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (g1 ^' g2) ) } by A3, A5;

hence x in L~ (g1 ^' g2) by A1, TARSKI:def 4; :: thesis: verum