set P = RAdj (R,T);
A1: 0. (RAdj (R,T)) = 0. S by dRA;
A2: the carrier of (RAdj (R,T)) = carrierRA T by dRA;

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

let x, y be Element of (RAdj (R,T)); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of S by Lm10;
thus x + y = a + b by Lm11
.= y + x by Lm11 ; :: thesis: verum

end;

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

let x, y, z be Element of (RAdj (R,T)); :: thesis: (x + y) + z = x + (y + z)
reconsider a = x, b = y, c = z as Element of S by Lm10;
A3: y + z = b + c by Lm11;
x + y = a + b by Lm11;
hence (x + y) + z = (a + b) + c by Lm11
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A3, Lm11 ;
:: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: RAdj (R,T) is right_complementable

let x be Element of (RAdj (R,T)); :: thesis: x + (0. (RAdj (R,T))) = x
reconsider a = x as Element of S by Lm10;
thus x + (0. (RAdj (R,T))) = a + (0. S) by A1, Lm11
.= x ; :: thesis: verum

end;

let x be Element of (RAdj (R,T)); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider a = x as Element of S by Lm10;
x in carrierRA T by A2;
then consider x1 being Element of S such that
A4: x = x1 and
A5: for U being Subring of S st R is Subring of U & T is Subset of U holds
x1 in U ;

now :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
- x1 in U

let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies - x1 in U )
assume ( R is Subring 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 Th19;
hence - x1 in U ; :: thesis: verum

end;

then - x1 in carrierRA T ;
then reconsider y = - x1 as Element of (RAdj (R,T)) by dRA;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (RAdj (R,T))
thus x + y = a + (- x1) by Lm11
.= 0. (RAdj (R,T)) by A1, A4, RLVECT_1:5 ; :: thesis: verum