take ZeroMap V,W ; :: thesis: ( ( for x, y being Vector of V holds (ZeroMap V,W) . (x + y) = ((ZeroMap V,W) . x) + ((ZeroMap V,W) . y) ) & ( for a being Scalar of K
for x being Vector of V holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x) ) )
thus ( ( for x, y being Vector of V holds (ZeroMap V,W) . (x + y) = ((ZeroMap V,W) . x) + ((ZeroMap V,W) . y) ) & ( for a being Scalar of K
for x being Vector of V holds (ZeroMap V,W) . (a * x) = (J . a) * ((ZeroMap V,W) . x) ) ) by Lm18, Lm19; :: thesis: verum