theorem ThnTV4: :: ZMODUL06:17

for V being Z_Module
for v being Vector of V holds
( not v is torsion iff ( Lin {v} is free & v <> 0. V ) )