theorem LmStrict11a: :: ZMODUL07:32
for V being Z_Module
for W being Submodule of V
for Ws being strict Submodule of V
for v being VECTOR of V st Ws = (Omega). W holds
v + W = v + Ws