set P = RAdj (R,T);
A1: 1. (RAdj (R,T)) = 1. S by dRA;

now :: thesis: for x, y, z being Element of (RAdj (R,T)) holds (x * y) * z = x * (y * z)

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 Lm12;
x * y = a * b by Lm12;
hence (x * y) * z = (a * b) * c by Lm12
.= a * (b * c) by GROUP_1:def 3
.= x * (y * z) by A3, Lm12 ;
:: thesis: verum

end;

hence RAdj (R,T) is associative ; :: thesis: ( RAdj (R,T) is well-unital & RAdj (R,T) is distributive )

now :: thesis: for x being Element of (RAdj (R,T)) holds
( x * (1. (RAdj (R,T))) = x & (1. (RAdj (R,T))) * x = x )

let x be Element of (RAdj (R,T)); :: thesis: ( x * (1. (RAdj (R,T))) = x & (1. (RAdj (R,T))) * x = x )
reconsider a = x as Element of S by Lm10;
thus x * (1. (RAdj (R,T))) = a * (1. S) by A1, Lm12
.= x ; :: thesis: (1. (RAdj (R,T))) * x = x
thus (1. (RAdj (R,T))) * x = (1. S) * a by A1, Lm12
.= x ; :: thesis: verum

end;

hence RAdj (R,T) is well-unital ; :: thesis: RAdj (R,T) is distributive

now :: thesis: for x, y, z being Element of (RAdj (R,T)) holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )

let x, y, z be Element of (RAdj (R,T)); :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider a = x, b = y, c = z as Element of S by Lm10;
A4: ( a * b = x * y & a * c = x * z ) by Lm12;
A6: ( b * a = y * x & c * a = z * x ) by Lm12;
A5: y + z = b + c by Lm11;
hence x * (y + z) = a * (b + c) by Lm12
.= (a * b) + (a * c) by VECTSP_1:def 7
.= (x * y) + (x * z) by A4, Lm11 ;
:: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (b + c) * a by A5, Lm12
.= (b * a) + (c * a) by VECTSP_1:def 7
.= (y * x) + (z * x) by A6, Lm11 ; :: thesis: verum

end;

hence RAdj (R,T) is distributive ; :: thesis: verum