:: deftheorem Def14 defines SumsReciTriang NUMPOLY1:def 14 :
for b₁ being Real_Sequence holds
( b₁ = SumsReciTriang iff for n being Nat holds b₁ . n = 2 - (2 / (n + 1)) );