:: deftheorem Def8 defines canHom_Int RING_3:def 8 :
for R being Ring
for b₂ being Function of INT.Ring,R holds
( b₂ = canHom_Int R iff for x being Element of INT.Ring holds b₂ . x = x '*' (1. R) );