:: deftheorem Def6 defines Sum MATRLIN:def 6 :
for V1 being non empty addLoopStr
for M being FinSequence of the carrier of V1 *
for b₃ being FinSequence of V1 holds
( b₃ = Sum M iff ( len b₃ = len M & ( for k being Nat st k in dom b₃ holds
b₃ /. k = Sum (M /. k) ) ) );