theorem ThQuotAX: :: ZMODUL04:13

for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for l being Linear_Combination of I
for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds
Class ((EQRZM V),[(Sum l),i]) in Lin IQ