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 by FDIFF_1:def 7;
then A2: A c= dom (r (#) f) by VALUED_1:def 5;
then ( r (#) f is_differentiable_on A & ( for x0 being Real st x0 in A holds
((r (#) f) `| A) . x0 = r * (diff f,x0) ) ) by A1, FDIFF_1:28;
then A3: dom ((r (#) f) `| A) = A by FDIFF_1:def 8;
dom (f `| A) = A by A1, FDIFF_1:def 8;
then A4: dom (r (#) (f `| A)) = A by VALUED_1:def 5;

now

let x0 be 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:28
.= r * ((f `| A) . x0) by A1, A5, FDIFF_1:def 8
.= (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:28, PARTFUN1:34; :: thesis: verum