let T, S be non trivial 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 & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST 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)) ) by Def6;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators S,T), R1 being REST of S,T such that
A3: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A2;
set L = r * L1;
reconsider R = r (#) R1 as REST of S,T by Th34;
A4: R1 is total by Def5;
A5: N1 c= dom (r (#) f) by A2, VFUNCT_1:def 4;

A6: now

let x be Point of S; :: thesis: ( x in N1 implies ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0)) )
assume A7: x in N1 ; :: thesis: ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0))
A8: x0 in N1 by NFCONT_1:4;
thus ((r (#) f) /. x) - ((r (#) f) /. x0) = (r * (f /. x)) - ((r (#) f) /. x0) by A5, A7, VFUNCT_1:def 4
.= (r * (f /. x)) - (r * (f /. x0)) by A5, A8, VFUNCT_1:def 4
.= r * ((f /. x) - (f /. x0)) by RLVECT_1:48
.= r * ((L1 . (x - x0)) + (R1 /. (x - x0))) by A3, A7
.= (r * (L1 . (x - x0))) + (r * (R1 /. (x - x0))) by RLVECT_1:def 9
.= ((r * L1) . (x - x0)) + (r * (R1 /. (x - x0))) by LOPBAN_1:42
.= ((r * L1) . (x - x0)) + (R /. (x - x0)) by A4, VFUNCT_1:45 ; :: thesis: verum

end;

hence r (#) f is_differentiable_in x0 by A5, Def6; :: thesis: diff (r (#) f),x0 = r * (diff f,x0)
hence diff (r (#) f),x0 = r * L1 by A5, A6, Def7
.= r * (diff f,x0) by A1, A2, A3, Def7 ;
:: thesis: verum