let R, S be AbGroup; 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 A1:
a in rng f
and A2:
b in rng f
and A3:
x = [a,b]
by ZFMISC_1:def 2;
consider a1 being
Element of
S such that A4:
(
a1 = a &
a1 in rng f )
by A1;
consider x1 being
object such that A5:
(
x1 in dom f &
f . x1 = a1 )
by A4, FUNCT_1:def 3;
reconsider x1 =
x1 as
Element of
R by A5;
consider a2 being
Element of
S such that A6:
(
a2 = b &
a2 in rng f )
by A2;
consider x2 being
object such that A7:
(
x2 in dom f &
f . x2 = a2 )
by A6, FUNCT_1:def 3;
reconsider x2 =
x2 as
Element of
R by A7;
A8:
dom f = the
carrier of
R
by FUNCT_2:def 1;
f . (x1 + x2) =
a1 + a2
by A7, A5, VECTSP_1:def 20
.=
the
addF of
S . x
by A3, A4, A6
;
hence
the
addF of
S . x in rng f
by A8, FUNCT_1:def 3;
verum end;
hence
rng f is Preserv of the addF of S
by REALSET1:def 1; verum