let V be Z_Module; :: thesis: for v being Vector of V holds
( not v is torsion iff ( Lin {v} is free & v <> 0. V ) )
let v be Vector of V; :: thesis: ( not v is torsion iff ( Lin {v} is free & v <> 0. V ) )
hereby :: thesis: ( Lin {v} is free & v <> 0. V implies not v is torsion )
assume not v is torsion ; :: thesis: ( Lin {v} is free & v <> 0. V )
then {v} is linearly-independent Subset of V by ThnTV3;
hence ( Lin {v} is free & v <> 0. V ) ; :: thesis: verum
end;
assume A1: ( Lin {v} is free & v <> 0. V ) ; :: thesis: not v is torsion
then A2: Lin {v} is torsion-free ;
A3: v <> 0. (Lin {v}) by A1, ZMODUL01:26;
v in {v} by TARSKI:def 1;
then v in Lin {v} by ZMODUL02:65;
then reconsider vl = v as Vector of (Lin {v}) ;
not vl is torsion by A2, A3;
hence not v is torsion by ThTV6; :: thesis: verum