let K, L be Ring; :: thesis: for J being Function of K,L
for V being LeftMod of K
for W being LeftMod of L holds ZeroMap V,W is Homomorphism of J,V,W
let J be Function of K,L; :: thesis: for V being LeftMod of K
for W being LeftMod of L holds ZeroMap V,W is Homomorphism of J,V,W
let V be LeftMod of K; :: thesis: for W being LeftMod of L holds ZeroMap V,W is Homomorphism of J,V,W
let W be LeftMod of L; :: thesis: ZeroMap V,W is Homomorphism of J,V,W
set z = ZeroMap V,W;
( ( for x, y being Vector of V holds (ZeroMap V,W) . (x + y) = ((ZeroMap V,W) . x) + ((ZeroMap V,W) . y) ) & ( for a being Scalar of K
for x being Vector of V holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x) ) ) by Lm18, Lm19;
hence ZeroMap V,W is Homomorphism of J,V,W by Def24; :: thesis: verum