for m being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1