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