theorem :: ZMODUL08:3
for V being Z_Module
for v being divisible Vector of V
for i being Element of INT.Ring holds i * v is divisible