let R be Ring; :: thesis: for G, H being LeftMod of holds ZeroMap G,H is linear
let G, H be LeftMod of ; :: thesis: ZeroMap G,H is linear
set f = ZeroMap G,H;
reconsider G' = G, H' = H as AbGroup ;
A1: for a being Scalar of
for x being Vector of holds (ZeroMap G,H) . (a * x) = a * ((ZeroMap G,H) . x)

proof

let a be Scalar of ; :: thesis: for x being Vector of holds (ZeroMap G,H) . (a * x) = a * ((ZeroMap G,H) . x)
let x be Vector of ; :: 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;

ZeroMap G',H' is additive by GRCAT_1:16;
then for x, y being Vector of holds (ZeroMap G,H) . (x + y) = ((ZeroMap G,H) . x) + ((ZeroMap G,H) . y) by GRCAT_1:def 13;
hence ZeroMap G,H is linear by A1, Def5; :: thesis: verum