:: deftheorem Def4 defines * MATRLIN:def 4 :
for K being non empty doubleLoopStr
for V1, V2 being non empty ModuleStr over K
for f being Function of V1,V2
for a being Element of K
for b₆ being Function of V1,V2 holds
( b₆ = a * f iff for v being Element of V1 holds b₆ . v = a * (f . v) );