let R be Ring; :: thesis: for S being R -homomorphic Ring holds Char S divides Char R
let S be R -homomorphic Ring; :: thesis: Char S divides 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 Homomorphism of R,S * (canHom_Int R) = canHom_Int S by Th83;
then ker (canHom_Int R) c= ker (canHom_Int S) by Th68;
then {m1} -Ideal c= ker (canHom_Int S) by Th81;
then {m1} -Ideal c= {n1} -Ideal by Th81;
then n1 divides m1 by RING_2:19;
hence Char S divides Char R by Lm3; :: thesis: verum