let V be Z_Module; :: thesis: for A being Subset of V
for v being Vector of V st A is linearly-independent & v in A holds
not v is torsion
let A be Subset of V; :: thesis: for v being Vector of V st A is linearly-independent & v in A holds
not v is torsion
let v be Vector of V; :: thesis: ( A is linearly-independent & v in A implies not v is torsion )
assume A1: ( A is linearly-independent & v in A ) ; :: thesis: not v is torsion
{v} is linearly-independent by A1, ZMODUL02:56, ZFMISC_1:31;
hence not v is torsion by ThnTV3; :: thesis: verum