let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear Group
for H being Subgroup of G holds H is n,R -linear
let n be Nat; :: thesis: for G being n,R -linear Group
for H being Subgroup of G holds H is n,R -linear
let G be n,R -linear Group; :: thesis: for H being Subgroup of G holds H is n,R -linear
let H be Subgroup of G; :: thesis: H is n,R -linear
A1: the carrier of H c= the carrier of (GL (n,R))

proof

A2: the carrier of H c= the carrier of G by GROUP_2:def 5;
the carrier of G c= the carrier of (GL (n,R)) by Th164;
hence the carrier of H c= the carrier of (GL (n,R)) by A2, XBOOLE_1:1; :: thesis: verum

end;

the multF of H = the multF of (GL (n,R)) || the carrier of H

proof

set UH = the carrier of H;
set UG = the carrier of G;
the carrier of H c= the carrier of G by GROUP_2:def 5;
then A3: [: the carrier of H, the carrier of H:] c= [: the carrier of G, the carrier of G:] by ZFMISC_1:96;
thus the multF of H = the multF of G || the carrier of H by GROUP_2:def 5
.= ( the multF of (GL (n,R)) || the carrier of G) || the carrier of H by Th168
.= the multF of (GL (n,R)) || the carrier of H by A3, FUNCT_1:51 ; :: thesis: verum

end;

hence H is n,R -linear by A1, GROUP_2:def 5; :: thesis: verum