:: deftheorem Def1 defines ker ZMODUL05:def 4 :
for V, W being Z_Module
for T being linear-transformation of V,W
for b₄ being strict Submodule of V holds
( b₄ = ker T iff [#] b₄ = { u where u is Element of V : T . u = 0. W } );