theorem Th41: :: MATRPROB:41

for M being Matrix of REAL
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