:: deftheorem defines RVectSp_Continuously_differentiable_Funcs NDIFF14:def 2 :
for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat holds RVectSp_Continuously_differentiable_Funcs (Z,Y,n) = 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)))) #);