let M be Matrix of REAL ; :: thesis: for p being FinSequence of REAL st width M = len p & width M > 0 holds
for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line M,i) "*" p
let p be FinSequence of REAL ; :: thesis: ( width M = len p & width M > 0 implies for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line M,i) "*" p )
assume A1: ( width M = len p & width M > 0 ) ; :: thesis: for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line M,i) "*" p
A2: len (M * p) = len (Col (M * (ColVec2Mx p)),1) by MATRIXR1:def 11
.= len (M * (ColVec2Mx p)) by MATRIX_1:def 9 ;

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: ( i in Seg (len (M * p)) implies (Line M,i) "*" p = (M * p) . i )
assume A3: i in Seg (len (M * p)) ; :: thesis: (Line M,i) "*" p = (M * p) . i
i in dom (M * (ColVec2Mx p)) by A2, A3, FINSEQ_1:def 3;
then A4: (Col (M * (ColVec2Mx p)),1) . i = (M * (ColVec2Mx p)) * i,1 by MATRIX_1:def 9;
A5: len (ColVec2Mx p) = width M by A1, MATRIXR1:def 9;
then width (M * (ColVec2Mx p)) = width (ColVec2Mx p) by Th39;
then width (M * (ColVec2Mx p)) = 1 by A1, MATRIXR1:def 9;
then 1 in Seg (width (M * (ColVec2Mx p))) by FINSEQ_1:3;
then [i,1] in Indices (M * (ColVec2Mx p)) by A2, A3, Th12;
then (M * (ColVec2Mx p)) * i,1 = (Line M,i) "*" (Col (ColVec2Mx p),1) by A5, Th39
.= (Line M,i) "*" p by A1, MATRIXR1:45 ;
hence (Line M,i) "*" p = (M * p) . i by A4, MATRIXR1:def 11; :: thesis: verum

end;