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 Lm16, Lm17;

hence ZeroMap (V,W) is Homomorphism of J,V,W by Def17; :: thesis: verum

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 Lm16, Lm17;

hence ZeroMap (V,W) is Homomorphism of J,V,W by Def17; :: thesis: verum