let r be Real; :: thesis: for A being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on A holds
( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) )
let A be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on A holds
( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on A implies ( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) ) )
assume A1: f is_differentiable_on A ; :: thesis: ( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) )
then A c= dom f ;
then A2: A c= dom (r (#) f) by VALUED_1:def 5;
then r (#) f is_differentiable_on A by A1, FDIFF_1:20;
then A3: dom ((r (#) f) `| A) = A by FDIFF_1:def 7;
dom (f `| A) = A by A1, FDIFF_1:def 7;
then A4: dom (r (#) (f `| A)) = A by VALUED_1:def 5;

now :: thesis: for x0 being Element of REAL st x0 in A holds
((r (#) f) `| A) . x0 = (r (#) (f `| A)) . x0

let x0 be Element of REAL ; :: thesis: ( x0 in A implies ((r (#) f) `| A) . x0 = (r (#) (f `| A)) . x0 )
assume A5: x0 in A ; :: thesis: ((r (#) f) `| A) . x0 = (r (#) (f `| A)) . x0
hence ((r (#) f) `| A) . x0 = r * (diff (f,x0)) by A1, A2, FDIFF_1:20
.= r * ((f `| A) . x0) by A1, A5, FDIFF_1:def 7
.= (r (#) (f `| A)) . x0 by A4, A5, VALUED_1:def 5 ;
:: thesis: verum

end;

hence ( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) ) by A1, A2, A3, A4, FDIFF_1:20, PARTFUN1:5; :: thesis: verum