let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear general Group holds the carrier of G = the carrier of (GL (n,R))
let n be Nat; :: thesis: for G being n,R -linear general Group holds the carrier of G = the carrier of (GL (n,R))
let G be n,R -linear general Group; :: thesis: the carrier of G = the carrier of (GL (n,R))
for x being object holds
( x in the carrier of G iff x in the carrier of (GL (n,R)) )

proof

let x be object ; :: thesis: ( x in the carrier of G iff x in the carrier of (GL (n,R)) )
( x is Element of (GL (n,R)) iff x in the carrier of (GL (n,R)) ) ;
then ( x in the carrier of (GL (n,R)) iff x is invertible Matrix of n,R ) by Th126;
then ( x in the carrier of (GL (n,R)) iff x in G ) by Def14;
hence ( x in the carrier of G iff x in the carrier of (GL (n,R)) ) by STRUCT_0:def 5; :: thesis: verum

end;

hence the carrier of G = the carrier of (GL (n,R)) by TARSKI:2; :: thesis: verum