let n be Nat; :: thesis: dim (TOP-REAL n) = n
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;
then dim ((Omega). (TOP-REAL n)) = n by EUCLID_7:46;
hence dim (TOP-REAL n) = n by RLVECT_5:30; :: thesis: verum