:: deftheorem defines linearly-closed RMOD_2:def 1 :
for R being Ring
for V being RightMod of R
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being Vector of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Scalar of R
for v being Vector of V st v in V1 holds
v * a in V1 ) ) );