let A, B be Matrix of K; :: thesis: ( len A = len M & width A = width M & ( for i, j being Nat st [i,j] in Indices M holds
A * i,j = a * (M * i,j) ) & len B = len M & width B = width M & ( for i, j being Nat st [i,j] in Indices M holds
B * i,j = a * (M * i,j) ) implies A = B )
assume that
A6: len A = len M and
A7: width A = width M and
A8: for i, j being Nat st [i,j] in Indices M holds
A * i,j = a * (M * i,j) and
A9: ( len B = len M & width B = width M ) and
A10: for i, j being Nat st [i,j] in Indices M holds
B * i,j = a * (M * i,j) ; :: thesis: A = B

now

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * i,j = B * i,j )
dom A = dom M by A6, FINSEQ_3:31;
then A12: Indices A = [:(dom M),(Seg (width M)):] by A7;
assume A13: [i,j] in Indices A ; :: thesis: A * i,j = B * i,j
hence A * i,j = a * (M * i,j) by A8, A12
.= B * i,j by A10, A13, A12 ;
:: thesis: verum

end;

hence A = B by A6, A7, A9, MATRIX_1:21; :: thesis: verum