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

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 A12: i <> j ; :: thesis: M1 * i,j = M2 * i,j
then M1 * i,j = 0. K by A5, A10;
hence M1 * i,j = M2 * i,j by A8, A7, A10, A12; :: thesis: verum

end;

now

assume A13: i = j ; :: thesis: M1 * i,j = M2 * i,j
then M1 * i,j = 1. K by A4, A10;
hence M1 * i,j = M2 * i,j by A8, A6, A10, A13; :: thesis: verum

end;

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

end;

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