theorem Th45: :: REAL_3:45
for r being Real st (scf r) . 0 > 0 holds
for n being Nat holds (c_n r) . n > 0