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 )
A4: Indices M1 = Indices M2 by Th27;
assume that
A5: for i being Nat st [i,i] in Indices M1 holds
M1 * i,i = 1. K and
A6: for i, j being Nat st [i,j] in Indices M1 & i <> j holds
M1 * i,j = 0. K and
A7: for i being Nat st [i,i] in Indices M2 holds
M2 * i,i = 1. K and
A8: for i, j being Nat st [i,j] in Indices M2 & i <> j holds
M2 * i,j = 0. K ; :: thesis: M1 = M2

A9: now

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * i,j = M2 * i,j )
assume A10: [i,j] in Indices M1 ; :: thesis: M1 * i,j = M2 * i,j

A11: now

assume i = j ; :: thesis: M1 * i,j = M2 * i,j
then ( M1 * i,j = 1. K & M2 * i,j = 1. K ) by A4, A5, A7, A10;
hence M1 * i,j = M2 * i,j ; :: thesis: verum

end;

now

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

end;

hence M1 * i,j = M2 * i,j by A11; :: thesis: verum

end;

( len M1 = n & width M1 = n & len M2 = n & width M2 = n ) by Th25;
hence M1 = M2 by A9, Th21; :: thesis: verum