let R be Ring; :: thesis: for n being Nat holds n -invertible_Matrices_over R is matrix_mult (n,R) -binopclosed
let n be Nat; :: thesis: n -invertible_Matrices_over R is matrix_mult (n,R) -binopclosed
set U = n -invertible_Matrices_over R;
set V = n -Matrices_over R;
for x being set st x in [:(n -invertible_Matrices_over R),(n -invertible_Matrices_over R):] holds
(matrix_mult (n,R)) . x in n -invertible_Matrices_over R

proof

let x be set ; :: thesis: ( x in [:(n -invertible_Matrices_over R),(n -invertible_Matrices_over R):] implies (matrix_mult (n,R)) . x in n -invertible_Matrices_over R )
assume x in [:(n -invertible_Matrices_over R),(n -invertible_Matrices_over R):] ; :: thesis: (matrix_mult (n,R)) . x in n -invertible_Matrices_over R
then consider a, b being object such that
A1: ( a in n -invertible_Matrices_over R & b in n -invertible_Matrices_over R & x = [a,b] ) by ZFMISC_1:def 2;
reconsider A = a, B = b as Element of n -Matrices_over R by A1;
A2: A * B is invertible Matrix of n,R

proof

reconsider X = A, Y = B as invertible Matrix of n,R by A1, Th145;
( X * Y is invertible & (X * Y) ~ = (Y ~) * (X ~) ) by MATRIX_6:36;
hence A * B is invertible Matrix of n,R ; :: thesis: verum

end;

(matrix_mult (n,R)) . x = (matrix_mult (n,R)) . (A,B) by A1
.= A * B by Def5 ;
hence (matrix_mult (n,R)) . x in n -invertible_Matrices_over R by A2, Th145; :: thesis: verum

end;

hence n -invertible_Matrices_over R is matrix_mult (n,R) -binopclosed by REALSET1:def 1; :: thesis: verum