for R being Ring
for V being RightMod of R
for A being Subset of V holds ZeroLC V is Linear_Combination of A