for D being non empty set
for F being FinSequence_of_Matrix of D st Sum (Len F) = 0 holds
Sum (Width F) = 0