:: deftheorem Def16 defines Ker GROUP_23:def 17 :
for I being non empty set
for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2
for b₅ being componentwise_strict normal Subgroup-Family of F1 holds
( b₅ = Ker f iff for i being Element of I holds b₅ . i = Ker (f . i) );