theorem ThEQRZMV3C: :: ZMODUL04:11
for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent holds
IQ is linearly-independent