let R be Ring; :: thesis: for X, Y being LeftMod of R
for L being linear-transformation of X,Y holds L . (0. X) = 0. Y
let X, Y be LeftMod of R; :: thesis: for L being linear-transformation of X,Y holds L . (0. X) = 0. Y
let L be linear-transformation of X,Y; :: thesis: L . (0. X) = 0. Y
thus L . (0. X) = L . ((0. R) * (0. X)) by VECTSP_1:14
.= (0. R) * (L . (0. X)) by MOD_2:def 2
.= 0. Y by VECTSP_1:14 ; :: thesis: verum