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 by MATRIX_1:25;
then A3: dom MR = dom p by FINSEQ_3:31;
thus ( len MR = len p & width MR = len p ) by A2, MATRIX_1:25; :: 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 )
width M1 = len p by MATRIX_1:25;
then A4: Seg (width MR) = dom p by FINSEQ_1:def 3;
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 A5: i in dom MR ; :: thesis: ( Line (MR,i) has_onlyone_value_in i & (Line (MR,i)) . i = p . i )
A6: Line (M1,i) has_onlyone_value_in i by A5, Th24;
(Line (MR,i)) . i = MR * (i,i) by A3, A4, A5, MATRIX_1:def 8
.= p . i by A1, A3, A5, Def4 ;
hence ( Line (MR,i) has_onlyone_value_in i & (Line (MR,i)) . i = p . i ) by A6; :: thesis: verum

end;

end;

assume that
A7: len MR = len p and
A8: width MR = len p and
A9: 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
reconsider MM = MR as Matrix of len p, REAL by A7, A8, MATRIX_2:7;
for i being Element of NAT st i in dom MM holds
Line (MM,i) has_onlyone_value_in i by A9;
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

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

end;

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