let R be Ring; :: thesis: for n being Nat holds 1_ (GL (n,R)) = 1. (R,n)
let n be Nat; :: thesis: 1_ (GL (n,R)) = 1. (R,n)
reconsider I = 1. (R,n) as Element of (GL (n,R)) by Th129;
for x being Element of (GL (n,R)) holds
( x * I = x & I * x = x )

proof

let x be Element of (GL (n,R)); :: thesis: ( x * I = x & I * x = x )
reconsider X = x as invertible Matrix of n,R by Th126;
thus x * I = X * (1. (R,n)) by Th127
.= x by MATRIX_3:19 ; :: thesis: I * x = x
thus I * x = (1. (R,n)) * X by Th127
.= x by MATRIX_3:18 ; :: thesis: verum

end;

hence 1_ (GL (n,R)) = 1. (R,n) by GROUP_1:4; :: thesis: verum