let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear Group holds 1_ G = 1. (R,n)
let n be Nat; :: thesis: for G being n,R -linear Group holds 1_ G = 1. (R,n)
let G be n,R -linear Group; :: thesis: 1_ G = 1. (R,n)
thus 1_ G = 1_ (GL (n,R)) by Th166
.= 1. (R,n) by Th130 ; :: thesis: verum