let R be Ring; :: thesis: R is INT.Ring -homomorphic
( canHom_Int R is additive & canHom_Int R is multiplicative & canHom_Int R is unity-preserving ) ;
hence R is INT.Ring -homomorphic ; :: thesis: verum