theorem :: ZMODUL02:63

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