let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T

for Z being Subset of S st Z is open holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

let f be PartFunc of S,T; :: thesis: for Z being Subset of S st Z is open holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

let Z be Subset of S; :: thesis: ( Z is open implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) ) )

assume A1: Z is open ; :: thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) ) :: thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) implies f is_differentiable_on Z )

A10: Z c= dom f and

A11: for x being Point of S st x in Z holds

f is_differentiable_in x ; :: thesis: f is_differentiable_on Z

thus Z c= dom f by A10; :: according to NDIFF_1:def 8 :: thesis: for x being Point of S st x in Z holds

f | Z is_differentiable_in x

let x0 be Point of S; :: thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )

assume A12: x0 in Z ; :: thesis: f | Z is_differentiable_in x0

then consider N1 being Neighbourhood of x0 such that

A13: N1 c= Z by A1, Th2;

f is_differentiable_in x0 by A11, A12;

then consider N being Neighbourhood of x0 such that

A14: N c= dom f and

A15: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

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

consider N2 being Neighbourhood of x0 such that

A16: N2 c= N1 and

A17: N2 c= N by Th1;

A18: N2 c= Z by A13, A16;

take N2 ; :: according to NDIFF_1:def 6 :: thesis: ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N2 holds

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

N2 c= dom f by A14, A17;

then A19: N2 c= (dom f) /\ Z by A18, XBOOLE_1:19;

hence N2 c= dom (f | Z) by RELAT_1:61; :: thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N2 holds

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

A20: x0 in N2 by NFCONT_1:4;

consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that

A21: for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A15;

take L ; :: thesis: ex R being RestFunc of S,T st

for x being Point of S st x in N2 holds

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

take R ; :: thesis: for x being Point of S st x in N2 holds

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

let x be Point of S; :: thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )

assume A22: 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 A17, A21;

then ((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A22, PARTFUN2:16;

hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A20, PARTFUN2:16; :: thesis: verum

for Z being Subset of S st Z is open holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

let f be PartFunc of S,T; :: thesis: for Z being Subset of S st Z is open holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

let Z be Subset of S; :: thesis: ( Z is open implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) ) )

assume A1: Z is open ; :: thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) ) :: thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) implies f is_differentiable_on Z )

proof

assume that
assume A2:
f is_differentiable_on Z
; :: thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) )

hence A3: Z c= dom f ; :: thesis: for x being Point of S st x in Z holds

f is_differentiable_in x

let x0 be Point of S; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )

assume A4: x0 in Z ; :: thesis: f is_differentiable_in x0

then f | Z is_differentiable_in x0 by A2;

then consider N being Neighbourhood of x0 such that

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

A6: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

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

consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that

A7: for x being Point of S st x in N holds

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

take N ; :: according to NDIFF_1:def 6 :: thesis: ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )

A8: 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 A5; :: thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

take L ; :: thesis: ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

take R ; :: thesis: for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

let x be Point of S; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )

assume A9: 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 A7;

then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5, A8, A9, PARTFUN2:16;

hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, PARTFUN2:17; :: thesis: verum

end;f is_differentiable_in x ) )

hence A3: Z c= dom f ; :: thesis: for x being Point of S st x in Z holds

f is_differentiable_in x

let x0 be Point of S; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )

assume A4: x0 in Z ; :: thesis: f is_differentiable_in x0

then f | Z is_differentiable_in x0 by A2;

then consider N being Neighbourhood of x0 such that

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

A6: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

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

consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that

A7: for x being Point of S st x in N holds

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

take N ; :: according to NDIFF_1:def 6 :: thesis: ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )

A8: 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 A5; :: thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

take L ; :: thesis: ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

take R ; :: thesis: for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

let x be Point of S; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )

assume A9: 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 A7;

then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5, A8, A9, PARTFUN2:16;

hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, PARTFUN2:17; :: thesis: verum

A10: Z c= dom f and

A11: for x being Point of S st x in Z holds

f is_differentiable_in x ; :: thesis: f is_differentiable_on Z

thus Z c= dom f by A10; :: according to NDIFF_1:def 8 :: thesis: for x being Point of S st x in Z holds

f | Z is_differentiable_in x

let x0 be Point of S; :: thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )

assume A12: x0 in Z ; :: thesis: f | Z is_differentiable_in x0

then consider N1 being Neighbourhood of x0 such that

A13: N1 c= Z by A1, Th2;

f is_differentiable_in x0 by A11, A12;

then consider N being Neighbourhood of x0 such that

A14: N c= dom f and

A15: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

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

consider N2 being Neighbourhood of x0 such that

A16: N2 c= N1 and

A17: N2 c= N by Th1;

A18: N2 c= Z by A13, A16;

take N2 ; :: according to NDIFF_1:def 6 :: thesis: ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N2 holds

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

N2 c= dom f by A14, A17;

then A19: N2 c= (dom f) /\ Z by A18, XBOOLE_1:19;

hence N2 c= dom (f | Z) by RELAT_1:61; :: thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N2 holds

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

A20: x0 in N2 by NFCONT_1:4;

consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that

A21: for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A15;

take L ; :: thesis: ex R being RestFunc of S,T st

for x being Point of S st x in N2 holds

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

take R ; :: thesis: for x being Point of S st x in N2 holds

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

let x be Point of S; :: thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )

assume A22: 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 A17, A21;

then ((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A22, PARTFUN2:16;

hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A20, PARTFUN2:16; :: thesis: verum