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

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 Lm12
.= b * a by GROUP_1:def 12
.= y * x by Lm12 ; :: thesis: verum

end;

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