let F be Field; :: thesis: for V, W being VectSp of
for T being linear-transformation of V,W
for x being Element of holds T . x = 0. W
let V, W be VectSp of ; :: thesis: for T being linear-transformation of V,W
for x being Element of holds T . x = 0. W
let T be linear-transformation of V,W; :: thesis: for x being Element of holds T . x = 0. W
let x be Element of ; :: thesis: T . x = 0. W
reconsider y = x as Element of by VECTSP_4:18;
y in ker T by STRUCT_0:def 5;
hence T . x = 0. W by Th10; :: thesis: verum