theorem Th3: :: RLVECT_5:3

for V being RealLinearSpace
for L being Linear_Combination of V
for x being VECTOR of V holds
( x in Carrier L iff ex v being VECTOR of V st
( x = v & L . v <> 0 ) )