:: deftheorem defines LC_Z_Module ZMODUL02:def 35 :
for R being Ring
for V being LeftMod of R
for A being Subset of V
for b₄ being strict Submodule of LC_Z_Module V holds
( b₄ = LC_Z_Module A iff the carrier of b₄ = { l where l is Linear_Combination of A : verum } );