:: deftheorem Def4 defines SimpleContinuedFraction REAL_3:def 4 :
for r being Real
for b₂ being Integer_Sequence holds
( b₂ = SimpleContinuedFraction r iff for n being Nat holds b₂ . n = [\((rfs r) . n)/] );