:: deftheorem Def48 defines QuotientHom AIMLOOP:def 50 :
for Q being multLoop
for N being normal SubLoop of Q
for b₃ being Function of Q,(Q _/_ N) holds
( b₃ = QuotientHom (Q,N) iff for x being Element of Q holds b₃ . x = x * N );