theorem Th40: :: ZMODUL01:40

for R being Ring
for V being LeftMod of R
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [: the carrier of R,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the lmult of V | [: the carrier of R,V1:] holds
ModuleStr(# D,A,d1,M #) is Submodule of V