theorem Th101: :: ZMODUL01:101

for V being Z_Module
for W being Submodule of V holds ((Omega). V) + W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_5:11;