let r be real number ; :: thesis: for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
r (#) f is_differentiable_on X
let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
r (#) f is_differentiable_on X
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on X implies r (#) f is_differentiable_on X )
reconsider r1 = r as Real by XREAL_0:def 1;
assume A1: f is_differentiable_on X ; :: thesis: r (#) f is_differentiable_on X
then reconsider Z = X as Subset of REAL by FDIFF_1:15;
reconsider Z = Z as open Subset of REAL by A1, FDIFF_1:17;
X c= dom f by A1, FDIFF_1:def 7;
then Z c= dom (r (#) f) by VALUED_1:def 5;
then r1 (#) f is_differentiable_on X by A1, FDIFF_1:28;
hence r (#) f is_differentiable_on X ; :: thesis: verum