let R be Ring; :: thesis: for S being R -monomorphic Ring holds Char S = Char R
let S be R -monomorphic Ring; :: thesis: Char S = Char R
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;

per cases ( Char R = 0 or Char R > 0 ) ;

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

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

now :: thesis: not Char S <> 0. INT.Ring

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

end;

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

end;

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

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: verum

end;

end;