let F be RealNormSpace; :: thesis: for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let X be set ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of REAL, the carrier of F; :: thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )
assume that
A1: f is_differentiable_on X and
A2: Z c= X ; :: thesis: f is_differentiable_on Z
X c= dom f by A1;
then A3: Z c= dom f by A2;

now :: thesis: for x0 being Real st x0 in Z holds
f | Z is_differentiable_in x0

let x0 be Real; :: thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A4: x0 in Z ; :: thesis: f | Z is_differentiable_in x0
then f | X is_differentiable_in x0 by A1, A2;
then consider N being Neighbourhood of x0 such that
A5: N c= dom (f | X) and
A6: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
consider N1 being Neighbourhood of x0 such that
A7: N1 c= Z by A4, RCOMP_1:18;
consider N2 being Neighbourhood of x0 such that
A8: N2 c= N and
A9: N2 c= N1 by RCOMP_1:17;
A10: N2 c= Z by A7, A9;
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 A5;
then N2 c= dom f by A8;
then N2 c= (dom f) /\ Z by A10, XBOOLE_1:19;
then A11: N2 c= dom (f | Z) by RELAT_1:61;
A12: N2 c= dom (f | X) by A8, A5;
consider L being LinearFunc of F, R being RestFunc of F such that
A13: for x being Real st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A6;
for x being Real st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))

proof

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 A15: ((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A8, A13;
A16: x0 in N2 by RCOMP_1:16;
((f | X) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A15, A16, A12, PARTFUN2:15;
then (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A14, A12, PARTFUN2:15;
then (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A16, A11, PARTFUN2:15;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A14, A11, PARTFUN2:15; :: thesis: verum

end;

hence f | Z is_differentiable_in x0 by A11; :: thesis: verum

end;

hence f is_differentiable_on Z by A3; :: thesis: verum