theorem :: ZMODUL01:10

for a being Element of INT.Ring
for V being Z_Module
for v, w being Vector of V st V is Mult-cancelable & a <> 0. INT.Ring & a * v = a * w holds
v = w