theorem ThEQRZMV4: :: ZMODUL04:12

for V being Z_Module
for I being Subset of V
for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )