let M1, M2 be Matrix of n,K; :: thesis: ( ( for i being Nat st [i,i] in Indices M1 holds
M1 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M1 & i <> j holds
M1 * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices M2 holds
M2 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M2 & i <> j holds
M2 * (i,j) = 0. K ) implies M1 = M2 )
assume that
A3: for i being Nat st [i,i] in Indices M1 holds
M1 * (i,i) = 1. K and
A4: for i, j being Nat st [i,j] in Indices M1 & i <> j holds
M1 * (i,j) = 0. K and
A5: for i being Nat st [i,i] in Indices M2 holds
M2 * (i,i) = 1. K and
A6: for i, j being Nat st [i,j] in Indices M2 & i <> j holds
M2 * (i,j) = 0. K ; :: thesis: M1 = M2
A7: Indices M1 = Indices M2 by MATRIX_0:26;

A8: 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 A9: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)

A10: now :: thesis: ( i <> j implies M1 * (i,j) = M2 * (i,j) )

assume A11: i <> j ; :: thesis: M1 * (i,j) = M2 * (i,j)
then M1 * (i,j) = 0. K by A4, A9;
hence M1 * (i,j) = M2 * (i,j) by A7, A6, A9, A11; :: thesis: verum

end;

now :: thesis: ( i = j implies M1 * (i,j) = M2 * (i,j) )

assume A12: i = j ; :: thesis: M1 * (i,j) = M2 * (i,j)
then M1 * (i,j) = 1. K by A3, A9;
hence M1 * (i,j) = M2 * (i,j) by A7, A5, A9, A12; :: thesis: verum

end;

hence M1 * (i,j) = M2 * (i,j) by A10; :: thesis: verum

end;

A13: ( len M2 = n & width M2 = n ) by MATRIX_0:24;
( len M1 = n & width M1 = n ) by MATRIX_0:24;
hence M1 = M2 by A8, A13, MATRIX_0:21; :: thesis: verum