:: deftheorem Def10 defines "**" HILB10_7:def 10 :
for D being non empty set
for B being BinOp of D
for F being b₁ * -valued Function
for b₄ being Function of (dom F),D holds
( b₄ = B "**" F iff for x being object st x in dom F holds
b₄ . x = B "**" (F . x) );