let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being Homomorphism of R,S
for a being Element of (Image f) ex x being Element of R st f . x = a
let S be R -homomorphic Ring; :: thesis: for f being Homomorphism of R,S
for a being Element of (Image f) ex x being Element of R st f . x = a
let f be Homomorphism of R,S; :: thesis: for a being Element of (Image f) ex x being Element of R st f . x = a
let a be Element of (Image f); :: thesis: ex x being Element of R st f . x = a
the carrier of (Image f) = rng f by defim;
then ex x being object st
( x in dom f & f . x = a ) by FUNCT_1:def 3;
hence ex x being Element of R st f . x = a ; :: thesis: verum