let R be Ring; :: thesis: for n being Nat holds inverse_op (GL (n,R)) = matrix_inv (n,R)
let n be Nat; :: thesis: inverse_op (GL (n,R)) = matrix_inv (n,R)
A1: dom (inverse_op (GL (n,R))) = the carrier of (GL (n,R)) by FUNCT_2:def 1
.= n -invertible_Matrices_over R by Th146
.= dom (matrix_inv (n,R)) by FUNCT_2:def 1 ;
for x being object st x in dom (matrix_inv (n,R)) holds
(matrix_inv (n,R)) . x = (inverse_op (GL (n,R))) . x

proof

let x be object ; :: thesis: ( x in dom (matrix_inv (n,R)) implies (matrix_inv (n,R)) . x = (inverse_op (GL (n,R))) . x )
assume A2: x in dom (matrix_inv (n,R)) ; :: thesis: (matrix_inv (n,R)) . x = (inverse_op (GL (n,R))) . x
then reconsider g = x as Element of (GL (n,R)) by A1;
reconsider X = g as invertible Matrix of n,R by Th126;
reconsider M = x as Element of n -invertible_Matrices_over R by A2;
thus (inverse_op (GL (n,R))) . x = g " by GROUP_1:def 6
.= X ~ by Th131
.= (matrix_inv (n,R)) . M by Def12
.= (matrix_inv (n,R)) . x ; :: thesis: verum

end;

hence inverse_op (GL (n,R)) = matrix_inv (n,R) by A1, FUNCT_1:2; :: thesis: verum