Char R = 0 by Def6;
hence canHom_Int R is monomorphism by Th82; :: thesis: verum