:: deftheorem Def2 defines ColSum MATRPROB:def 2 :
for m being Matrix of REAL
for b₂ being FinSequence of REAL 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)) ) ) );