theorem Th7: :: NDIFF_3:7

for F being RealNormSpace
for R1, R2 being RestFunc of F holds
( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )