theorem :: RLVECT_5:33

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