theorem Th15: :: LMOD_XX1:15

for R being Ring
for M, N being LeftMod of R
for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (ADD (M,N)) . (f,g) iff for x being Element of the carrier of M holds h . x = (f . x) + (g . x) )