theorem :: MOD_4:42
for K being Ring
for V, W being LeftMod of K
for f being Function of V,W holds
( f is Homomorphism of V,W iff ( ( for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of K
for x being Vector of V holds f . (a * x) = a * (f . x) ) ) )