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)) ) ) ) )
set MM = Vec2DiagMx p;
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)) ) ) )

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)) ) )
hence ( len MR1 = len p & width MR1 = width MR ) by A1, Th26; :: thesis: for i being Element of NAT st i in dom MR1 holds
Line (MR1,i) = (p . i) * (Line (MR,i))
A3: width MR1 = width MR by A1, A2, Th26;
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 i in dom MR1 ; :: thesis: Line (MR1,i) = (p . i) * (Line (MR,i))
then A4: i in Seg (len MR1) by FINSEQ_1:def 3;
A5: 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 j in dom (Line (MR1,i)) ; :: thesis: (Line (MR1,i)) . j = ((p . i) * (Line (MR,i))) . j
then j in Seg (len (Line (MR1,i))) by FINSEQ_1:def 3;
then A6: j in Seg (width MR1) by MATRIX_1:def 8;
then A7: [i,j] in Indices MR1 by A4, MATRPROB:12;
A8: j in NAT by ORDINAL1:def 13;
thus (Line (MR1,i)) . j = MR1 * (i,j) by A6, MATRIX_1:def 8
.= (p . i) * (MR * (i,j)) by A1, A2, A8, A7, Th26
.= (p . i) * ((Line (MR,i)) . j) by A3, A6, MATRIX_1:def 8
.= ((p . i) * (Line (MR,i))) . j by RVSUM_1:66 ; :: thesis: verum

end;

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 ;
hence Line (MR1,i) = (p . i) * (Line (MR,i)) by A5, FINSEQ_1:17; :: thesis: verum

end;

end;

assume that
A9: len MR1 = len p and
A10: width MR1 = width MR and
A11: 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 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 A10, A14, MATRIX_1:def 8 ;
:: thesis: verum

end;

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