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 being Element of NAT st i in dom MR1 holds
Line MR1,i = (p . i) * (Line MR,i) ) ) )
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 being Element of NAT st i in dom MR1 holds
Line MR1,i = (p . i) * (Line MR,i) ) ) ) )
assume A1: len p = len MR ; :: thesis: ( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i being Element of NAT st i in dom MR1 holds
Line MR1,i = (p . i) * (Line MR,i) ) ) )
set MM = Vec2DiagMx p;

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

assume A2: MR1 = (Vec2DiagMx p) * MR ; :: thesis: ( len MR1 = len p & width MR1 = width MR & ( for i being Element of NAT st i in dom MR1 holds
Line MR1,i = (p . i) * (Line MR,i) ) )
then A3: ( 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) ) ) by A1, Th26;
thus ( len MR1 = len p & width MR1 = width MR ) by A1, A2, Th26; :: thesis: for i being Element of NAT st i in dom MR1 holds
Line MR1,i = (p . i) * (Line MR,i)
thus for i being Element of NAT st i in dom MR1 holds
Line MR1,i = (p . i) * (Line MR,i) :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i in dom MR1 implies Line MR1,i = (p . i) * (Line MR,i) )
assume A4: i in dom MR1 ; :: thesis: Line MR1,i = (p . i) * (Line MR,i)
A5: i in Seg (len MR1) by A4, FINSEQ_1:def 3;
A6: dom (Line MR1,i) = Seg (len (Line MR1,i)) by FINSEQ_1:def 3
.= Seg (width MR1) by MATRIX_1:def 8
.= Seg (len (Line MR,i)) by A3, MATRIX_1:def 8
.= dom (Line MR,i) by FINSEQ_1:def 3
.= dom ((p . i) * (Line MR,i)) by VALUED_1:def 5 ;
for j being Nat st j in dom (Line MR1,i) holds
(Line MR1,i) . j = ((p . i) * (Line MR,i)) . j

proof

let j be Nat; :: thesis: ( j in dom (Line MR1,i) implies (Line MR1,i) . j = ((p . i) * (Line MR,i)) . j )
assume A7: j in dom (Line MR1,i) ; :: thesis: (Line MR1,i) . j = ((p . i) * (Line MR,i)) . j
A8: j in NAT by ORDINAL1:def 13;
j in Seg (len (Line MR1,i)) by A7, FINSEQ_1:def 3;
then A9: j in Seg (width MR1) by MATRIX_1:def 8;
then A10: [i,j] in Indices MR1 by A5, MATRPROB:12;
thus (Line MR1,i) . j = MR1 * i,j by A9, MATRIX_1:def 8
.= (p . i) * (MR * i,j) by A1, A2, A8, A10, Th26
.= (p . i) * ((Line MR,i) . j) by A3, A9, MATRIX_1:def 8
.= ((p . i) * (Line MR,i)) . j by RVSUM_1:66 ; :: thesis: verum

end;

hence Line MR1,i = (p . i) * (Line MR,i) by A6, FINSEQ_1:17; :: thesis: verum

end;

end;

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

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices MR1 implies MR1 * i,j = (p . i) * (MR * i,j) )
assume A12: [i,j] in Indices MR1 ; :: thesis: MR1 * i,j = (p . i) * (MR * i,j)
A13: ( i in dom MR1 & j in dom (MR1 . i) ) by A12, MATRPROB:13;
A14: j in Seg (width MR1) by A12, MATRPROB:12;
hence MR1 * i,j = (Line MR1,i) . j by MATRIX_1:def 8
.= ((p . i) * (Line MR,i)) . j by A11, A13
.= (p . i) * ((Line MR,i) . j) by RVSUM_1:66
.= (p . i) * (MR * i,j) by A11, A14, MATRIX_1:def 8 ;
:: thesis: verum

end;

hence MR1 = (Vec2DiagMx p) * MR by A1, A11, Th26; :: thesis: verum