take
ZeroMap (V,W)
; ( ( 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 Lm16, Lm17; verum