theorem Th4: :: LMOD_XX1:4

for M, N being AbGroup
for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,g) = (ADD (M,N)) . (g,f)