defpred S₁[ Nat, Nat, Real] means ( ( $1 = $2 implies $3 = p . $1 ) & ( $1 <> $2 implies $3 = 0 ) );
A1: for i, j being Nat st [i,j] in [:(Seg (len p)),(Seg (len p)):] holds
ex x being Element of REAL st S₁[i,j,x]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg (len p)),(Seg (len p)):] implies ex x being Element of REAL st S₁[i,j,x] )
assume [i,j] in [:(Seg (len p)),(Seg (len p)):] ; :: thesis: ex x being Element of REAL st S₁[i,j,x]
A2: p . i in REAL by XREAL_0:def 1;
A3: 0 in REAL by XREAL_0:def 1;
( i = j implies S₁[i,j,p . i] ) ;
hence ex x being Element of REAL st S₁[i,j,x] by A2, A3; :: thesis: verum

end;

consider M being Matrix of len p,REAL such that
A4: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * (i,j)] from MATRIX_0:sch 2(A1);
for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0 holds
i = j by A4;
then reconsider M1 = M as diagonal Matrix of len p,REAL by Def3;
take M1 ; :: thesis: for j being Nat st j in dom p holds
M1 * (j,j) = p . j
len M = len p by MATRIX_0:24;
then A5: Seg (len M1) = dom p by FINSEQ_1:def 3;
width M = len p by MATRIX_0:24;
then A6: Seg (width M1) = dom p by FINSEQ_1:def 3;
for j being Nat st j in dom p holds
M1 * (j,j) = p . j

proof

let j be Nat; :: thesis: ( j in dom p implies M1 * (j,j) = p . j )
assume j in dom p ; :: thesis: M1 * (j,j) = p . j
then [j,j] in Indices M1 by A6, A5, MATRPROB:12;
hence M1 * (j,j) = p . j by A4; :: thesis: verum

end;

hence for j being Nat st j in dom p holds
M1 * (j,j) = p . j ; :: thesis: verum