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

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