let a be Scalar of R; :: according to MOD_2:def 3 :: 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:13;
hence (ZeroMap (G,H)) . (a * x) = a * ((ZeroMap (G,H)) . x) by VECTSP_1:59; :: thesis: verum