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
A5: len A = len M and
A6: width A = width M and
A7: for i, j being Nat st [i,j] in Indices M holds
A * (i,j) = a * (M * (i,j)) and
A8: ( len B = len M & width B = width M ) and
A9: for i, j being Nat st [i,j] in Indices M holds
B * (i,j) = a * (M * (i,j)) ; :: thesis: A = B

now :: thesis: for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)

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

end;

hence A = B by A5, A6, A8, MATRIX_0:21; :: thesis: verum