let p be FinSequence of REAL ; :: thesis: for MR, MR1 being Matrix of REAL st len p = len MR holds
( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j) ) ) )
let MR, MR1 be Matrix of REAL ; :: thesis: ( len p = len MR implies ( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j) ) ) ) )
assume A1: len p = len MR ; :: thesis: ( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j) ) ) )
then A2: dom p = dom MR by FINSEQ_3:31;
set MM = Vec2DiagMx p;
A3: ( len (Vec2DiagMx p) = len p & width (Vec2DiagMx p) = len p & ( for i being Element of NAT st i in dom (Vec2DiagMx p) holds
( Line (Vec2DiagMx p),i has_onlyone_value_in i & (Line (Vec2DiagMx p),i) . i = p . i ) ) ) by Th25;

hereby :: thesis: ( len MR1 = len p & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j) ) implies MR1 = (Vec2DiagMx p) * MR )

assume A4: MR1 = (Vec2DiagMx p) * MR ; :: thesis: ( len MR1 = len p & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j) ) )
then ( len MR1 = len (Vec2DiagMx p) & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (Line (Vec2DiagMx p),i) "*" (Col MR,j) ) ) by A1, A3, MATRPROB:39;
then A5: ( dom MR1 = dom p & dom MR1 = dom (Vec2DiagMx p) & Seg (width MR1) = Seg (width MR) ) by A3, FINSEQ_3:31;
thus ( len MR1 = len p & width MR1 = width MR ) by A1, A3, A4, MATRPROB:39; :: thesis: for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j)
thus for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j) :: thesis: verum

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices MR1 implies MR1 * i,j = (p . i) * (MR * i,j) )
assume A6: [i,j] in Indices MR1 ; :: thesis: MR1 * i,j = (p . i) * (MR * i,j)
set q = mlt (Line (Vec2DiagMx p),i),(Col MR,j);
( i in Seg (len MR1) & j in Seg (width MR1) ) by A6, MATRPROB:12;
then A7: i in dom MR1 by FINSEQ_1:def 3;
then A8: ( Line (Vec2DiagMx p),i has_onlyone_value_in i & (Line (Vec2DiagMx p),i) . i = p . i ) by A5, Th25;
( len (Line (Vec2DiagMx p),i) = width (Vec2DiagMx p) & len (Col MR,j) = len MR ) by MATRIX_1:def 8, MATRIX_1:def 9;
then A9: ( mlt (Line (Vec2DiagMx p),i),(Col MR,j) has_onlyone_value_in i & (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) . i = ((Line (Vec2DiagMx p),i) . i) * ((Col MR,j) . i) ) by A1, A3, A8, Th12;
thus MR1 * i,j = (Line (Vec2DiagMx p),i) "*" (Col MR,j) by A1, A3, A4, A6, MATRPROB:39
.= Sum (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) by EUCLID_2:def 1
.= (p . i) * ((Col MR,j) . i) by A8, A9, Th13
.= (p . i) * (MR * i,j) by A2, A5, A7, MATRIX_1:def 9 ; :: thesis: verum

end;

end;

assume A10: ( len MR1 = len p & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (p . i) * (MR * i,j) ) ) ; :: thesis: MR1 = (Vec2DiagMx p) * MR
then A11: ( dom MR1 = dom (Vec2DiagMx p) & dom MR = dom MR1 ) by A1, A3, FINSEQ_3:31;
for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * i,j = (Line (Vec2DiagMx p),i) "*" (Col MR,j)

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices MR1 implies MR1 * i,j = (Line (Vec2DiagMx p),i) "*" (Col MR,j) )
assume A12: [i,j] in Indices MR1 ; :: thesis: MR1 * i,j = (Line (Vec2DiagMx p),i) "*" (Col MR,j)
set q = mlt (Line (Vec2DiagMx p),i),(Col MR,j);
( i in Seg (len MR1) & j in Seg (width MR1) ) by A12, MATRPROB:12;
then A13: i in dom MR1 by FINSEQ_1:def 3;
then A14: ( Line (Vec2DiagMx p),i has_onlyone_value_in i & (Line (Vec2DiagMx p),i) . i = p . i ) by A11, Th25;
( len (Line (Vec2DiagMx p),i) = width (Vec2DiagMx p) & len (Col MR,j) = len MR ) by MATRIX_1:def 8, MATRIX_1:def 9;
then A15: ( mlt (Line (Vec2DiagMx p),i),(Col MR,j) has_onlyone_value_in i & (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) . i = ((Line (Vec2DiagMx p),i) . i) * ((Col MR,j) . i) ) by A1, A3, A14, Th12;
thus MR1 * i,j = (p . i) * (MR * i,j) by A10, A12
.= (p . i) * ((Col MR,j) . i) by A11, A13, MATRIX_1:def 9
.= Sum (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) by A14, A15, Th13
.= (Line (Vec2DiagMx p),i) "*" (Col MR,j) by EUCLID_2:def 1 ; :: thesis: verum

end;

hence MR1 = (Vec2DiagMx p) * MR by A1, A3, A10, MATRPROB:39; :: thesis: verum