theorem ThLin1: :: ZMODUL06:19

for V being Z_Module
for v being Vector of V
for u being object st u in Lin {v} holds
ex i being Element of INT.Ring st u = i * v