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 st ( for b being Element of ADG holds f . b = o9 + b ) holds
f is one-to-one
let f be Function of the carrier of ADG, the carrier of ADG; :: thesis: for o9 being Element of ADG st ( for b being Element of ADG holds f . b = o9 + b ) holds
f is one-to-one
let o9 be Element of ADG; :: thesis: ( ( for b being Element of ADG holds f . b = o9 + b ) implies f is one-to-one )
assume A1: for b being Element of ADG holds f . b = o9 + b ; :: thesis: f is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x19 = x1, x29 = x2 as Element of ADG by A2, FUNCT_2:def 1;
o9 + x29 = f . x19 by A1, A3
.= o9 + x19 by A1 ;
hence x1 = x2 by RLVECT_1:8; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 4; :: thesis: verum