:: deftheorem defines scalar-linear FVALUAT1:def 16 :
for R being Ring
for M1, M2 being RightMod of R
for h being Function of M1,M2 holds
( h is scalar-linear iff for x being Element of M1
for r being Element of R holds h . (x * r) = (h . x) * r );