let R be Ring; :: thesis: for n being Nat
for X being Element of (GL (n,R)) st ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) holds
X in center (GL (n,R))
let n be Nat; :: thesis: for X being Element of (GL (n,R)) st ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) holds
X in center (GL (n,R))
let X be Element of (GL (n,R)); :: thesis: ( ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) implies X in center (GL (n,R)) )
given z being Element of R such that A1: ( z in center R & X = z * (1. (R,n)) ) ; :: thesis: X in center (GL (n,R))
reconsider A = X as Matrix of n,R by Th126;
for Y being Element of (GL (n,R)) holds X * Y = Y * X

proof

let Y be Element of (GL (n,R)); :: thesis: X * Y = Y * X
reconsider B = Y as Matrix of n,R by Th126;
thus X * Y = A * B by Th127
.= B * A by A1, Th100
.= Y * X by Th127 ; :: thesis: verum

end;

hence X in center (GL (n,R)) by GROUP_5:77; :: thesis: verum