let F be Ring; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W holds 0. V in ker T
let V, W be VectSp of F; :: 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. F) * (0. V) by VECTSP_1:14;
then T . (0. V) = (0. F) * (T . (0. V)) by MOD_2:def 2
.= 0. W by VECTSP_1:14 ;
hence 0. V in ker T by Th10; :: thesis: verum