let M1, M2 be Matrix of n,m,K; :: thesis: ( len M1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M1 * (i,j) = M * (i,k) ) & ( j = k implies M1 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M1 * (i,j) = M * (i,j) ) ) ) & len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = M * (i,k) ) & ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ) ) implies M1 = M2 )
assume that
len M1 = len M and
A23: for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M1 * (i,j) = M * (i,k) ) & ( j = k implies M1 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M1 * (i,j) = M * (i,j) ) ) and
len M2 = len M and
A24: for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = M * (i,k) ) & ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ) ; :: thesis: M1 = M2
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)

proof

A25: Indices M = Indices M1 by MATRIX_0:26;
let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then A26: ( i in dom M & j in Seg (width M) ) by A25, ZFMISC_1:87;
then A27: ( j = k implies M1 * (i,j) = M * (i,l) ) by A23;
A28: ( j = l implies M2 * (i,j) = M * (i,k) ) by A24, A26;
A29: ( j <> l & j <> k implies M1 * (i,j) = M * (i,j) ) by A23, A26;
A30: ( j = k implies M2 * (i,j) = M * (i,l) ) by A24, A26;
( j = l implies M1 * (i,j) = M * (i,k) ) by A23, A26;
hence M1 * (i,j) = M2 * (i,j) by A24, A26, A27, A29, A28, A30; :: thesis: verum

end;

hence M1 = M2 by MATRIX_0:27; :: thesis: verum