let R be 0 -characteristic Ring; :: thesis: R is infinite
set f = canHom_Int R;
dom (canHom_Int R) = the carrier of INT.Ring by FUNCT_2:def 1;
then rng (canHom_Int R) is infinite by CARD_1:59;
hence R is infinite ; :: thesis: verum