theorem Th7: :: INTEGRA7:7

for r being Real
for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
r (#) f is_differentiable_on X