let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear Group holds inverse_op G = (inverse_op (GL (n,R))) | the carrier of G
let n be Nat; :: thesis: for G being n,R -linear Group holds inverse_op G = (inverse_op (GL (n,R))) | the carrier of G
let G be n,R -linear Group; :: thesis: inverse_op G = (inverse_op (GL (n,R))) | the carrier of G
set UG = the carrier of G;
set UMG = the carrier of multMagma(# the carrier of G, the multF of G #);
A1: multMagma(# the carrier of G, the multF of G #) is Subgroup of GL (n,R) by Def13;
thus inverse_op G = inverse_op multMagma(# the carrier of G, the multF of G #) by Th162
.= (inverse_op (GL (n,R))) | the carrier of G by A1, GROUP_2:49 ; :: thesis: verum