let K, L be Ring; :: thesis: for V being LeftMod of K
for W being LeftMod of L
for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y)
let V be LeftMod of K; :: thesis: for W being LeftMod of L
for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y)
let W be LeftMod of L; :: thesis: for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y)
set f = ZeroMap (V,W);
thus for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y) :: thesis: verum

proof

let x, y be Vector of V; :: thesis: (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y)
A1: (ZeroMap (V,W)) . y = 0. W by FUNCOP_1:7;
( (ZeroMap (V,W)) . (x + y) = 0. W & (ZeroMap (V,W)) . x = 0. W ) by FUNCOP_1:7;
hence (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y) by A1, RLVECT_1:def 4; :: thesis: verum

end;