theorem Th21: :: EUCLID:24

for n being Nat
for p being Point of (TOP-REAL n) holds p is FinSequence of REAL