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 :: thesis: for y being object st y in the carrier of ADG holds
y in rng f
let y be object ; :: 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 3
.= y9 + (0. ADG) by RLVECT_1:5
.= y by RLVECT_1:4 ;
hence y in rng f by A1, FUNCT_1:def 3; :: 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:4;
hence rng f = the carrier of (GroupVect ((AV ADG),o)) by A3, XBOOLE_0:def 10; :: thesis: verum