let R be Ring; :: thesis: for n being Nat
for G being b₁,R -linear general Group holds multMagma(# the carrier of G, the multF of G #) = GL (n,R)
let n be Nat; :: thesis: for G being n,R -linear general Group holds multMagma(# the carrier of G, the multF of G #) = GL (n,R)
let G be n,R -linear general Group; :: thesis: multMagma(# the carrier of G, the multF of G #) = GL (n,R)
the multF of G = the multF of (GL (n,R)) by Th175;
hence multMagma(# the carrier of G, the multF of G #) = GL (n,R) by Th174; :: thesis: verum