theorem Th23: :: LMOD_XX1:23
for R being comRing
for M, N being LeftMod of R
for f1, g1 being Element of (Func_Mod (R,M,N))
for f, g being Element of (Hom (R,M,N)) st f1 = f & g1 = g holds
f + g = f1 + g1