for R being Ring
for V being LeftMod 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 by VECTSP_6:4;