let R be Ring; :: thesis: for n being Nat
for X being Element of (Matrix_ring (n,R))
for A being Matrix of n,R st A = X holds
( X in center (Matrix_ring (n,R)) iff for B being Matrix of n,R holds A * B = B * A )
let n be Nat; :: thesis: for X being Element of (Matrix_ring (n,R))
for A being Matrix of n,R st A = X holds
( X in center (Matrix_ring (n,R)) iff for B being Matrix of n,R holds A * B = B * A )
let X be Element of (Matrix_ring (n,R)); :: thesis: for A being Matrix of n,R st A = X holds
( X in center (Matrix_ring (n,R)) iff for B being Matrix of n,R holds A * B = B * A )
let A be Matrix of n,R; :: thesis: ( A = X implies ( X in center (Matrix_ring (n,R)) iff for B being Matrix of n,R holds A * B = B * A ) )
assume A1: A = X ; :: thesis: ( X in center (Matrix_ring (n,R)) iff for B being Matrix of n,R holds A * B = B * A )

hereby :: thesis: ( ( for B being Matrix of n,R holds A * B = B * A ) implies X in center (Matrix_ring (n,R)) )

assume A2: X in center (Matrix_ring (n,R)) ; :: thesis: for B being Matrix of n,R holds A * B = B * A
let B be Matrix of n,R; :: thesis: A * B = B * A
reconsider Y = B as Element of (Matrix_ring (n,R)) by Th72;
thus A * B = X * Y by A1, Th75
.= Y * X by A2, WEDDWITT:17
.= B * A by A1, Th75 ; :: thesis: verum

end;

assume A3: for B being Matrix of n,R holds A * B = B * A ; :: thesis: X in center (Matrix_ring (n,R))
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 A1, Th75
.= B * A by A3
.= Y * X by A1, Th75 ; :: thesis: verum

end;

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