let V, W be Z_Module; :: thesis: for T being linear-transformation of V,W holds 0. V in ker T
let T be linear-transformation of V,W; :: thesis: 0. V in ker T
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 0. V in ker T by Th10; :: thesis: verum