let R be Ring; :: thesis: for n being Nat holds the carrier of (GL (n,R)) = n -invertible_Matrices_over R
let n be Nat; :: thesis: the carrier of (GL (n,R)) = n -invertible_Matrices_over R
for x being object holds
( x in the carrier of (GL (n,R)) iff x in n -invertible_Matrices_over R )

proof

let x be object ; :: thesis: ( x in the carrier of (GL (n,R)) iff x in n -invertible_Matrices_over 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;
hence ( x in the carrier of (GL (n,R)) iff x in n -invertible_Matrices_over R ) by Th145; :: thesis: verum

end;

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