theorem :: RMOD_4:69

for R being domRing
for V being RightMod of R holds Lin ({} the carrier of V) = (0). V