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