let r be Real; :: thesis:
let Z be open Subset of REAL ; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
assume that
A1: Z c= dom (r (#) f) and
A2: f is_differentiable_on Z ; :: thesis:

let x0 be Real; :: thesis:
assume x0 in Z ; :: thesis:
then f is_differentiable_in x0 by A2, Th16;
hence r (#) f is_differentiable_in x0 by Th23; :: thesis:

end;

hence A3: r (#) f is_differentiable_on Z by A1, Th16; :: thesis:

let x be Real; :: thesis:
assume A4: x in Z ; :: thesis:
then A5: f is_differentiable_in x by A2, Th16;
thus ((r (#) f) `| Z) . x = diff (r (#) f),x by A3, A4, Def8
.= r * (diff f,x) by A5, Th23 ; :: thesis:

end;

hence for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff f,x) ; :: thesis: