let M1, M2 be diagonal Matrix of len p, REAL ; :: thesis: ( ( for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j ) & ( for j being Element of NAT st j in dom p holds
M2 * (j,j) = p . j ) implies M1 = M2 )
assume that
A5: for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j and
A6: for j being Element of NAT st j in dom p holds
M2 * (j,j) = p . j ; :: thesis: M1 = M2
width M1 = len p by MATRIX_1:24;
then A7: Seg (width M1) = dom p by FINSEQ_1:def 3;
A8: Indices M1 = Indices M2 by MATRIX_1: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 A9: [i,j] in Indices M1 ; :: thesis: M1 * (b₁,b₂) = M2 * (b₁,b₂)
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 12;
A10: [i1,j1] in Indices M1 by A9;
then A11: j1 in Seg (width M1) by MATRPROB:12;

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

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

hence M1 * (i,j) = p . j by A5, A7, A11
.= M2 * (i,j) by A6, A7, A11, A12 ;
:: thesis: verum

end;

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

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

end;

end;

end;

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