theorem Th26: :: ZMODUL05:37

for V being Z_Module
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. INT.Ring