:: deftheorem HDef6 defines * ZMODLAT1:def 20 :
for V being non empty ModuleStr over INT.Ring
for v being Element of F_Real
for f, b₄ being FrFunctional of V holds
( b₄ = v * f iff for x being Element of V holds b₄ . x = v * (f . x) );