theorem :: NDIFF_3:25

for F being RealNormSpace ex R being RestFunc of F st
( R /. 0 = 0. F & R is_continuous_in 0 )