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
A8: for j being Element of NAT st j in dom p holds
M1 * j,j = p . j and
A9: for j being Element of NAT st j in dom p holds
M2 * j,j = p . j ; :: thesis: M1 = M2
A10: Indices M1 = Indices M2 by MATRIX_1:27;
( width M1 = len p & width M2 = len p ) by MATRIX_1:25;
then A11: ( Seg (width M1) = dom p & Seg (width M2) = dom p ) by FINSEQ_1:def 3;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * b₁,b₂ = M2 * b₁,b₂ )
assume A12: [i,j] in Indices M1 ; :: thesis: M1 * b₁,b₂ = M2 * b₁,b₂
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 13;
A13: [i1,j1] in Indices M1 by A12;
then A14: j1 in Seg (width M1) by MATRPROB:12;

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

suppose A15: i = j ; :: thesis: M1 * b₁,b₂ = M2 * b₁,b₂

hence M1 * i,j = p . j by A8, A11, A14
.= M2 * i,j by A9, A11, A14, A15 ;
:: thesis: verum

end;

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

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

end;

end;

end;

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