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;

A7: now :: thesis: for x being Point of S st x in N1 holds
((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0))

let x be Point of S; :: thesis: ( x in N1 implies ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0)) )
A8: x0 in N1 by NFCONT_1:4;
assume A9: x in N1 ; :: thesis: ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0))
hence ((r (#) f) /. x) - ((r (#) f) /. x0) = (r * (f /. x)) - ((r (#) f) /. x0) by A5, 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:34
.= r * ((L1 . (x - x0)) + (R1 /. (x - x0))) by A4, A9
.= (r * (L1 . (x - x0))) + (r * (R1 /. (x - x0))) by RLVECT_1:def 5
.= ((r * L1) . (x - x0)) + (r * (R1 /. (x - x0))) by LOPBAN_1:36
.= ((r * L1) . (x - x0)) + (R /. (x - x0)) by A6, VFUNCT_1:39 ;
:: thesis: verum

end;

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