theorem ThEQRZMV3A: :: ZMODUL04:8

for V being Z_Module
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT )