theorem Th27: :: REAL_3:27

for n, m being Nat
for r being Real st (rfs r) . n = 0 & n <= m holds
(rfs r) . m = 0