theorem Th5: :: LMODFREE:5

for R being Ring
for X being set
for v1, w1 being Element of Funcs (X, the carrier of R)
for v, w being Element of (FS_Funcs (X,R)) st v1 = v & w1 = w holds
v + w = (ADD (X,R)) . (v1,w1)