let S, T be RealNormSpace; :: thesis: for Z being Subset of S st Z is open holds

for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

let Z be Subset of S; :: thesis: ( Z is open implies for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) )

assume A1: Z is open ; :: thesis: for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

let r be Real; :: thesis: for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

let f be PartFunc of S,T; :: thesis: ( Z c= dom (r (#) f) & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) )

assume that

A2: Z c= dom (r (#) f) and

A3: f is_differentiable_on Z ; :: thesis: ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

((r (#) f) `| Z) /. x = r * (diff (f,x))

((r (#) f) `| Z) /. x = r * (diff (f,x)) ; :: thesis: verum

for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

let Z be Subset of S; :: thesis: ( Z is open implies for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) )

assume A1: Z is open ; :: thesis: for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

let r be Real; :: thesis: for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

let f be PartFunc of S,T; :: thesis: ( Z c= dom (r (#) f) & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) )

assume that

A2: Z c= dom (r (#) f) and

A3: f is_differentiable_on Z ; :: thesis: ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )

now :: thesis: for x0 being Point of S st x0 in Z holds

r (#) f is_differentiable_in x0

hence A4:
r (#) f is_differentiable_on Z
by A1, A2, Th31; :: thesis: for x being Point of S st x in Z holds r (#) f is_differentiable_in x0

let x0 be Point of S; :: 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 A1, A3, Th31;

hence r (#) f is_differentiable_in x0 by Th37; :: thesis: verum

end;assume x0 in Z ; :: thesis: r (#) f is_differentiable_in x0

then f is_differentiable_in x0 by A1, A3, Th31;

hence r (#) f is_differentiable_in x0 by Th37; :: thesis: verum

((r (#) f) `| Z) /. x = r * (diff (f,x))

now :: thesis: for x being Point of S st x in Z holds

((r (#) f) `| Z) /. x = r * (diff (f,x))

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

let x be Point of S; :: thesis: ( x in Z implies ((r (#) f) `| Z) /. x = r * (diff (f,x)) )

assume A5: x in Z ; :: thesis: ((r (#) f) `| Z) /. x = r * (diff (f,x))

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: verum

end;assume A5: x in Z ; :: thesis: ((r (#) f) `| Z) /. x = r * (diff (f,x))

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: verum

((r (#) f) `| Z) /. x = r * (diff (f,x)) ; :: thesis: verum