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

now

let x1, x2 be set ; :: 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 x1' = x1, x2' = x2 as Element of ADG by A2, FUNCT_2:def 1;
o' + x2' = f . x1' by A1, A3
.= o' + x1' by A1 ;
hence x1 = x2 by RLVECT_1:21; :: thesis: verum

end;

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