let ADG be Proper_Uniquely_Two_Divisible_Group; :: thesis: for f being Function of the carrier of ADG,the carrier of ADG
for o' being Element of
for o being Element of st ( for b being Element of holds f . b = o' + 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 o' being Element of
for o being Element of st ( for b being Element of holds f . b = o' + 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 o' be Element of ; :: thesis: for o being Element of st ( for b being Element of holds f . b = o' + b ) holds
rng f = the carrier of (GroupVect (AV ADG),o)
let o be Element of ; :: thesis: ( ( for b being Element of holds f . b = o' + b ) implies rng f = the carrier of (GroupVect (AV ADG),o) )
assume A2: for b being Element of holds f . b = o' + 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 y' = y as Element of the carrier of ADG ;
set x' = y' - o';
f . (y' - o') = o' + ((- o') + y') by A2
.= (o' + (- o')) + y' by RLVECT_1:def 6
.= y' + (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