theorem Th52: :: AFVECT0:52

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
for o being Element of (AV ADG) st ( for x being Element of ADG holds f . x = o9 + x ) & o = o9 holds
for a, b being Element of ADG holds
( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )