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
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) )
let f be Function of the carrier of ADG, the carrier of ADG; :: thesis: 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) )
let o9 be Element of ADG; :: thesis: 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) )
let o be Element of (AV ADG); :: thesis: ( ( for x being Element of ADG holds f . x = o9 + x ) & o = o9 implies 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) ) )
assume that
A1: for x being Element of ADG holds f . x = o9 + x and
A2: o = o9 ; :: thesis: 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) )
let a, b be Element of ADG; :: thesis: ( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
set a9 = f . a;
set b9 = f . b;
A3: AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #) by TDGROUP:def 3;
then reconsider a99 = f . a, b99 = f . b as Element of (AV ADG) ;
thus f . (a + b) = (Padd o) . ((f . a),(f . b)) :: thesis: ( f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )

proof

A4: (Padd o) . ((f . a),(f . b)) = Padd (o,a99,b99) by Def6;
then reconsider c99 = (Padd o) . ((f . a),(f . b)) as Element of (AV ADG) ;
reconsider c9 = c99 as Element of ADG by A3;
o,a99 // b99,c99 by A4, Def5;
then [[o9,(f . a)],[(f . b),c9]] in CONGRD ADG by A2, A3, ANALOAF:def 2;
then A5: o9 + c9 = (f . a) + (f . b) by TDGROUP:def 2;
( f . a = o9 + a & f . b = o9 + b ) by A1;
then o9 + c9 = o9 + ((a + o9) + b) by A5, RLVECT_1:def 3
.= o9 + (o9 + (a + b)) by RLVECT_1:def 3 ;
then c9 = o9 + (a + b) by RLVECT_1:8
.= f . (a + b) by A1 ;
hence f . (a + b) = (Padd o) . ((f . a),(f . b)) ; :: thesis: verum

end;

f . (0. ADG) = o9 + (0. ADG) by A1
.= 0. (GroupVect ((AV ADG),o)) by A2, RLVECT_1:4 ;
hence f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) ; :: thesis: f . (- a) = (Pcom o) . (f . a)
thus f . (- a) = (Pcom o) . (f . a) :: thesis: verum

proof

A6: (Pcom o) . (f . a) = Pcom (o,a99) by Def7;
then reconsider c99 = (Pcom o) . (f . a) as Element of (AV ADG) ;
reconsider c9 = c99 as Element of ADG by A3;
a99,o // o,c99 by A6, Lm1;
then [[(f . a),o9],[o9,c9]] in CONGRD ADG by A2, A3, ANALOAF:def 2;
then (f . a) + c9 = o9 + o9 by TDGROUP:def 2;
then A7: o9 + o9 = (o9 + a) + c9 by A1
.= o9 + (a + c9) by RLVECT_1:def 3 ;
f . (- a) = o9 + (- a) by A1
.= (c9 + a) + (- a) by A7, RLVECT_1:8
.= c9 + (a + (- a)) by RLVECT_1:def 3
.= c9 + (0. ADG) by RLVECT_1:5
.= c9 by RLVECT_1:4 ;
hence f . (- a) = (Pcom o) . (f . a) ; :: thesis: verum

end;