theorem Th1: :: LMOD_XX1:1

for M, N being AbGroup
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) )