let X, Y be Z_Module; :: 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. INT.Ring) * (0. X)) by ZMODUL01:1
.= (0. INT.Ring) * (L . (0. X)) by MOD_2:def 2
.= 0. Y by ZMODUL01:1 ; :: thesis: verum