let F be RealNormSpace; :: thesis: for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
let r be Real; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
let f be PartFunc of REAL, the carrier of F; :: thesis: ( Z c= dom (r (#) f) & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) )
assume that
A1: Z c= dom (r (#) f) and
A2: f is_differentiable_on Z ; :: thesis: ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )

now :: thesis: for x0 being Real st x0 in Z holds
r (#) f is_differentiable_in x0

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

end;

hence A3: r (#) f is_differentiable_on Z by A1, Th10; :: thesis: for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x))
let x be Real; :: thesis: ( x in Z implies ((r (#) f) `| Z) . x = r * (diff (f,x)) )
assume A4: x in Z ; :: thesis: ((r (#) f) `| Z) . x = r * (diff (f,x))
then A5: f is_differentiable_in x by A2, Th10;
thus ((r (#) f) `| Z) . x = diff ((r (#) f),x) by A3, A4, Def6
.= r * (diff (f,x)) by A5, Th16 ; :: thesis: verum