:: deftheorem HDef4 defines - ZMODLAT1:def 18 :
for V being non empty ModuleStr over INT.Ring
for f, b₃ being FrFunctional of V holds
( b₃ = - f iff for x being Element of V holds b₃ . x = - (f . x) );