let F be RealNormSpace; 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; 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; 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; ( 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
; ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
hence A3:
r (#) f is_differentiable_on Z
by A1, Th10; for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x))
let x be Real; ( x in Z implies ((r (#) f) `| Z) . x = r * (diff (f,x)) )
assume A4:
x in Z
; ((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
; verum