let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear Group holds 1_ G = 1_ (GL (n,R))
let n be Nat; :: thesis: for G being n,R -linear Group holds 1_ G = 1_ (GL (n,R))
let G be n,R -linear Group; :: thesis: 1_ G = 1_ (GL (n,R))
A1: multMagma(# the carrier of G, the multF of G #) is Subgroup of GL (n,R) by Def13;
( the carrier of multMagma(# the carrier of G, the multF of G #) = the carrier of G & the multF of multMagma(# the carrier of G, the multF of G #) = the multF of G || the carrier of multMagma(# the carrier of G, the multF of G #) ) ;
then multMagma(# the carrier of G, the multF of G #) is Subgroup of G by GROUP_2:def 5;
hence 1_ G = 1_ multMagma(# the carrier of G, the multF of G #) by GROUP_2:44
.= 1_ (GL (n,R)) by A1, GROUP_2:44 ;
:: thesis: verum