let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module holds ZMtoMQV (V,p,(0. V)) = 0. (Z_MQ_VectSp (V,p))
let V be free Z_Module; :: thesis: ZMtoMQV (V,p,(0. V)) = 0. (Z_MQ_VectSp (V,p))
thus 0. (Z_MQ_VectSp (V,p)) = 0. (VectQuot (V,(p (*) V)))
.= zeroCoset (V,(p (*) V)) by VECTSP10:def 6
.= ZMtoMQV (V,p,(0. V)) by ZMODUL01:59 ; :: thesis: verum