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 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 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 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 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 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 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 Nat st i in dom MR1 holds
Line (MR1,i) = (p . i) * (Line (MR,i)) :: thesis: verum

proof

let i be 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_0:def 7;
then A7: [i,j] in Indices MR1 by A4, MATRPROB:12;
thus (Line (MR1,i)) . j = MR1 * (i,j) by A6, MATRIX_0:def 7
.= (p . i) * (MR * (i,j)) by A1, A2, A7, Th26
.= (p . i) * ((Line (MR,i)) . j) by A3, A6, MATRIX_0:def 7
.= ((p . i) * (Line (MR,i))) . j by RVSUM_1:44 ; :: thesis: verum

end;

dom (Line (MR1,i)) = Seg (len (Line (MR1,i))) by FINSEQ_1:def 3
.= Seg (width MR1) by MATRIX_0:def 7
.= Seg (len (Line (MR,i))) by A3, MATRIX_0:def 7
.= 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:13; :: thesis: verum

end;

end;

assume that
A8: len MR1 = len p and
A9: width MR1 = width MR and
A10: for i being Nat st i in dom MR1 holds
Line (MR1,i) = (p . i) * (Line (MR,i)) ; :: thesis: MR1 = (Vec2DiagMx p) * MR
for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices MR1 implies MR1 * (i,j) = (p . i) * (MR * (i,j)) )
assume A11: [i,j] in Indices MR1 ; :: thesis: MR1 * (i,j) = (p . i) * (MR * (i,j))
A12: i in dom MR1 by A11, MATRPROB:13;
A13: j in Seg (width MR1) by A11, MATRPROB:12;
hence MR1 * (i,j) = (Line (MR1,i)) . j by MATRIX_0:def 7
.= ((p . i) * (Line (MR,i))) . j by A10, A12
.= (p . i) * ((Line (MR,i)) . j) by RVSUM_1:44
.= (p . i) * (MR * (i,j)) by A9, A13, MATRIX_0:def 7 ;
:: thesis: verum

end;

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