let X be set ; :: thesis: for Z being open Subset of REAL

for f being PartFunc of REAL,REAL 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,REAL st f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

let f be PartFunc of REAL,REAL; :: 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;

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

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

A5: ex L being LinearFunc ex R being RestFunc 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

A6: N1 c= Z by A3, RCOMP_1:18;

consider N2 being Neighbourhood of x0 such that

A7: N2 c= N and

A8: N2 c= N1 by RCOMP_1:17;

A9: N2 c= Z by A6, A8;

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

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 A4;

then N2 c= dom f by A7;

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

hence A10: 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

A11: for x being Real st x in N holds

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

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 A12: 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 A7, A11;

then A13: ((f | X) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, A3, FUNCT_1:49;

x in N by A7, A12;

then (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A4, A13, FUNCT_1:47;

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

hence ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A12, FUNCT_1:47; :: thesis: verum

for f being PartFunc of REAL,REAL 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,REAL st f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

let f be PartFunc of REAL,REAL; :: 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;

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

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

A5: ex L being LinearFunc ex R being RestFunc 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

A6: N1 c= Z by A3, RCOMP_1:18;

consider N2 being Neighbourhood of x0 such that

A7: N2 c= N and

A8: N2 c= N1 by RCOMP_1:17;

A9: N2 c= Z by A6, A8;

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

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 A4;

then N2 c= dom f by A7;

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

hence A10: 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

A11: for x being Real st x in N holds

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

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 A12: 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 A7, A11;

then A13: ((f | X) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, A3, FUNCT_1:49;

x in N by A7, A12;

then (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A4, A13, FUNCT_1:47;

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

hence ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A12, FUNCT_1:47; :: thesis: verum