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 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 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 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_0:def 8 ;

hereby :: thesis: verum

let i be 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_0:def 8;
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))) ;
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;