theorem Th18: :: ORDEQ_01:18

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds
f + g = f1 + g1