:: deftheorem Def3 defines remainders_for_scf REAL_3:def 3 :
for r being Real
for b₂ being Real_Sequence holds
( b₂ = remainders_for_scf r iff ( b₂ . 0 = r & ( for n being Nat holds b₂ . (n + 1) = 1 / (frac (b₂ . n)) ) ) );