let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
let f be PartFunc of REAL,REAL; ( Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) ) )
reconsider j = 1 as Element of REAL by XREAL_0:def 1;
reconsider cf = REAL --> (In (0,REAL)) as Function of REAL,REAL ;
set R = cf;
then reconsider R = cf as RestFunc by Def2;
reconsider L = id REAL as PartFunc of REAL,REAL ;
for p being Real holds L . p = 1 * p
by XREAL_0:def 1, FUNCT_1:18;
then reconsider L = L as LinearFunc by Def3;
assume that
A7:
Z c= dom f
and
A8:
f | Z = id Z
; ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
hence A15:
f is_differentiable_on Z
by A7, Th9; for x being Real st x in Z holds
(f `| Z) . x = 1
let x0 be Real; ( x0 in Z implies (f `| Z) . x0 = 1 )
assume A16:
x0 in Z
; (f `| Z) . x0 = 1
then consider N1 being Neighbourhood of x0 such that
A17:
N1 c= Z
by RCOMP_1:18;
A18:
f is_differentiable_in x0
by A11, A16;
then
ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
;
then consider N being Neighbourhood of x0 such that
A19:
N c= dom f
;
consider N2 being Neighbourhood of x0 such that
A20:
N2 c= N1
and
A21:
N2 c= N
by RCOMP_1:17;
A22:
N2 c= dom f
by A19, A21;
A23:
for x being Real st x in N2 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
thus (f `| Z) . x0 =
diff (f,x0)
by A15, A16, Def7
.=
L . j
by A18, A22, A23, Def5
.=
1
; verum