let S, T be RealNormSpace; :: thesis: for r being Real
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let r be Real; :: thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let x0 be Point of S; :: thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) )
assume A1: f is_differentiable_in x0 ; :: thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
then consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that
A4: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A3;
reconsider R = r (#) R1 as RestFunc of S,T by Th29;
set L = r * L1;
A5: N1 c= dom (r (#) f) by A2, VFUNCT_1:def 4;
A6: R1 is total by Def5;
hence r (#) f is_differentiable_in x0 by A5; :: thesis: diff ((r (#) f),x0) = r * (diff (f,x0))
hence diff ((r (#) f),x0) = r * L1 by A5, A7, Def7
.= r * (diff (f,x0)) by A1, A2, A4, Def7 ;
:: thesis: verum