let R be Ring; :: thesis: ( Char R = 0 iff canHom_Int R is monomorphism )
set f = canHom_Int R;
( canHom_Int R is monomorphism iff ker (canHom_Int R) = {(0. INT.Ring)} ) by RING_2:12;
then ( canHom_Int R is monomorphism iff ker (canHom_Int R) = {(0. INT.Ring)} -Ideal ) by IDEAL_1:47;
hence ( Char R = 0 iff canHom_Int R is monomorphism ) by Th81; :: thesis: verum