let ADG be Proper_Uniquely_Two_Divisible_Group; :: thesis:
let f be Function of the carrier of ADG,the carrier of ADG; :: thesis:
let o' be Element of ADG; :: thesis:
let o be Element of (AV ADG); :: thesis:
assume that
A1: for x being Element of ADG holds f . x = o' + x and
A2: o = o' ; :: thesis:
let a, b be Element of ADG; :: thesis:
set a' = f . a;
set b' = f . b;
A3: AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #) by TDGROUP:def 5;
then reconsider a'' = f . a, b'' = f . b as Element of (AV ADG) ;
thus f . (a + b) = (Padd o) . (f . a),(f . b) :: thesis:

proof

A4: (Padd o) . (f . a),(f . b) = Padd o,a'',b'' by Def7;
then reconsider c'' = (Padd o) . (f . a),(f . b) as Element of (AV ADG) ;
reconsider c' = c'' as Element of ADG by A3;
o,a'' // b'',c'' by A4, Def5;
then [[o',(f . a)],[(f . b),c']] in CONGRD ADG by A2, A3, ANALOAF:def 2;
then A5: o' + c' = (f . a) + (f . b) by TDGROUP:def 4;
( f . a = o' + a & f . b = o' + b ) by A1;
then o' + c' = o' + ((a + o') + b) by A5, RLVECT_1:def 6
.= o' + (o' + (a + b)) by RLVECT_1:def 6 ;
then c' = o' + (a + b) by RLVECT_1:21
.= f . (a + b) by A1 ;
hence f . (a + b) = (Padd o) . (f . a),(f . b) ; :: thesis:

end;

thus f . (0. ADG) = 0. (GroupVect (AV ADG),o) :: thesis:

proof

thus f . (0. ADG) = o' + (0. ADG) by A1
.= 0. (GroupVect (AV ADG),o) by A2, RLVECT_1:10 ; :: thesis:

end;

thus f . (- a) = (Pcom o) . (f . a) :: thesis:

proof

A6: (Pcom o) . (f . a) = Pcom o,a'' by Def8;
then reconsider c'' = (Pcom o) . (f . a) as Element of (AV ADG) ;
reconsider c' = c'' as Element of ADG by A3;
a'',o // o,c'' by A6, Lm1;
then [[(f . a),o'],[o',c']] in CONGRD ADG by A2, A3, ANALOAF:def 2;
then (f . a) + c' = o' + o' by TDGROUP:def 4;
then A7: o' + o' = (o' + a) + c' by A1
.= o' + (a + c') by RLVECT_1:def 6 ;
f . (- a) = o' + (- a) by A1
.= (c' + a) + (- a) by A7, RLVECT_1:21
.= c' + (a + (- a)) by RLVECT_1:def 6
.= c' + (0. ADG) by RLVECT_1:16
.= c' by RLVECT_1:10 ;
hence f . (- a) = (Pcom o) . (f . a) ; :: thesis:

end;