theorem Th20: :: MATRPROB:20

for m being Matrix of REAL holds
( len (Sum m) = len m & ( for i being Nat st i in Seg (len m) holds
(Sum m) . i = Sum (Line (m,i)) ) )