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