let K, L be Ring; :: thesis: for J being Function of K,L

for V being LeftMod of K

for W being LeftMod of L

for a being Scalar of K

for x being Vector of V 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 K

for W being LeftMod of L

for a being Scalar of K

for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let V be LeftMod of K; :: thesis: for W being LeftMod of L

for a being Scalar of K

for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let W be LeftMod of L; :: thesis: for a being Scalar of K

for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let a be Scalar of K; :: thesis: for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let x be Vector of V; :: 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:7;

hence (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x) by VECTSP_1:14; :: thesis: verum

for V being LeftMod of K

for W being LeftMod of L

for a being Scalar of K

for x being Vector of V 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 K

for W being LeftMod of L

for a being Scalar of K

for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let V be LeftMod of K; :: thesis: for W being LeftMod of L

for a being Scalar of K

for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let W be LeftMod of L; :: thesis: for a being Scalar of K

for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let a be Scalar of K; :: thesis: for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)

let x be Vector of V; :: 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:7;

hence (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x) by VECTSP_1:14; :: thesis: verum