theorem :: MATGRP_0:157

for R being Ring
for n being Nat holds the strict b₂,b₁ -linear general Group = GL (n,R) by Th176;