let R be Ring; :: thesis: for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
F is having_an_inverseOp
let n be Nat; :: thesis: for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
F is having_an_inverseOp
let F be BinOp of (n -invertible_Matrices_over R); :: thesis: ( F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) implies F is having_an_inverseOp )
assume F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) ; :: thesis: F is having_an_inverseOp
then matrix_inv (n,R) is_an_inverseOp_wrt F by Th154;
hence F is having_an_inverseOp by FINSEQOP:def 2; :: thesis: verum