let x0, r be Real; :: thesis: for f being PartFunc of REAL ,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 ,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 & ex L being LINEAR ex R being REST st
for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Def5;
consider L1 being LINEAR, R1 being REST such that
A3: for x being Real st x in N1 holds
(f . x) - (f . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A2;
reconsider L = r (#) L1 as LINEAR by Th7;
reconsider R = r (#) R1 as REST by Th9;
A4: L1 is total by Def4;
A5: R1 is total by Def3;
A6: N1 c= dom (r (#) f) by A2, VALUED_1:def 5;

A7: now

let x be Real; :: thesis: ( x in N1 implies ((r (#) f) . x) - ((r (#) f) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A8: x in N1 ; :: thesis: ((r (#) f) . x) - ((r (#) f) . x0) = (L . (x - x0)) + (R . (x - x0))
A9: x0 in N1 by RCOMP_1:37;
thus ((r (#) f) . x) - ((r (#) f) . x0) = (r * (f . x)) - ((r (#) f) . x0) by A6, A8, VALUED_1:def 5
.= (r * (f . x)) - (r * (f . x0)) by A6, A9, VALUED_1:def 5
.= r * ((f . x) - (f . x0))
.= r * ((L1 . (x - x0)) + (R1 . (x - x0))) by A3, A8
.= (r * (L1 . (x - x0))) + (r * (R1 . (x - x0)))
.= (L . (x - x0)) + (r * (R1 . (x - x0))) by A4, RFUNCT_1:73
.= (L . (x - x0)) + (R . (x - x0)) by A5, RFUNCT_1:73 ; :: thesis: verum

end;

hence r (#) f is_differentiable_in x0 by A6, Def5; :: thesis: diff (r (#) f),x0 = r * (diff f,x0)
hence diff (r (#) f),x0 = L . 1 by A6, A7, Def6
.= r * (L1 . 1) by A4, RFUNCT_1:73
.= r * (diff f,x0) by A1, A2, A3, Def6 ;
:: thesis: verum