theorem Th4: :: MOD_3:4

for x being object
for R being Ring
for V being LeftMod of R
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) by VECTSP_7:7;