:: deftheorem Def1 defines alternating_series LEIBNIZ1:def 1 :
for a, b₂ being Real_Sequence holds
( b₂ = alternating_series a iff for i being Nat holds b₂ . i = ((- 1) |^ i) * (a . i) );