set P = FAdj (F,T);
A1: 0. (FAdj (F,T)) = 0. E by dFA;
A2: the carrier of (FAdj (F,T)) = carrierFA T by dFA;

let x, y be Element of (FAdj (F,T)); :: thesis:
reconsider a = x, b = y as Element of E by Lm10f;
thus x + y = a + b by Lm11f
.= y + x by Lm11f ; :: thesis:

end;

let x, y, z be Element of (FAdj (F,T)); :: thesis:
reconsider a = x, b = y, c = z as Element of E by Lm10f;
A3: y + z = b + c by Lm11f;
x + y = a + b by Lm11f;
hence (x + y) + z = (a + b) + c by Lm11f
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A3, Lm11f ;
:: thesis:

end;

let x be Element of (FAdj (F,T)); :: thesis:
reconsider a = x as Element of E by Lm10f;
thus x + (0. (FAdj (F,T))) = a + (0. E) by A1, Lm11f
.= x ; :: thesis:

end;

let x be Element of (FAdj (F,T)); :: according to ALGSTR_0:def 16 :: thesis:
reconsider a = x as Element of E by Lm10f;
x in carrierFA T by A2;
then consider x1 being Element of E such that
A4: x = x1 and
A5: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x1 in U ;

let U be Subfield of E; :: thesis:
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis:
then x1 in U by A5;
then reconsider t = x1 as Element of U ;
- t = - x1 by GAUSSINT:19;
hence - x1 in U ; :: thesis:

end;

then - x1 in carrierFA T ;
then reconsider y = - x1 as Element of (FAdj (F,T)) by dFA;
take y ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + y = a + (- x1) by Lm11f
.= 0. (FAdj (F,T)) by A1, A4, RLVECT_1:5 ; :: thesis: