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 )
A11: Indices M = [:(dom M),(Seg (width M)):] by MATRIX_1:def 5;
dom A = dom M by A6, FINSEQ_3:31;
then A12: Indices A = [:(dom M),(Seg (width M)):] by A7, MATRIX_1:def 5;
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, A11
.= B * i,j by A10, A13, A12, A11 ;
:: thesis: verum

end;

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