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

let x0 be Point of S; :: thesis:
assume x0 in Z ; :: thesis:
then f is_differentiable_in x0 by A1, A3, Th31;
hence r (#) f is_differentiable_in x0 by Th37; :: thesis:

end;

hence A4: r (#) f is_differentiable_on Z by A1, A2, Th31; :: thesis:

let x be Point of S; :: thesis:
assume A5: x in Z ; :: thesis:
then A6: f is_differentiable_in x by A1, A3, Th31;
thus ((r (#) f) `| Z) /. x = diff ((r (#) f),x) by A4, A5, Def9
.= r * (diff (f,x)) by A6, Th37 ; :: thesis:

end;

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