theorem Th30: :: LMOD_XX1:31

for R being comRing
for M being LeftMod of R
for f, g, h being Endomorphism of R,M holds
( AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g)) iff for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x) )