theorem Th40: :: MATRPROB:40

for M being Matrix of REAL
for p being FinSequence of REAL st len M = len p holds
for i being Nat st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col (M,i))