:: deftheorem defines zeroCoset ZMODUL02:def 8 :
for V being Z_Module
for W being Submodule of V holds zeroCoset (V,W) = the carrier of W;