theorem Th16: :: MEASURE9:18

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