let V be Z_Module; :: thesis: for v being Vector of V holds
( not v is torsion iff {v} is linearly-independent )
let v be Vector of V; :: thesis: ( not v is torsion iff {v} is linearly-independent )
A1: ( not v is torsion implies {v} is linearly-independent )

proof

assume B1: not v is torsion ; :: thesis: {v} is linearly-independent
let l be Linear_Combination of {v}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume B4: Sum l = 0. V ; :: thesis: Carrier l = {}

now :: thesis: Carrier l = {}

per cases ( Carrier l = {} or Carrier l = {v} ) by ZFMISC_1:33, VECTSP_6:def 4;

suppose Carrier l = {} ; :: thesis: Carrier l = {}

hence Carrier l = {} ; :: thesis: verum

end;

suppose B5: Carrier l = {v} ; :: thesis: Carrier l = {}

then B6: 0. V = (l . v) * v by B4, ZMODUL02:24;

now :: thesis: not v in Carrier l

assume v in Carrier l ; :: thesis: contradiction
then ex u being Vector of V st
( v = u & l . u <> 0. INT.Ring ) ;
hence contradiction by B1, B6; :: thesis: verum

end;

hence Carrier l = {} by B5, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence Carrier l = {} ; :: thesis: verum

end;

( {v} is linearly-independent implies not v is torsion )

proof

assume B1: {v} is linearly-independent ; :: thesis: not v is torsion
assume v is torsion ; :: thesis: contradiction
then consider i being Element of INT.Ring such that
C2: ( i <> 0 & i * v = 0. V ) ;
consider l being Linear_Combination of V such that
C3: ( l . v = 1 & ( for u being Vector of V st v <> u holds
l . u = 0. INT.Ring ) ) by ZMODUL03:1;
for u being Vector of V st u <> v holds
not u in Carrier l

proof

let u be Vector of V; :: thesis: ( u <> v implies not u in Carrier l )
assume u <> v ; :: thesis: not u in Carrier l
then l . u = 0 by C3;
hence not u in Carrier l by ZMODUL02:8; :: thesis: verum

end;

then for u being object holds
( u = v iff u in Carrier l ) by C3;
then C5: Carrier l = {v} by TARSKI:def 1;
then C6: Carrier (i * l) = {v} by C2, ZMODUL02:29;
C7: Carrier (i * l) <> {} by C2, C5, ZMODUL02:29;
reconsider li = i * l as Linear_Combination of {v} by C6, VECTSP_6:def 4;
Sum (i * l) = i * (Sum l) by ZMODUL02:53
.= i * ((1. INT.Ring) * v) by C3, C5, ZMODUL02:24
.= 0. V by C2 ;
then Sum li = 0. V ;
hence contradiction by B1, C7; :: thesis: verum

end;

hence ( not v is torsion iff {v} is linearly-independent ) by A1; :: thesis: verum