theorem :: MOD_3:12
for R being Ring
for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) by VECTSP_7:15;