let r be Real; :: thesis: ( ( for n being Nat holds (scf r) . n = 0 ) implies r = 0 )
assume for n being Nat holds (scf r) . n = 0 ; :: thesis: r = 0
then (rfs r) . 0 = 0 by Th33;
hence r = 0 by Def3; :: thesis: verum