theorem :: VECTSP_9:30

for GF being Field
for V being finite-dimensional VectSp of GF holds
( dim V = 1 iff ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) )