let F be RealNormSpace; :: thesis: for x0 being Real
for f being PartFunc of REAL, the carrier of F
for r being Real st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let x0 be Real; :: thesis: for f being PartFunc of REAL, the carrier of F
for r being Real 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 REAL, the carrier of F; :: thesis: for r being Real 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: ( 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 LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
consider L1 being LinearFunc of F, R1 being RestFunc of F such that
A4: for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A3;
reconsider R = r (#) R1 as RestFunc of F by Th8;
reconsider L = r (#) L1 as LinearFunc of F by Th4;
A5: N1 c= dom (r (#) f) by A2, VFUNCT_1:def 4;
R1 is total by Def1;
then r (#) R1 is total by VFUNCT_1:34;
then A6: dom (r (#) R1) = REAL by FUNCT_2:def 1;
r (#) L1 is total by VFUNCT_1:34;
then A7: dom (r (#) L1) = REAL by FUNCT_2:def 1;

A8: now :: thesis: for x being Real st x in N1 holds
((r (#) f) /. x) - ((r (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0))

let x be Real; :: thesis: ( x in N1 implies ((r (#) f) /. x) - ((r (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A9: x0 in N1 by RCOMP_1:16;
A10: x - x0 in REAL by XREAL_0:def 1;
assume A11: x in N1 ; :: thesis: ((r (#) f) /. x) - ((r (#) f) /. x0) = (L /. (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, A9, VFUNCT_1:def 4
.= r * ((f /. x) - (f /. x0)) by RLVECT_1:34
.= r * ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A4, A11
.= (r * (L1 /. (x - x0))) + (r * (R1 /. (x - x0))) by RLVECT_1:def 5
.= (L /. (x - x0)) + (r * (R1 /. (x - x0))) by A7, VFUNCT_1:def 4, A10
.= (L /. (x - x0)) + (R /. (x - x0)) by A6, VFUNCT_1:def 4, A10 ;
:: 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) = L /. jj by A5, A8, Def4
.= L /. jj
.= r * (L1 /. jj) by A7, VFUNCT_1:def 4
.= r * (L1 /. jj)
.= r * (diff (f,x0)) by A1, A2, A4, Def4 ;
:: thesis: verum