theorem Th21: :: INTEGRA8:21

for R1 being RestFunc holds - R1 is RestFunc