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;

hence diff ((r (#) f),x0) = r * L1 by A5, A7, Def7

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

:: thesis: verum

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

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

hence diff ((r (#) f),x0) = r * L1 by A5, A7, Def7

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

:: thesis: verum