let n be Nat; :: thesis: the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n)
reconsider D = REAL as non empty set ;
A1: Funcs ((Seg n),D) = REAL n by FINSEQ_2:93;
RealVectSpace (Seg n) = RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def 6;
hence the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n) by A1, EUCLID:22; :: thesis: verum