theorem :: ZMODUL02:72
for V being Z_Module
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) by MOD_3:12;