defpred S₁[ Nat, Nat, Element of 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
for x1, x2 being Element of REAL st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
A2: 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]
( ( i = j implies S₁[i,j,p . i] ) & ( i <> j implies S₁[i,j, 0 ] ) ) ;
hence ex x being Element of REAL st S₁[i,j,x] ; :: thesis: verum

end;

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

proof

let j be Element of NAT ; :: thesis: ( j in dom p implies M1 * j,j = p . j )
assume A7: j in dom p ; :: thesis: M1 * j,j = p . j
[j,j] in Indices M1 by A5, A7, MATRPROB:12;
hence M1 * j,j = p . j by A3; :: thesis: verum

end;

take M1 ; :: thesis: for j being Element of NAT st j in dom p holds
M1 * j,j = p . j
thus for j being Element of NAT st j in dom p holds
M1 * j,j = p . j by A6; :: thesis: verum