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 ADG
for o being Element of (AV ADG) st ( for b being Element of ADG 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 ADG
for o being Element of (AV ADG) st ( for b being Element of ADG holds f . b = o' + b ) holds
rng f = the carrier of (GroupVect (AV ADG),o)
let o' be Element of ADG; :: thesis: for o being Element of (AV ADG) st ( for b being Element of ADG holds f . b = o' + 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 = o' + b ) implies rng f = the carrier of (GroupVect (AV ADG),o) )
assume A1: for b being Element of ADG holds f . b = o' + b ; :: thesis: rng f = the carrier of (GroupVect (AV ADG),o)
set X = the carrier of ADG;
A2: ( the carrier of ADG = dom f & rng f c= the carrier of ADG ) by FUNCT_2:def 1, RELAT_1:def 19;
A3: the carrier of ADG = the carrier of (GroupVect (AV ADG),o) by TDGROUP:9;

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 A1
.= (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 A2, FUNCT_1:def 5; :: thesis: verum

end;

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