let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear Group holds the multF of G = (matrix_mult (n,R)) || the carrier of G
let n be Nat; :: thesis: for G being n,R -linear Group holds the multF of G = (matrix_mult (n,R)) || the carrier of G
let G be n,R -linear Group; :: thesis: the multF of G = (matrix_mult (n,R)) || the carrier of G
set UG = the carrier of G;
set UGL = the carrier of (GL (n,R));
the carrier of G c= the carrier of (GL (n,R)) by Th164;
then A1: [: the carrier of G, the carrier of G:] c= [: the carrier of (GL (n,R)), the carrier of (GL (n,R)):] by ZFMISC_1:96;
multMagma(# the carrier of G, the multF of G #) is Subgroup of GL (n,R) by Def13;
hence the multF of G = the multF of (GL (n,R)) || the carrier of G by GROUP_2:def 5
.= (matrix_mult (n,R)) || the carrier of G by A1, RELAT_1:74 ;
:: thesis: verum