for ADG being Proper_Uniquely_Two_Divisible_Group
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