theorem Th10: :: NDIFF14:10

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat holds 0. (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) = Z --> (0. Y)