theorem Th4: :: FDIFF_1:4
for R1, R2 being RestFunc holds
( R1 + R2 is RestFunc & R1 - R2 is RestFunc & R1 (#) R2 is RestFunc )