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 )

A7: Z c= dom f and

A8: 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 A7; :: according to FDIFF_1:def 6 :: 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 A9: x0 in Z ; :: thesis: 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 ; :: according to FDIFF_1:def 4 :: thesis: ( 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; :: thesis: 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 ; :: thesis: 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 ; :: 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 A19: 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 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; :: thesis: verum

( 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 that
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 ; :: 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;

then consider N being Neighbourhood of x0 such that

A3: N c= dom (f | Z) and

A4: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) ;

take N ; :: according to FDIFF_1:def 4 :: thesis: ( 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)) )

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 A3; :: thesis: 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 L being LinearFunc, R being RestFunc such that

A5: for x being Real st x in N holds

((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;

take L ; :: thesis: ex R being RestFunc 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 A6: 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 A5;

then (f . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3, A6, FUNCT_1:47;

hence (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, FUNCT_1:49; :: thesis: verum

end;f is_differentiable_in x ) )

hence Z c= dom f ; :: 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;

then consider N being Neighbourhood of x0 such that

A3: N c= dom (f | Z) and

A4: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) ;

take N ; :: according to FDIFF_1:def 4 :: thesis: ( 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)) )

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 A3; :: thesis: 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 L being LinearFunc, R being RestFunc such that

A5: for x being Real st x in N holds

((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;

take L ; :: thesis: ex R being RestFunc 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 A6: 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 A5;

then (f . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3, A6, FUNCT_1:47;

hence (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, FUNCT_1:49; :: thesis: verum

A7: Z c= dom f and

A8: 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 A7; :: according to FDIFF_1:def 6 :: 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 A9: x0 in Z ; :: thesis: 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 ; :: according to FDIFF_1:def 4 :: thesis: ( 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; :: thesis: 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 ; :: thesis: 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 ; :: 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 A19: 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 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; :: thesis: verum