for n being Element of NAT
for f being FinSequence of REAL st len f = n holds
f in the carrier of (TOP-REAL n) by TOPREAL3:46;