theorem Th2: :: VECTSP_9:2

for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V