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 V holds
( x in ker T iff 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 V holds
( x in ker T iff T . x = 0. W )
let T be linear-transformation of V,W; :: thesis: for x being Element of V holds
( x in ker T iff T . x = 0. W )
let x be Element of V; :: thesis: ( x in ker T iff T . x = 0. W )
thus ( x in ker T implies T . x = 0. W ) :: thesis: ( T . x = 0. W implies x in ker T )

proof

assume x in ker T ; :: thesis: T . x = 0. W
then A1: x in [#] (ker T) ;
[#] (ker T) = { u where u is Element of V : T . u = 0. W } by Def1;
then ex u being Element of V st
( u = x & T . u = 0. W ) by A1;
hence T . x = 0. W ; :: thesis: verum

end;

assume T . x = 0. W ; :: thesis: x in ker T
then x in { u where u is Element of V : T . u = 0. W } ;
then x in [#] (ker T) by Def1;
hence x in ker T ; :: thesis: verum