:: deftheorem Def29 defines Ker AIMLOOP:def 31 :
for Q, Q2 being multLoop
for f being homomorphic Function of Q,Q2
for b₄ being Subset of Q holds
( b₄ = Ker f iff for x being Element of Q holds
( x in b₄ iff f . x = 1. Q2 ) );