theorem Th34: :: REAL_3:34
for r being Real st ( for n being Nat holds (scf r) . n = 0 ) holds
r = 0