for p, i 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 p <> 0 & W = p (*) V holds
i * x = (i mod p) * x