:: deftheorem defines RightModule VECTSP_2:def 5 :
for R being Ring holds RightModule R = RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #);