let L, K be Ring; :: thesis: for J being Function of K,L
for V being LeftMod of
for W being LeftMod of
for a being Scalar of
for x being Vector of holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x)
let J be Function of K,L; :: thesis: for V being LeftMod of
for W being LeftMod of
for a being Scalar of
for x being Vector of holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x)
let V be LeftMod of ; :: thesis: for W being LeftMod of
for a being Scalar of
for x being Vector of holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x)
let W be LeftMod of ; :: thesis: for a being Scalar of
for x being Vector of holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x)
let a be Scalar of ; :: thesis: for x being Vector of holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x)
let x be Vector of ; :: thesis: (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x)
set z = ZeroMap V,W;
( (ZeroMap V,W) . (a * x) = 0. W & (ZeroMap V,W) . x = 0. W ) by FUNCOP_1:13;
hence (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x) by VECTSP_1:59; :: thesis: verum