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
A6: for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j and
A7: 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 A8: Seg (width M1) = dom p by FINSEQ_1:def 3;
A9: Indices M1 = Indices M2 by MATRIX_1:26;

now

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

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

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

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

end;

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

hence M1 * (i,j) = 0 by A11, Def3
.= M2 * (i,j) by A9, A11, A14, Def3 ;
:: thesis: verum

end;

end;

end;

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