theorem ThEQRZMV3D: :: ZMODUL04:15

for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds
IQ is Basis of (Z_MQ_VectSp V)