let R be Ring; :: thesis:
let S be R -monomorphic Ring; :: thesis:
set n = Char S;
set m = Char R;
reconsider n1 = Char S, m1 = Char R as Element of INT.Ring by INT_1:def 2;
the Monomorphism of R,S * (canHom_Int R) = canHom_Int S by Th83;
then ker (canHom_Int R) = ker (canHom_Int S) by Th69;
then A1: {m1} -Ideal = ker (canHom_Int S) by Th81;
then A2: ( Char S divides Char R & Char R divides Char S ) by Th81;

suppose A3: Char R = 0 ; :: thesis:

then A4: {(0. INT.Ring)} = {m1} -Ideal by IDEAL_1:47
.= {n1} -Ideal by A1, Th81 ;

assume A5: Char S <> 0. INT.Ring ; :: thesis:
n1 in {n1} -Ideal by IDEAL_1:66;
hence contradiction by A5, A4, TARSKI:def 1; :: thesis:

end;

hence Char S = Char R by A3; :: thesis:

end;

suppose A6: Char R > 0 ; :: thesis:

consider u being Integer such that
A7: Char R = (Char S) * u by A2;
consider v being Integer such that
A8: Char S = (Char R) * v by A2;
Char R = ((Char R) * v) * u by A7, A8
.= (Char R) * (v * u) ;
then (Char R) / (Char R) = (v * u) * ((Char R) / (Char R)) by XCMPLX_1:74;
then (Char R) / (Char R) = (u * v) * 1 by A6, XCMPLX_1:60;
then A9: u * v = 1 by A6, XCMPLX_1:60;
u <> - 1 by A7, A6;
then ( u = 1 & v = 1 ) by A9, INT_1:9;
hence Char S = Char R by A7; :: thesis:

end;

end;