let R be Ring; :: thesis: for n being Nat
for z being Element of R st z in center R holds
for A being Matrix of n,R holds A * (z * (1. (R,n))) = (z * (1. (R,n))) * A
let n be Nat; :: thesis: for z being Element of R st z in center R holds
for A being Matrix of n,R holds A * (z * (1. (R,n))) = (z * (1. (R,n))) * A
let z be Element of R; :: thesis: ( z in center R implies for A being Matrix of n,R holds A * (z * (1. (R,n))) = (z * (1. (R,n))) * A )
assume A1: z in center R ; :: thesis: for A being Matrix of n,R holds A * (z * (1. (R,n))) = (z * (1. (R,n))) * A
let A be Matrix of n,R; :: thesis: A * (z * (1. (R,n))) = (z * (1. (R,n))) * A
A * (1. (R,n)) = A by MATRIX_3:19
.= (1. (R,n)) * A by MATRIX_3:18 ;
hence A * (z * (1. (R,n))) = (z * (1. (R,n))) * A by A1, Th99; :: thesis: verum