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)) ) )

reconsider j = 1 as Element of REAL by XREAL_0:def 1;

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 ex R being RestFunc st

for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ;

consider L1 being LinearFunc, R1 being RestFunc 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 by Th5;

reconsider L = r (#) L1 as LinearFunc by Th3;

A5: L1 is total by Def3;

A6: N1 c= dom (r (#) f) by A2, VALUED_1:def 5;

A7: R1 is total by Def2;

hence diff ((r (#) f),x0) = L . 1 by A6, A8, Def5

.= r * (L1 . j) by A5, RFUNCT_1:57

.= r * (diff (f,x0)) by A1, A2, A4, Def5 ;

:: thesis: verum

( 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)) ) )

reconsider j = 1 as Element of REAL by XREAL_0:def 1;

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 ex R being RestFunc st

for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ;

consider L1 being LinearFunc, R1 being RestFunc 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 by Th5;

reconsider L = r (#) L1 as LinearFunc by Th3;

A5: L1 is total by Def3;

A6: N1 c= dom (r (#) f) by A2, VALUED_1:def 5;

A7: R1 is total by Def2;

A8: now :: thesis: for x being Real st x in N1 holds

((r (#) f) . x) - ((r (#) f) . x0) = (L . (x - x0)) + (R . (x - x0))

hence
r (#) f is_differentiable_in x0
by A6; :: thesis: diff ((r (#) f),x0) = r * (diff (f,x0))((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;

reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume A10: 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 A6, 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 A4, A10

.= (r * (L1 . (x - x0))) + (r * (R1 . (x - x0)))

.= (L . (xx - xx0)) + (r * (R1 . (xx - xx0))) by A5, RFUNCT_1:57

.= (L . (x - x0)) + (R . (x - x0)) by A7, RFUNCT_1:57 ;

:: thesis: verum

end;A9: x0 in N1 by RCOMP_1:16;

reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume A10: 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 A6, 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 A4, A10

.= (r * (L1 . (x - x0))) + (r * (R1 . (x - x0)))

.= (L . (xx - xx0)) + (r * (R1 . (xx - xx0))) by A5, RFUNCT_1:57

.= (L . (x - x0)) + (R . (x - x0)) by A7, RFUNCT_1:57 ;

:: thesis: verum

hence diff ((r (#) f),x0) = L . 1 by A6, A8, Def5

.= r * (L1 . j) by A5, RFUNCT_1:57

.= r * (diff (f,x0)) by A1, A2, A4, Def5 ;

:: thesis: verum