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
( ( i = l implies M1 * i,j = M * k,j ) & ( i = k implies M1 * i,j = M * l,j ) & ( i <> l & i <> 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
( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) ) ) implies M1 = M2 )
assume that
len M1 = len M and
A2: for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies M1 * i,j = M * k,j ) & ( i = k implies M1 * i,j = M * l,j ) & ( i <> l & i <> k implies M1 * i,j = M * i,j ) ) and
len M2 = len M and
A3: for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> 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

A4: Indices M = Indices M1 by MATRIX_1:27;
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 A5: ( i in dom M & j in Seg (width M) ) by A4, ZFMISC_1:106;
then A6: ( i = k implies M1 * i,j = M * l,j ) by A2;
A7: ( i = l implies M2 * i,j = M * k,j ) by A3, A5;
A8: ( i <> l & i <> k implies M1 * i,j = M * i,j ) by A2, A5;
A9: ( i = k implies M2 * i,j = M * l,j ) by A3, A5;
( i = l implies M1 * i,j = M * k,j ) by A2, A5;
hence M1 * i,j = M2 * i,j by A3, A5, A6, A8, A7, A9; :: thesis: verum

end;

hence M1 = M2 by MATRIX_1:28; :: thesis: verum