theorem Th27: :: ZMODUL03:27

for p being prime Element of INT.Ring
for V being free Z_Module holds ZMtoMQV (V,p,(0. V)) = 0. (Z_MQ_VectSp (V,p))