theorem Th130: :: MATGRP_0:112

for R being Ring
for n being Nat holds 1_ (GL (n,R)) = 1. (R,n)