let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear Group holds the carrier of G c= n -invertible_Matrices_over R
let n be Nat; :: thesis: for G being n,R -linear Group holds the carrier of G c= n -invertible_Matrices_over R
let G be n,R -linear Group; :: thesis: the carrier of G c= n -invertible_Matrices_over R
( the carrier of G c= the carrier of (GL (n,R)) & the carrier of (GL (n,R)) = n -invertible_Matrices_over R ) by Th146, Th164;
hence the carrier of G c= n -invertible_Matrices_over R ; :: thesis: verum