theorem Th1: :: LMODFREE:1

for R being Ring
for X being set
for f, g, h being Element of Funcs (X, the carrier of R) holds
( h = (ADD (X,R)) . (f,g) iff for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x)) )