let g1, g2 be FinSequence of (TOP-REAL 2); :: thesis: L~ g1 c= L~ (g1 ^' g2)
let x be set ; :: 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 Element of NAT : ( 1 <= i & i + 1 <= len g1 ) } ) by TARSKI:def 4;
consider j being Element of 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 Element of NAT : ( 1 <= i & i + 1 <= len (g1 ^' g2) ) } by A3, A5;
hence x in L~ (g1 ^' g2) by A1, TARSKI:def 4; :: thesis: verum