theorem :: ZMODUL01:100

for R being Ring
for V being LeftMod of R holds ((0). V) + ((Omega). V) = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_5:10;