let R be Ring; :: thesis: for n being Nat
for X being Element of (Matrix_ring (n,R)) holds
( X in center (Matrix_ring (n,R)) iff ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) )
let n be Nat; :: thesis: for X being Element of (Matrix_ring (n,R)) holds
( X in center (Matrix_ring (n,R)) iff ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) )
let X be Element of (Matrix_ring (n,R)); :: thesis: ( X in center (Matrix_ring (n,R)) iff ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) )

hereby :: thesis: ( ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) implies X in center (Matrix_ring (n,R)) )

assume A1: X in center (Matrix_ring (n,R)) ; :: thesis: ex z being Element of R st
( z in center R & X = z * (1. (R,n)) )
reconsider A = X as Matrix of n,R by Th72;
for B being Matrix of n,R holds A * B = B * A by A1, Th105;
then consider z being Element of R such that
A2: ( z in center R & A = z * (1. (R,n)) ) by Th103;
take z = z; :: thesis: ( z in center R & X = z * (1. (R,n)) )
thus z in center R by A2; :: thesis: X = z * (1. (R,n))
thus X = z * (1. (R,n)) by A2; :: thesis: verum

end;

given z being Element of R such that A3: ( z in center R & X = z * (1. (R,n)) ) ; :: thesis: X in center (Matrix_ring (n,R))
reconsider A = X as Matrix of n,R by Th72;
for Y being Element of (Matrix_ring (n,R)) holds X * Y = Y * X

proof

let Y be Element of (Matrix_ring (n,R)); :: thesis: X * Y = Y * X
reconsider B = Y as Matrix of n,R by Th72;
thus X * Y = A * B by Th75
.= B * A by A3, Th100
.= Y * X by Th75 ; :: thesis: verum

end;

hence X in center (Matrix_ring (n,R)) by WEDDWITT:17; :: thesis: verum