let r be Real; :: 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 ;
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:8;
reconsider Z = Z as open Subset of REAL by A1, FDIFF_1:10;
X c= dom f by A1;
then Z c= dom (r (#) f) by VALUED_1:def 5;
then r1 (#) f is_differentiable_on X by A1, FDIFF_1:20;
hence r (#) f is_differentiable_on X ; :: thesis: verum