:: deftheorem Def8 defines backContinued_fraction REAL_3:def 8 :
for r being Real
for b₂ being Real_Sequence holds
( b₂ = backContinued_fraction r iff ( b₂ . 0 = (scf r) . 0 & ( for n being Nat holds b₂ . (n + 1) = (1 / (b₂ . n)) + ((scf r) . (n + 1)) ) ) );