let R be Ring; :: thesis: for V, W being LeftMod of R
for f being linear-transformation of V,W holds the carrier of (ker f) = f " {(0. W)}
let V, W be LeftMod of R; :: thesis: for f being linear-transformation of V,W holds the carrier of (ker f) = f " {(0. W)}
let f be linear-transformation of V,W; :: thesis: the carrier of (ker f) = f " {(0. W)}
A0: [#] (ker f) = { u where u is Element of V : f . u = 0. W } by RANKNULL:def 1;
for x being object holds
( x in the carrier of (ker f) iff x in f " {(0. W)} )

proof

let x be object ; :: thesis: ( x in the carrier of (ker f) iff x in f " {(0. W)} )

hereby :: thesis: ( x in f " {(0. W)} implies x in the carrier of (ker f) )

assume x in the carrier of (ker f) ; :: thesis: x in f " {(0. W)}
then consider v being Vector of V such that
A2: ( x = v & f . v = 0. W ) by A0;
f . x in {(0. W)} by A2, TARSKI:def 1;
hence x in f " {(0. W)} by FUNCT_2:38, A2; :: thesis: verum

end;

assume A11: x in f " {(0. W)} ; :: thesis: x in the carrier of (ker f)
then A1: ( x in the carrier of V & f . x in {(0. W)} ) by FUNCT_2:38;
reconsider v = x as Vector of V by A11;
f . v = 0. W by A1, TARSKI:def 1;
hence x in the carrier of (ker f) by A0; :: thesis: verum

end;

hence the carrier of (ker f) = f " {(0. W)} by TARSKI:2; :: thesis: verum