theorem Th10: :: RLVECT_X:10

for i being Integer
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A