let f be PartFunc of REAL,REAL; :: thesis:
let I be non empty Interval; :: thesis:
let r be Real; :: thesis:
assume A1: f is_differentiable_on_interval I ; :: thesis:
then A2: I c= dom (r (#) f) by VALUED_1:def 5;
A3: f is_differentiable_on ].(inf I),(sup I).[ by A1;
for x being Real st x in ].(inf I),(sup I).[ holds
(r (#) f) | ].(inf I),(sup I).[ is_differentiable_in x

let x be Real; :: thesis:
assume x in ].(inf I),(sup I).[ ; :: thesis:
then f | ].(inf I),(sup I).[ is_differentiable_in x by A3;
then r (#) (f | ].(inf I),(sup I).[) is_differentiable_in x by FDIFF_1:15;
hence (r (#) f) | ].(inf I),(sup I).[ is_differentiable_in x by RFUNCT_1:49; :: thesis:

end;

then r (#) f is_differentiable_on ].(inf I),(sup I).[ by A3, VALUED_1:def 5;
hence A4: r (#) f is_differentiable_on_interval I by A1, Th21, Th22, VALUED_1:def 5; :: thesis:
then A5: dom ((r (#) f) `\ I) = I by Def2;
dom (f `\ I) = I by A1, Def2;
then A6: dom (r (#) (f `\ I)) = I by VALUED_1:def 5;
A7: for x being Element of REAL st x in dom ((r (#) f) `\ I) holds
((r (#) f) `\ I) . x = (r (#) (f `\ I)) . x

let x be Element of REAL ; :: thesis:
assume A8: x in dom ((r (#) f) `\ I) ; :: thesis:
then A9: x in I by A4, Def2;

suppose A10: x = inf I ; :: thesis:

then A11: inf I = lower_bound I by A9, Lm5;
A12: (f `\ I) . x = Rdiff (f,x) by A1, A9, A10, Def2;
((r (#) f) `\ I) . x = Rdiff ((r (#) f),x) by A4, A9, A10, Def2;
then ((r (#) f) `\ I) . x = r * ((f `\ I) . x) by A1, A8, A4, Def2, A10, A11, A12, Th21;
hence ((r (#) f) `\ I) . x = (r (#) (f `\ I)) . x by A5, A6, A8, VALUED_1:def 5; :: thesis:

end;

suppose A13: x = sup I ; :: thesis:

then A14: sup I = upper_bound I by A9, Lm6;
A15: (f `\ I) . x = Ldiff (f,x) by A1, A9, A13, Def2;
((r (#) f) `\ I) . x = Ldiff ((r (#) f),x) by A4, A9, A13, Def2;
then ((r (#) f) `\ I) . x = r * ((f `\ I) . x) by A1, A8, A4, Def2, A13, A14, A15, Th22;
hence ((r (#) f) `\ I) . x = (r (#) (f `\ I)) . x by A5, A6, A8, VALUED_1:def 5; :: thesis:

end;

suppose A16: ( x <> inf I & x <> sup I ) ; :: thesis:

then A17: ( (f `\ I) . x = diff (f,x) & ((r (#) f) `\ I) . x = diff ((r (#) f),x) ) by A1, A4, A9, Def2;
reconsider J = ].(inf I),(sup I).[ as open Subset of REAL by Th2;
J c= I by Th2;
then A18: J c= dom (r (#) f) by A2;
then A19: r (#) f is_differentiable_on J by A1, FDIFF_1:20;
( inf I <= x & x <= sup I ) by A9, XXREAL_2:61, XXREAL_2:62;
then A20: ( inf I < x & x < sup I ) by A16, XXREAL_0:1;
then x in J by XXREAL_1:4;
then ( ((r (#) f) `| J) . x = diff ((r (#) f),x) & (f `| J) . x = diff (f,x) ) by A1, A19, FDIFF_1:def 7;
then ((r (#) f) `\ I) . x = r * ((f `\ I) . x) by A17, A20, A18, A1, FDIFF_1:20, XXREAL_1:4;
hence ((r (#) f) `\ I) . x = (r (#) (f `\ I)) . x by A5, A6, A8, VALUED_1:def 5; :: thesis:

end;

end;

end;

hence (r (#) f) `\ I = r (#) (f `\ I) by A5, A6, PARTFUN1:5; :: thesis:

hereby :: thesis:

let x be Real; :: thesis:
assume A21: x in I ; :: thesis:
then ((r (#) f) `\ I) . x = (r (#) (f `\ I)) . x by A5, A7;
hence ((r (#) f) `\ I) . x = r * ((f `\ I) . x) by A21, A6, VALUED_1:def 5; :: thesis:

end;