let R be Ring; :: thesis: for n being Nat
for z being Element of R st z in center R holds
for A, B being Matrix of n,R st A * B = B * A holds
A * (z * B) = (z * B) * A
let n be Nat; :: thesis: for z being Element of R st z in center R holds
for A, B being Matrix of n,R st A * B = B * A holds
A * (z * B) = (z * B) * A
let z be Element of R; :: thesis: ( z in center R implies for A, B being Matrix of n,R st A * B = B * A holds
A * (z * B) = (z * B) * A )
assume A1: z in center R ; :: thesis: for A, B being Matrix of n,R st A * B = B * A holds
A * (z * B) = (z * B) * A
let A, B be Matrix of n,R; :: thesis: ( A * B = B * A implies A * (z * B) = (z * B) * A )
assume A2: A * B = B * A ; :: thesis: A * (z * B) = (z * B) * A
thus A * (z * B) = (A * z) * B by Th24
.= (z * A) * B by A1, Th98
.= z * (A * B) by Th29
.= (z * B) * A by A2, Th29 ; :: thesis: verum