let M1, M2 be Matrix of K; :: thesis: ( len M1 = len A & width M1 = width B & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = (Line A,i) "*" (Col B,j) ) & len M2 = len A & width M2 = width B & ( for i, j being Nat st [i,j] in Indices M2 holds
M2 * i,j = (Line A,i) "*" (Col B,j) ) implies M1 = M2 )
assume that
A5: len M1 = len A and
A6: width M1 = width B and
A7: for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = (Line A,i) "*" (Col B,j) and
A8: len M2 = len A and
A9: width M2 = width B and
A10: for i, j being Nat st [i,j] in Indices M2 holds
M2 * i,j = (Line A,i) "*" (Col B,j) ; :: thesis: M1 = M2
dom M2 = dom M1 by A5, A8, FINSEQ_3:31;
then A11: ( Indices M1 = [:(dom M1),(Seg (width M1)):] & Indices M2 = [:(dom M1),(Seg (width M1)):] ) by A6, A9, MATRIX_1:def 5;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * i,j = M2 * i,j )
assume A12: [i,j] in Indices M1 ; :: thesis: M1 * i,j = M2 * i,j
then M1 * i,j = (Line A,i) "*" (Col B,j) by A7;
hence M1 * i,j = M2 * i,j by A10, A11, A12; :: thesis: verum

end;

hence M1 = M2 by A5, A6, A8, A9, MATRIX_1:21; :: thesis: verum