:: deftheorem Def2 defines Submodule RMOD_2:def 2 :
for R being Ring
for V, b₃ being RightMod of R holds
( b₃ is Submodule of V iff ( the carrier of b₃ c= the carrier of V & 0. b₃ = 0. V & the addF of b₃ = the addF of V | [: the carrier of b₃, the carrier of b₃:] & the rmult of b₃ = the rmult of V | [: the carrier of b₃, the carrier of R:] ) );