theorem :: ZMODLAT1:49

for V being non empty ModuleStr over INT.Ring
for f being FrFunctional of V holds f + (0FrFunctional V) = f