theorem Th5: :: FDIFF_1:5
for r being Real
for R being RestFunc holds r (#) R is RestFunc