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 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 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 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:29;

hereby :: thesis: ( len MR1 = len p & width MR1 = width MR & ( for i, j being 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 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 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:29;
A8: dom MR1 = dom p by A1, A6, FINSEQ_3:29;
thus for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) :: thesis: verum

proof

let i, j be 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_0:def 7;
A13: len (Col (MR,j)) = len MR by MATRIX_0:def 8;
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 16
.= (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_0:def 8 ; :: thesis: verum

end;

end;

assume that
A16: len MR1 = len p and
A17: width MR1 = width MR and
A18: for i, j being 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:29;
A20: dom MR = dom MR1 by A3, A16, FINSEQ_3:29;
for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j))

proof

let i, j be 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_0:def 7;
A25: len (Col (MR,j)) = len MR by MATRIX_0:def 8;
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_0:def 8
.= 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 16 ; :: thesis: verum

end;

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