let R be Ring; :: thesis: for n being Nat
for S being Subring of R holds GL (n,S) is strict Subgroup of GL (n,R)
let n be Nat; :: thesis: for S being Subring of R holds GL (n,S) is strict Subgroup of GL (n,R)
let S be Subring of R; :: thesis: GL (n,S) is strict Subgroup of GL (n,R)
( the carrier of (GL (n,S)) c= the carrier of (GL (n,R)) & the multF of (GL (n,S)) = the multF of (GL (n,R)) || the carrier of (GL (n,S)) ) by Th140, Th141;
hence GL (n,S) is strict Subgroup of GL (n,R) by GROUP_2:def 5; :: thesis: verum