let F be RealNormSpace; 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; 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; 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; ( 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
; ( 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;
hence
r (#) f is_differentiable_in x0
by A5; 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
;
verum