theorem Th156: :: MATGRP_0:136

for R being Ring
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_a_unity & F is associative & F is having_an_inverseOp )