take canHom_Int R ; :: thesis: ( canHom_Int R is additive & canHom_Int R is multiplicative & canHom_Int R is unity-preserving & canHom_Int R is monomorphism )
thus ( canHom_Int R is additive & canHom_Int R is multiplicative & canHom_Int R is unity-preserving & canHom_Int R is monomorphism ) ; :: thesis: verum