let p be FinSequence of REAL ; :: thesis: for MR being Matrix of REAL holds
( MR = Vec2DiagMx p iff ( len MR = len p & width MR = len p & ( for i being Element of NAT st i in dom MR holds
( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) ) ) )
let MR be Matrix of REAL ; :: thesis: ( MR = Vec2DiagMx p iff ( len MR = len p & width MR = len p & ( for i being Element of NAT st i in dom MR holds
( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) ) ) )

hereby :: thesis: ( len MR = len p & width MR = len p & ( for i being Element of NAT st i in dom MR holds
( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) ) implies MR = Vec2DiagMx p )

assume A1: MR = Vec2DiagMx p ; :: thesis: ( len MR = len p & width MR = len p & ( for i being Element of NAT st i in dom MR holds
( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) ) )
then reconsider M1 = MR as diagonal Matrix of len p, REAL ;
A2: ( len M1 = len p & width M1 = len p ) by MATRIX_1:25;
then A3: ( dom MR = dom p & Seg (width MR) = dom p ) by FINSEQ_1:def 3, FINSEQ_3:31;
thus ( len MR = len p & width MR = len p ) by A2; :: thesis: for i being Element of NAT st i in dom MR holds
( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i )
thus for i being Element of NAT st i in dom MR holds
( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i in dom MR implies ( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) )
assume A4: i in dom MR ; :: thesis: ( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i )
A5: Line M1,i has_onlyone_value_in i by A4, Th24;
(Line MR,i) . i = MR * i,i by A3, A4, MATRIX_1:def 8
.= p . i by A1, A3, A4, Def4 ;
hence ( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) by A5; :: thesis: verum

end;

end;

assume A6: ( len MR = len p & width MR = len p & ( for i being Element of NAT st i in dom MR holds
( Line MR,i has_onlyone_value_in i & (Line MR,i) . i = p . i ) ) ) ; :: thesis: MR = Vec2DiagMx p
then reconsider MM = MR as Matrix of len p, REAL by MATRIX_2:7;
for i being Element of NAT st i in dom MM holds
Line MM,i has_onlyone_value_in i by A6;
then reconsider MM = MM as diagonal Matrix of len p, REAL by Th24;
for j being Element of NAT st j in dom p holds
MM * j,j = p . j

proof

let j be Element of NAT ; :: thesis: ( j in dom p implies MM * j,j = p . j )
assume A7: j in dom p ; :: thesis: MM * j,j = p . j
A8: ( dom MM = dom p & Seg (width MM) = dom p ) by A6, FINSEQ_1:def 3, FINSEQ_3:31;
hence MM * j,j = (Line MM,j) . j by A7, MATRIX_1:def 8
.= p . j by A6, A7, A8 ;
:: thesis: verum

end;

hence MR = Vec2DiagMx p by Def4; :: thesis: verum