let R be Ring; for S being R -homomorphic Ring
for f being Homomorphism of R,S holds rng f is Preserv of the addF of S
let S be R -homomorphic Ring; for f being Homomorphism of R,S holds rng f is Preserv of the addF of S
let f be Homomorphism of R,S; rng f is Preserv of the addF of S
set F = rng f;
set A = the addF of S;
now for x being set st x in [:(rng f),(rng f):] holds
the addF of S . x in rng flet x be
set ;
( x in [:(rng f),(rng f):] implies the addF of S . x in rng f )assume
x in [:(rng f),(rng f):]
;
the addF of S . x in rng fthen consider a,
b being
object such that A2:
a in rng f
and A3:
b in rng f
and A4:
x = [a,b]
by ZFMISC_1:def 2;
consider a1 being
Element of
S such that A5:
(
a1 = a &
a1 in rng f )
by A2;
consider x1 being
object such that A6:
(
x1 in dom f &
f . x1 = a1 )
by A5, FUNCT_1:def 3;
reconsider x1 =
x1 as
Element of
R by A6;
consider a2 being
Element of
S such that A7:
(
a2 = b &
a2 in rng f )
by A3;
consider x2 being
object such that A8:
(
x2 in dom f &
f . x2 = a2 )
by A7, FUNCT_1:def 3;
reconsider x2 =
x2 as
Element of
R by A8;
A9:
dom f = the
carrier of
R
by FUNCT_2:def 1;
f . (x1 + x2) =
a1 + a2
by A8, A6, VECTSP_1:def 20
.=
the
addF of
S . x
by A4, A5, A7
;
hence
the
addF of
S . x in rng f
by A9, FUNCT_1:def 3;
verum end;
hence
rng f is Preserv of the addF of S
by REALSET1:def 1; verum