let Z be open Subset of REAL ; :: thesis: 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 ; :: thesis: ( 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 ) ) ) :: thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )

proof

assume A1: f is_differentiable_on Z ; :: thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) )
hence Z c= dom f by Def7; :: thesis: for x being Real st x in Z holds
f is_differentiable_in x
let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A2: x0 in Z ; :: thesis: f is_differentiable_in x0
then f | Z is_differentiable_in x0 by A1, Def7;
then consider N being Neighbourhood of x0 such that
A3: ( N c= dom (f | Z) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Def5;
take N ; :: according to FDIFF_1:def 5 :: thesis: ( N c= dom f & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
dom (f | Z) = (dom f) /\ Z by RELAT_1:90;
then dom (f | Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A3, XBOOLE_1:1; :: thesis: ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
consider L being LINEAR, R being REST such that
A4: for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
take L ; :: thesis: ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
take R ; :: thesis: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
let x be Real; :: thesis: ( x in N implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A5: x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;
then (f . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3, A5, FUNCT_1:70;
hence (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, FUNCT_1:72; :: thesis: verum

end;

assume A6: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) ; :: thesis: f is_differentiable_on Z
hence Z c= dom f ; :: according to FDIFF_1:def 7 :: thesis: for x being Real st x in Z holds
f | Z is_differentiable_in x
let x0 be Real; :: thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A7: x0 in Z ; :: thesis: f | Z is_differentiable_in x0
then f is_differentiable_in x0 by A6;
then consider N being Neighbourhood of x0 such that
A8: ( N c= dom f & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Def5;
consider N1 being Neighbourhood of x0 such that
A9: N1 c= Z by A7, RCOMP_1:39;
consider N2 being Neighbourhood of x0 such that
A10: ( N2 c= N1 & N2 c= N ) by RCOMP_1:38;
take N2 ; :: according to FDIFF_1:def 5 :: thesis: ( N2 c= dom (f | Z) & ex L being LINEAR ex R being REST st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
A11: N2 c= dom f by A8, A10, XBOOLE_1:1;
N2 c= Z by A9, A10, XBOOLE_1:1;
then N2 c= (dom f) /\ Z by A11, XBOOLE_1:19;
hence A12: N2 c= dom (f | Z) by RELAT_1:90; :: thesis: ex L being LINEAR ex R being REST 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 LINEAR, R being REST such that
A13: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A8;
take L ; :: thesis: ex R being REST st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
take R ; :: thesis: 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; :: thesis: ( x in N2 implies ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A14: x in N2 ; :: thesis: ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
then (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A13;
then A15: ((f | Z) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A12, A14, FUNCT_1:70;
x0 in N2 by RCOMP_1:37;
hence ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A12, A15, FUNCT_1:70; :: thesis: verum