let R be Ring; :: thesis: for z being Element of R st z in center R holds
for A being Matrix of R holds A * z = z * A
let z be Element of R; :: thesis: ( z in center R implies for A being Matrix of R holds A * z = z * A )
assume A1: z in center R ; :: thesis: for A being Matrix of R holds A * z = z * A
let A be Matrix of R; :: thesis: A * z = z * A
A2: ( len (A * z) = len (z * A) & width (A * z) = width (z * A) )

proof

thus len (A * z) = len A by MATRIX_3:def 6
.= len (z * A) by MATRIX_3:def 5 ; :: thesis: width (A * z) = width (z * A)
thus width (A * z) = width A by MATRIX_3:def 6
.= width (z * A) by MATRIX_3:def 5 ; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices (A * z) holds
(A * z) * (i,j) = (z * A) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (A * z) implies (A * z) * (i,j) = (z * A) * (i,j) )
assume A3: [i,j] in Indices (A * z) ; :: thesis: (A * z) * (i,j) = (z * A) * (i,j)
A4: Indices (A * z) = [:(dom (A * z)),(Seg (width (A * z))):] by MATRIX_0:def 4
.= [:(Seg (len (A * z))),(Seg (width (A * z))):] by FINSEQ_1:def 3
.= [:(Seg (len A)),(Seg (width (A * z))):] by MATRIX_3:def 6
.= [:(Seg (len A)),(Seg (width A)):] by MATRIX_3:def 6
.= [:(dom A),(Seg (width A)):] by FINSEQ_1:def 3
.= Indices A by MATRIX_0:def 4 ;
hence (A * z) * (i,j) = (A * (i,j)) * z by A3, MATRIX_3:def 6
.= z * (A * (i,j)) by A1, WEDDWITT:17
.= (z * A) * (i,j) by A3, A4, MATRIX_3:def 5 ;
:: thesis: verum

end;

hence A * z = z * A by A2, MATRIX_0:21; :: thesis: verum