:: deftheorem Def2 defines +... FLEXARY1:def 2 :
for n being Nat
for f being complex-valued Function st (dom f) /\ NAT is finite holds
for b₃ being complex number holds
( b₃ = (f,n) +... iff for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
b₃ = (f,n) +...+ (f,k) );