theorem :: NDIFF14:6

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat holds RLSStruct(# (Continuously_differentiable_Functions (Z,Y,n)),(Zero_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Add_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Mult_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))) #) is Subspace of RealVectSpace (Z,Y) by Th5, RSSPACE:11;