theorem :: ZMODUL05:5

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