:: deftheorem defines (Omega). RMOD_2:def 4 :
for R being Ring
for V being RightMod of R holds (Omega). V = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);