let V be RealLinearSpace; :: thesis: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace
(Omega). V is RealLinearSpace ;
hence RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace ; :: thesis: verum