theorem Th7: :: NDIFF14:7

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat
for v, u being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )