theorem :: ZMODUL06:21

for V being Z_Module
for v being Vector of V
for i being Element of INT.Ring holds i * v in Lin {v} by ZMODUL01:37, ThLin2;