theorem :: NDIFF14:8

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat
for f, g, h being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) holds
( h = f + g iff for x being Element of Z holds h . x = (f . x) + (g . x) )