let F be Ring; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W holds T . (0. V) = 0. W
let V, W be VectSp of F; :: 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. 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 T . (0. V) = 0. W ; :: thesis: verum