:: deftheorem defhomI defines canHom RING_2:def 5 :
for R being Ring
for I being Ideal of R
for b₃ being Function of R,(R / I) holds
( b₃ = canHom I iff for a being Element of R holds b₃ . a = Class ((EqRel (R,I)),a) );