:: deftheorem defmu defines '*' VECTSP13:def 13 :
for X being non empty set
for L being non empty multLoopStr
for f being Function of X,L
for a being Element of L
for b₅ being Function of X,L holds
( b₅ = a '*' f iff for x being Element of X holds b₅ . x = a * (f . x) );