for R being Ring
for V being RightMod of R
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B