theorem Th22: :: FDIFF_12:22

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