theorem :: REAL_3:48

for r being Real st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat holds (c_n r) . n >= tau |^ n