theorem :: RUSUB_4:13

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