:: deftheorem Def10 defines ColSum MATRIXC1:def 10 :
for M being Matrix of COMPLEX
for b₂ being FinSequence of COMPLEX holds
( b₂ = ColSum M iff ( len b₂ = width M & ( for j being Nat st j in Seg (width M) holds
b₂ . j = Sum (Col (M,j)) ) ) );