let p be Prime; :: 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. (Z_ModuleQuot (V,(p (*) V)))
.= zeroCoset (V,(p (*) V)) by ZMODUL02:def 10
.= ZMtoMQV (V,p,(0. V)) by ZMODUL01:59 ; :: thesis: verum