theorem Th21: :: FDIFF_12:21

for f being PartFunc of REAL,REAL
for x0, r being Real st f is_right_differentiable_in x0 holds
( r (#) f is_right_differentiable_in x0 & Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0)) )