let n be Nat; :: thesis: 0.REAL n = 0. (TOP-REAL 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 Def8;
hence 0.REAL n = 0. (TOP-REAL n) ; :: thesis: verum