theorem ThEQRZMV3: :: ZMODUL04:9

for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )