let Z be open Subset of REAL; for f being PartFunc of REAL,REAL holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
let f be PartFunc of REAL,REAL; ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
thus
( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )
assume that
A7:
Z c= dom f
and
A8:
for x being Real st x in Z holds
f is_differentiable_in x
; f is_differentiable_on Z
thus
Z c= dom f
by A7; FDIFF_1:def 6 for x being Real st x in Z holds
f | Z is_differentiable_in x
let x0 be Real; ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A9:
x0 in Z
; f | Z is_differentiable_in x0
then consider N1 being Neighbourhood of x0 such that
A10:
N1 c= Z
by RCOMP_1:18;
f is_differentiable_in x0
by A8, A9;
then consider N being Neighbourhood of x0 such that
A11:
N c= dom f
and
A12:
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))
;
consider N2 being Neighbourhood of x0 such that
A13:
N2 c= N1
and
A14:
N2 c= N
by RCOMP_1:17;
A15:
N2 c= Z
by A10, A13;
take
N2
; FDIFF_1:def 4 ( N2 c= dom (f | Z) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
N2 c= dom f
by A11, A14;
then
N2 c= (dom f) /\ Z
by A15, XBOOLE_1:19;
hence A16:
N2 c= dom (f | Z)
by RELAT_1:61; ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
consider L being LinearFunc, R being RestFunc such that
A17:
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A12;
A18:
x0 in N2
by RCOMP_1:16;
take
L
; ex R being RestFunc st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
take
R
; for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
let x be Real; ( x in N2 implies ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A19:
x in N2
; ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
then
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A14, A17;
then
((f | Z) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A16, A19, FUNCT_1:47;
hence
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
by A16, A18, FUNCT_1:47; verum