let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being Homomorphism of R,S
for a, b being Element of (Image f)
for x, y being Element of S st a = x & b = y holds
( a + b = x + y & a * b = x * y )
let S be R -homomorphic Ring; :: thesis: for f being Homomorphism of R,S
for a, b being Element of (Image f)
for x, y being Element of S st a = x & b = y holds
( a + b = x + y & a * b = x * y )
let f be Homomorphism of R,S; :: thesis: for a, b being Element of (Image f)
for x, y being Element of S st a = x & b = y holds
( a + b = x + y & a * b = x * y )
let a, b be Element of (Image f); :: thesis: for x, y being Element of S st a = x & b = y holds
( a + b = x + y & a * b = x * y )
let x, y be Element of S; :: thesis: ( a = x & b = y implies ( a + b = x + y & a * b = x * y ) )
set I = Image f;
the carrier of (Image f) = rng f by defim;
then A1: [a,b] in [:(rng f),(rng f):] by ZFMISC_1:def 2;
assume AS: ( a = x & b = y ) ; :: thesis: ( a + b = x + y & a * b = x * y )
the addF of (Image f) . (a,b) = ( the addF of S || (rng f)) . (a,b) by defim
.= the addF of S . (x,y) by AS, A1, FUNCT_1:49 ;
hence a + b = x + y ; :: thesis: a * b = x * y
the multF of (Image f) . (a,b) = ( the multF of S || (rng f)) . (a,b) by defim
.= the multF of S . (x,y) by AS, A1, FUNCT_1:49 ;
hence a * b = x * y ; :: thesis: verum