theorem :: MATGRP_0:150

for R being Ring
for n being Nat holds the multF of (GL (n,R)) = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) by Th146;