let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being Homomorphism of R,S holds 1. S in rng f
let S be R -homomorphic Ring; :: thesis: for f being Homomorphism of R,S holds 1. S in rng f
let f be Homomorphism of R,S; :: thesis: 1. S in rng f
A: f . (1_ R) = 1_ S by GROUP_1:def 13
.= 1. S ;
dom f = the carrier of R by FUNCT_2:def 1;
hence 1. S in rng f by A, FUNCT_1:def 3; :: thesis: verum