let F be Ring; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V st T . x = T . y holds
x - y in ker T
let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W
for x, y being Element of V st T . x = T . y holds
x - y in ker T
let T be linear-transformation of V,W; :: thesis: for x, y being Element of V st T . x = T . y holds
x - y in ker T
let x, y be Element of V; :: thesis: ( T . x = T . y implies x - y in ker T )
assume A1: T . x = T . y ; :: thesis: x - y in ker T
T . (x - y) = (T . x) - (T . y) by Th8
.= 0. W by A1, VECTSP_1:19 ;
hence x - y in ker T by Th10; :: thesis: verum