:: deftheorem Def6 defines convergent_denominators REAL_3:def 6 :
for r being Real
for b₂ being Real_Sequence holds
( b₂ = convergent_denominators r iff ( b₂ . 0 = 1 & b₂ . 1 = (scf r) . 1 & ( for n being Nat holds b₂ . (n + 2) = (((scf r) . (n + 2)) * (b₂ . (n + 1))) + (b₂ . n) ) ) );