:: deftheorem ch defines canHom RING_2:def 7 :
for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S
for b₄ being Function of (R / (ker f)),(Image f) holds
( b₄ = canHom f iff for a being Element of R holds b₄ . (Class ((EqRel (R,(ker f))),a)) = f . a );