defpred S1[ 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 S1[i,j,x]
proof
let i,
j be
Nat;
( [i,j] in [:(Seg (len p)),(Seg (len p)):] implies ex x being Element of REAL st S1[i,j,x] )
assume
[i,j] in [:(Seg (len p)),(Seg (len p)):]
;
ex x being Element of REAL st S1[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
S1[
i,
j,
p . i] )
;
hence
ex
x being
Element of
REAL st
S1[
i,
j,
x]
by A2, A3;
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
S1[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
; 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
hence
for j being Nat st j in dom p holds
M1 * (j,j) = p . j
; verum