theorem :: ZMODUL02:63

for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V st R = INT.Ring & V is Mult-cancelable holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )