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