let F be Ring; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
let T be linear-transformation of V,W; :: thesis: for x being Element of (ker T) holds T . x = 0. W
let x be Element of (ker T); :: thesis: T . x = 0. W
reconsider y = x as Element of V by VECTSP_4:10;
y in ker T ;
hence T . x = 0. W by Th10; :: thesis: verum