theorem Th1: :: ZMODUL02:1

for p being Element of INT.Ring
for V being Z_Module
for W being Submodule of V
for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds
p * x = 0. (VectQuot (V,W))