:: deftheorem Def10 defines * AOFA_I00:def 10 :
for X being non empty set
for f being Function of X,INT
for x being Integer
for b₄ being Function of X,INT holds
( b₄ = f * x iff for s being Element of X holds b₄ . s = (f . s) * x );