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) ) ) ) )
set MM = Vec2DiagMx p;
A1: len (Vec2DiagMx p) = len p by Th25;
A2: width (Vec2DiagMx p) = len p by Th25;
assume A3: 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 A4: dom p = dom MR by FINSEQ_3:31;

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 A5: 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) ) )
hence ( len MR1 = len p & width MR1 = width MR ) by A3, A1, A2, 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)
A6: len MR1 = len (Vec2DiagMx p) by A3, A2, A5, MATRPROB:39;
then A7: dom MR1 = dom (Vec2DiagMx p) by FINSEQ_3:31;
A8: dom MR1 = dom p by A1, A6, FINSEQ_3:31;
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 A9: [i,j] in Indices MR1 ; :: thesis: MR1 * i,j = (p . i) * (MR * i,j)
i in Seg (len MR1) by A9, MATRPROB:12;
then A10: i in dom MR1 by FINSEQ_1:def 3;
then A11: (Line (Vec2DiagMx p),i) . i = p . i by A7, Th25;
set q = mlt (Line (Vec2DiagMx p),i),(Col MR,j);
A12: len (Line (Vec2DiagMx p),i) = width (Vec2DiagMx p) by MATRIX_1:def 8;
A13: len (Col MR,j) = len MR by MATRIX_1:def 9;
A14: Line (Vec2DiagMx p),i has_onlyone_value_in i by A7, A10, Th25;
then A15: (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) . i = ((Line (Vec2DiagMx p),i) . i) * ((Col MR,j) . i) by A3, A2, A12, A13, Th12;
thus MR1 * i,j = (Line (Vec2DiagMx p),i) "*" (Col MR,j) by A3, A2, A5, A9, MATRPROB:39
.= Sum (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) by RVSUM_1:def 17
.= (p . i) * ((Col MR,j) . i) by A3, A2, A14, A11, A12, A13, A15, Th12, Th13
.= (p . i) * (MR * i,j) by A4, A8, A10, MATRIX_1:def 9 ; :: thesis: verum

end;

end;

assume that
A16: len MR1 = len p and
A17: width MR1 = width MR and
A18: 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
A19: dom MR1 = dom (Vec2DiagMx p) by A1, A16, FINSEQ_3:31;
A20: dom MR = dom MR1 by A3, A16, 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 A21: [i,j] in Indices MR1 ; :: thesis: MR1 * i,j = (Line (Vec2DiagMx p),i) "*" (Col MR,j)
i in Seg (len MR1) by A21, MATRPROB:12;
then A22: i in dom MR1 by FINSEQ_1:def 3;
then A23: (Line (Vec2DiagMx p),i) . i = p . i by A19, Th25;
set q = mlt (Line (Vec2DiagMx p),i),(Col MR,j);
A24: len (Line (Vec2DiagMx p),i) = width (Vec2DiagMx p) by MATRIX_1:def 8;
A25: len (Col MR,j) = len MR by MATRIX_1:def 9;
A26: Line (Vec2DiagMx p),i has_onlyone_value_in i by A19, A22, Th25;
then A27: (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) . i = ((Line (Vec2DiagMx p),i) . i) * ((Col MR,j) . i) by A3, A2, A24, A25, Th12;
thus MR1 * i,j = (p . i) * (MR * i,j) by A18, A21
.= (p . i) * ((Col MR,j) . i) by A20, A22, MATRIX_1:def 9
.= Sum (mlt (Line (Vec2DiagMx p),i),(Col MR,j)) by A3, A2, A26, A23, A24, A25, A27, Th12, Th13
.= (Line (Vec2DiagMx p),i) "*" (Col MR,j) by RVSUM_1:def 17 ; :: thesis: verum

end;

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