:: deftheorem Def1 defines Sum MATRPROB:def 1 :
for e being FinSequence of REAL *
for b₂ being FinSequence of REAL holds
( b₂ = Sum e iff ( len b₂ = len e & ( for k being Nat st k in dom b₂ holds
b₂ . k = Sum (e . k) ) ) );