:: deftheorem Def1 defines JSum BOR_CANT:def 1 :
for s, b₂ being Real_Sequence holds
( b₂ = JSum s iff for d being Nat holds b₂ . d = Sum ((- (s . d)) rExpSeq) );