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