for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT holds L~ (f /^ n) c= L~ f