let V, W be Z_Module; :: thesis: for T being linear-transformation of V,W holds T . (0. V) = 0. W
let T be linear-transformation of V,W; :: thesis: T . (0. V) = 0. W
0. V = (0. INT.Ring) * (0. V) by ZMODUL01:1;
then T . (0. V) = (0. INT.Ring) * (T . (0. V)) by MOD_2:def 2
.= 0. W by ZMODUL01:1 ;
hence T . (0. V) = 0. W ; :: thesis: verum