theorem Th35: :: ZMODUL03:35

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
IQ is Basis of (Z_MQ_VectSp (V,p))