let ADG be Proper_Uniquely_Two_Divisible_Group; :: thesis: for f being Function of the carrier of ADG,the carrier of ADG
for o9 being Element of ADG
for o being Element of (AV ADG) st ( for b being Element of ADG holds f . b = o9 + b ) holds
rng f = the carrier of (GroupVect (AV ADG),o)
let f be Function of the carrier of ADG,the carrier of ADG; :: thesis: for o9 being Element of ADG
for o being Element of (AV ADG) st ( for b being Element of ADG holds f . b = o9 + b ) holds
rng f = the carrier of (GroupVect (AV ADG),o)
set X = the carrier of ADG;
A1: the carrier of ADG = dom f by FUNCT_2:def 1;
let o9 be Element of ADG; :: thesis: for o being Element of (AV ADG) st ( for b being Element of ADG holds f . b = o9 + b ) holds
rng f = the carrier of (GroupVect (AV ADG),o)
let o be Element of (AV ADG); :: thesis: ( ( for b being Element of ADG holds f . b = o9 + b ) implies rng f = the carrier of (GroupVect (AV ADG),o) )
assume A2: for b being Element of ADG holds f . b = o9 + b ; :: thesis: rng f = the carrier of (GroupVect (AV ADG),o)

now

let y be set ; :: thesis: ( y in the carrier of ADG implies y in rng f )
assume y in the carrier of ADG ; :: thesis: y in rng f
then reconsider y9 = y as Element of the carrier of ADG ;
set x9 = y9 - o9;
f . (y9 - o9) = o9 + ((- o9) + y9) by A2
.= (o9 + (- o9)) + y9 by RLVECT_1:def 6
.= y9 + (0. ADG) by RLVECT_1:16
.= y by RLVECT_1:10 ;
hence y in rng f by A1, FUNCT_1:def 5; :: thesis: verum

end;

then A3: the carrier of ADG c= rng f by TARSKI:def 3;
( rng f c= the carrier of ADG & the carrier of ADG = the carrier of (GroupVect (AV ADG),o) ) by RELAT_1:def 19, TDGROUP:9;
hence rng f = the carrier of (GroupVect (AV ADG),o) by A3, XBOOLE_0:def 10; :: thesis: verum