theorem Th101: :: ZMODUL01:101

for R being Ring
for V being LeftMod of R
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;