:: deftheorem defmu defines '*' VECTSP13:def 18 :
for X being non empty set
for R being non empty 1-sorted
for L being non empty ModuleStr over R
for f being Function of X,L
for a being Element of R
for b₆ being Function of X,L holds
( b₆ = a '*' f iff for x being Element of X holds b₆ . x = a * (f . x) );