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;

hereby :: according to RLVECT_1:def 2 :: thesis: ( FAdj (F,T) is add-associative & FAdj (F,T) is right_zeroed & FAdj (F,T) is right_complementable )

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

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( FAdj (F,T) is right_zeroed & FAdj (F,T) is right_complementable )

let x, y, z be Element of (FAdj (F,T)); :: thesis: (x + y) + z = x + (y + z)
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: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: FAdj (F,T) is right_complementable

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

end;

let x be Element of (FAdj (F,T)); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
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 ;

now :: thesis: 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: ( F is Subfield of U & T is Subset of U implies - x1 in U )
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis: - x1 in U
then x1 in U by A5;
then reconsider t = x1 as Element of U ;
- t = - x1 by GAUSSINT:19;
hence - x1 in U ; :: thesis: verum

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: x + y = 0. (FAdj (F,T))
thus x + y = a + (- x1) by Lm11f
.= 0. (FAdj (F,T)) by A1, A4, RLVECT_1:5 ; :: thesis: verum