let g1, g2 be FinSequence of (TOP-REAL 2); L~ g1 c= L~ (g1 ^' g2)
let x be object ; TARSKI:def 3 ( not x in L~ g1 or x in L~ (g1 ^' g2) )
assume
x in L~ g1
; 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; verum