theorem Th50: :: MATRPROB:50

for x being FinSequence of REAL
for M being Matrix of REAL st len x = len M & x = (len x) |-> 1 holds
for k being Nat st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))