:: deftheorem Def13 defines ReciTriangRS NUMPOLY1:def 13 :
for b₁ being Real_Sequence holds
( b₁ = ReciTriangRS iff for i being Nat holds b₁ . i = 1 / (Triangle i) );