:: deftheorem Def6 defines * HAHNBAN1:def 6 :
for K being non empty multMagma
for V being non empty ModuleStr over K
for v being Element of K
for f, b₅ being Functional of V holds
( b₅ = v * f iff for x being Element of V holds b₅ . x = v * (f . x) );