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