for r being Real holds
( r is rational iff ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0 )