:: deftheorem Def10 defines Sum RVSUM_1:def 10 :
for F being complex-valued FinSequence
for b₂ being Complex holds
( b₂ = Sum F iff ex f being FinSequence of COMPLEX st
( f = F & b₂ = addcomplex $$ f ) );