let M1, M2 be diagonal Matrix of len p,REAL; :: thesis: ( ( for j being Nat st j in dom p holds
M1 * (j,j) = p . j ) & ( for j being Nat st j in dom p holds
M2 * (j,j) = p . j ) implies M1 = M2 )
assume that
A7: for j being Nat st j in dom p holds
M1 * (j,j) = p . j and
A8: for j being Nat st j in dom p holds
M2 * (j,j) = p . j ; :: thesis: M1 = M2
width M1 = len p by MATRIX_0:24;
then A9: Seg (width M1) = dom p by FINSEQ_1:def 3;
A10: Indices M1 = Indices M2 by MATRIX_0:26;

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 * (b₁,b₂) = M2 * (b₁,b₂) )
assume A11: [i,j] in Indices M1 ; :: thesis: M1 * (b₁,b₂) = M2 * (b₁,b₂)
reconsider i1 = i, j1 = j as Nat ;
A12: [i1,j1] in Indices M1 by A11;
then A13: j1 in Seg (width M1) by MATRPROB:12;

per cases ( i = j or i <> j ) ;

suppose A14: i = j ; :: thesis: M1 * (b₁,b₂) = M2 * (b₁,b₂)

hence M1 * (i,j) = p . j by A7, A9, A13
.= M2 * (i,j) by A8, A9, A13, A14 ;
:: thesis: verum

end;

suppose A15: i <> j ; :: thesis: M1 * (b₁,b₂) = M2 * (b₁,b₂)

hence M1 * (i,j) = 0 by A12, Def3
.= M2 * (i,j) by A10, A12, A15, Def3 ;
:: thesis: verum

end;

end;

end;

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