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