let R be Ring; :: thesis: for n being Nat
for H being Subgroup of GL (n,R) holds H is n,R -linear
let n be Nat; :: thesis: for H being Subgroup of GL (n,R) holds H is n,R -linear
let H be Subgroup of GL (n,R); :: thesis: H is n,R -linear
multMagma(# the carrier of H, the multF of H #) is Subgroup of H by Th161;
hence H is n,R -linear by GROUP_2:56; :: thesis: verum