theorem LMFirst5: :: ZMODUL07:31

for V being Z_Module
for W being Submodule of V holds ker (ZQMorph (V,W)) = (Omega). W