RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by EUCLID:def 8;
then (Omega). (TOP-REAL n) = RealVectSpace (Seg n) by RLSUB_1:def 4;
hence TOP-REAL n is finite-dimensional by Th3; :: thesis: verum