theorem :: MATGRP_0:147

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds 1_ G = 1. (R,n)