let f be PartFunc of REAL,REAL; :: thesis: 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)) )
let x0, r be Real; :: thesis: ( f is_left_differentiable_in x0 implies ( r (#) f is_left_differentiable_in x0 & Ldiff ((r (#) f),x0) = r * (Ldiff (f,x0)) ) )
assume A1: f is_left_differentiable_in x0 ; :: thesis: ( r (#) f is_left_differentiable_in x0 & Ldiff ((r (#) f),x0) = r * (Ldiff (f,x0)) )
then ( r = 0 implies ( r (#) f is_left_differentiable_in x0 & Ldiff ((r (#) f),x0) = r * (Ldiff (f,x0)) ) ) by Lm17;
hence ( r (#) f is_left_differentiable_in x0 & Ldiff ((r (#) f),x0) = r * (Ldiff (f,x0)) ) by A1, Lm19; :: thesis: verum