:: deftheorem HDef3 defines + ZMODLAT1:def 17 :
for V being non empty ModuleStr over INT.Ring
for f, g, b₄ being FrFunctional of V holds
( b₄ = f + g iff for x being Element of V holds b₄ . x = (f . x) + (g . x) );