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 (Z_ModuleQuot (V,W)) st W = p (*) V holds
p * x = 0. (Z_ModuleQuot (V,W))