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:13;
( (ZeroMap V,W) . (x + y) = 0. W & (ZeroMap V,W) . x = 0. W ) by FUNCOP_1:13;
hence (ZeroMap V,W) . (x + y) = ((ZeroMap V,W) . x) + ((ZeroMap V,W) . y) by A1, RLVECT_1:def 7; :: thesis: verum

end;