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

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