let R be Ring; :: thesis: for G, H being LeftMod of R holds ZeroMap G,H is linear
let G, H be LeftMod of R; :: thesis: ZeroMap G,H is linear
set f = ZeroMap G,H;
reconsider G' = G, H' = H as AbGroup ;
ZeroMap G',H' is additive by GRCAT_1:16;
then A1: for x, y being Vector of G holds (ZeroMap G,H) . (x + y) = ((ZeroMap G,H) . x) + ((ZeroMap G,H) . y) by GRCAT_1:def 13;
for a being Scalar of R
for x being Vector of G holds (ZeroMap G,H) . (a * x) = a * ((ZeroMap G,H) . x)

proof

let a be Scalar of R; :: thesis: for x being Vector of G holds (ZeroMap G,H) . (a * x) = a * ((ZeroMap G,H) . x)
let x be Vector of G; :: thesis: (ZeroMap G,H) . (a * x) = a * ((ZeroMap G,H) . x)
( (ZeroMap G,H) . (a * x) = 0. H & (ZeroMap G,H) . x = 0. H ) by FUNCOP_1:13;
hence (ZeroMap G,H) . (a * x) = a * ((ZeroMap G,H) . x) by VECTSP_1:59; :: thesis: verum

end;

hence ZeroMap G,H is linear by A1, Def5; :: thesis: verum