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:29;
then A11: ( Indices M1 = [:(dom M1),(Seg (width M1)):] & Indices M2 = [:(dom M1),(Seg (width M1)):] ) by A6, A9;

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

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_0:21; :: thesis: verum