let K be non empty commutative multMagma ; :: thesis: for M being Matrix of K
for a being Element of K holds a * M = M * a
let M be Matrix of K; :: thesis: for a being Element of K holds a * M = M * a
let a be Element of K; :: thesis: a * M = M * a
A1: len (a * M) = len M by Def5
.= len (M * a) by Def6 ;
A2: width (a * M) = width M by Def5
.= width (M * a) by Def6 ;
for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) = (M * a) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) = (M * a) * (i,j) )
assume A3: [i,j] in Indices (a * M) ; :: thesis: (a * M) * (i,j) = (M * a) * (i,j)
A4: [i,j] in Indices M

proof

A5: dom (a * M) = Seg (len (a * M)) by FINSEQ_1:def 3
.= Seg (len M) by Def5
.= dom M by FINSEQ_1:def 3 ;
width (a * M) = width M by Def5;
then [:(dom M),(Seg (width M)):] = [:(dom (a * M)),(Seg (width (a * M))):] by A5
.= Indices (a * M) ;
then Indices M = Indices (a * M) ;
hence [i,j] in Indices M by A3; :: thesis: verum

end;

thus (a * M) * (i,j) = a * (M * (i,j)) by A4, Def5
.= (M * a) * (i,j) by A4, Def6 ; :: thesis: verum

end;

hence a * M = M * a by A1, A2, MATRIX_0:21; :: thesis: verum