let X be set ; :: thesis: for S, T being RealNormSpace

for f being PartFunc of S,T

for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

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

for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

let f be PartFunc of S,T; :: thesis: for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

let Z be Subset of S; :: thesis: ( Z is open & f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )

assume A1: Z is open ; :: thesis: ( not f is_differentiable_on X or not Z c= X or f is_differentiable_on Z )

assume that

A2: f is_differentiable_on X and

A3: Z c= X ; :: thesis: f is_differentiable_on Z

X c= dom f by A2;

hence A4: Z c= dom f by A3; :: 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 A5: x0 in Z ; :: thesis: f | Z is_differentiable_in x0

then consider N1 being Neighbourhood of x0 such that

A6: N1 c= Z by A1, Th2;

f | X is_differentiable_in x0 by A2, A3, A5;

then consider N being Neighbourhood of x0 such that

A7: N c= dom (f | X) and

A8: 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) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ;

consider N2 being Neighbourhood of x0 such that

A9: N2 c= N and

A10: N2 c= N1 by Th1;

A11: N2 c= Z by A6, A10;

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)) )

dom (f | X) = (dom f) /\ X by RELAT_1:61;

then dom (f | X) c= dom f by XBOOLE_1:17;

then N c= dom f by A7;

then N2 c= dom f by A9;

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

hence A12: 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))

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

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

((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8;

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 A14: x in N2 ; :: thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))

then ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A9, A13;

then A15: ((f | X) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, A5, PARTFUN2:17;

x in N by A9, A14;

then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A7, A15, PARTFUN2:15;

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

hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A12, A14, PARTFUN2:15; :: thesis: verum

for f being PartFunc of S,T

for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

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

for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

let f be PartFunc of S,T; :: thesis: for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

let Z be Subset of S; :: thesis: ( Z is open & f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )

assume A1: Z is open ; :: thesis: ( not f is_differentiable_on X or not Z c= X or f is_differentiable_on Z )

assume that

A2: f is_differentiable_on X and

A3: Z c= X ; :: thesis: f is_differentiable_on Z

X c= dom f by A2;

hence A4: Z c= dom f by A3; :: 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 A5: x0 in Z ; :: thesis: f | Z is_differentiable_in x0

then consider N1 being Neighbourhood of x0 such that

A6: N1 c= Z by A1, Th2;

f | X is_differentiable_in x0 by A2, A3, A5;

then consider N being Neighbourhood of x0 such that

A7: N c= dom (f | X) and

A8: 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) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ;

consider N2 being Neighbourhood of x0 such that

A9: N2 c= N and

A10: N2 c= N1 by Th1;

A11: N2 c= Z by A6, A10;

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)) )

dom (f | X) = (dom f) /\ X by RELAT_1:61;

then dom (f | X) c= dom f by XBOOLE_1:17;

then N c= dom f by A7;

then N2 c= dom f by A9;

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

hence A12: 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))

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

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

((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8;

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 A14: x in N2 ; :: thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))

then ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A9, A13;

then A15: ((f | X) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, A5, PARTFUN2:17;

x in N by A9, A14;

then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A7, A15, PARTFUN2:15;

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

hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A12, A14, PARTFUN2:15; :: thesis: verum