theorem Th1V: :: ZMODUL06:1

for V being Z_Module
for W being Submodule of V holds (1. INT.Ring) (*) W = (Omega). W