theorem :: FDIFF_1:27

ex R being RestFunc st
( R . 0 = 0 & R is_continuous_in 0 )