:: deftheorem Def9 defines Ker GROUP_6:def 9 :
for G, H being Group
for g being Homomorphism of G,H
for b₄ being strict Subgroup of G holds
( b₄ = Ker g iff the carrier of b₄ = { a where a is Element of G : g . a = 1_ H } );