let F be non trivial RealNormSpace; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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 Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of F 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, the carrier of F; :: 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 A2: Z c= dom f by Def5; :: 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 A3: x0 in Z ; :: thesis: f is_differentiable_in x0
then f | Z is_differentiable_in x0 by A1, Def5;
then consider N being Neighbourhood of x0 such that
A4: N c= dom (f | Z) and
A5: ex L being LINEAR of F ex R being REST of F st
for x being Real st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
take N ; :: according to NDIFF_3:def 3 :: thesis: ( N c= dom f & ex L being LINEAR of F ex R being REST of F 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:61;
then dom (f | Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A4, XBOOLE_1:1; :: thesis: ex L being LINEAR of F ex R being REST of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
consider L being LINEAR of F, R being REST of F such that
A6: for x being Real st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5;

now

let x be Real; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A7: x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then A8: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6;
(f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8, A4, A7, PARTFUN2:15;
hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, A3, PARTFUN2:17; :: thesis: verum

end;

hence ex L being LINEAR of F ex R being REST of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; :: thesis: verum

end;

assume that
A9: Z c= dom f and
A10: for x being Real st x in Z holds
f is_differentiable_in x ; :: thesis: f is_differentiable_on Z
thus Z c= dom f by A9; :: according to NDIFF_3:def 5 :: 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 A11: x0 in Z ; :: thesis: f | Z is_differentiable_in x0
then consider N1 being Neighbourhood of x0 such that
A12: N1 c= Z by RCOMP_1:18;
f is_differentiable_in x0 by A10, A11;
then consider N being Neighbourhood of x0 such that
A13: N c= dom f and
A14: ex L being LINEAR of F ex R being REST of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def3;
consider N2 being Neighbourhood of x0 such that
A15: N2 c= N1 and
A16: N2 c= N by RCOMP_1:17;
A17: N2 c= Z by A12, A15, XBOOLE_1:1;
take N2 ; :: according to NDIFF_3:def 3 :: thesis: ( N2 c= dom (f | Z) & ex L being LINEAR of F ex R being REST of F 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 A13, A16, XBOOLE_1:1;
then N2 c= (dom f) /\ Z by A17, XBOOLE_1:19;
hence A18: N2 c= dom (f | Z) by RELAT_1:61; :: thesis: ex L being LINEAR of F ex R being REST of F 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 of F, R being REST of F such that
A19: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A14;
A20: x0 in N2 by RCOMP_1:16;
take L ; :: thesis: ex R being REST of F 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))

now

let x be Real; :: thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A21: 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 A16, A19;
then ((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A21, A18, PARTFUN2:15;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A20, A18, PARTFUN2:15; :: thesis: verum

end;

hence for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; :: thesis: verum