let a be Scalar of R; :: according to MOD_2:def 2 :: 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)
set f = ZeroMap (G,H);
( (ZeroMap (G,H)) . (a * x) = 0. H & (ZeroMap (G,H)) . x = 0. H ) by FUNCOP_1:7;
hence (ZeroMap (G,H)) . (a * x) = a * ((ZeroMap (G,H)) . x) by VECTSP_1:14; :: thesis: verum