:: deftheorem defines LeftModule VECTSP_2:def 4 :
for R being Ring holds LeftModule R = ModuleStr(# the carrier of R, the addF of R,(0. R), the multF of R #);