theorem Th5: :: FDIFF_1:5

for r being Real
for R being RestFunc holds r (#) R is RestFunc