let F be Field; :: 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) by STRUCT_0:def 5;
[#] (ker T) = { u where u is Element of V : T . u = 0. W } by Def1;
then consider u being Element of V such that
A2: u = x and
A3: T . u = 0. W by A1;
thus T . x = 0. W by A2, A3; :: 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 by STRUCT_0:def 5; :: thesis: verum