:: deftheorem defines Sum LMOD_7:def 8 :
for K being Ring
for V being LeftMod of K
for Li being FinSequence of Submodules V holds Sum Li = (SubJoin V) $$ Li;