:: deftheorem Def9 defines LineSum MATRIXC1:def 9 :
for M being Matrix of COMPLEX
for b₂ being FinSequence of COMPLEX holds
( b₂ = LineSum M iff ( len b₂ = len M & ( for i being Nat st i in Seg (len M) holds
b₂ . i = Sum (Line (M,i)) ) ) );