:: deftheorem Def8 defines Sum FLEXARY1:def 8 :
for f being FinSequence-yielding complex-functions-valued Function
for b₂ being complex-valued Function holds
( b₂ = Sum f iff ( dom b₂ = dom f & ( for x being set holds b₂ . x = Sum (f . x) ) ) );