theorem :: MATRPROB:51

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