theorem :: RMOD_4:16

for R being Ring
for V being RightMod of R
for x being set
for L being Linear_Combination of V holds
( x in Carrier L iff ex v being Vector of V st
( x = v & L . v <> 0. R ) ) ;