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