let f be PartFunc of REAL,REAL; :: thesis: for I, J being non empty Interval st f is_differentiable_on_interval I & J c= I & inf J < sup J holds
( f is_differentiable_on_interval J & ( for x being Real st x in J holds
(f `\ I) . x = (f `\ J) . x ) )
let I, J be non empty Interval; :: thesis: ( f is_differentiable_on_interval I & J c= I & inf J < sup J implies ( f is_differentiable_on_interval J & ( for x being Real st x in J holds
(f `\ I) . x = (f `\ J) . x ) ) )
assume that
A1: f is_differentiable_on_interval I and
A2: J c= I and
A3: inf J < sup J ; :: thesis: ( f is_differentiable_on_interval J & ( for x being Real st x in J holds
(f `\ I) . x = (f `\ J) . x ) )
I c= dom f by A1;
then A4: J c= dom f by A2;
A5: ( inf I <= inf J & sup J <= sup I ) by A2, XXREAL_2:59, XXREAL_2:60;
for x being Real st x in J holds
( ( x = inf J implies f | J is_right_differentiable_in x ) & ( x = sup J implies f | J is_left_differentiable_in x ) & ( x in ].(inf J),(sup J).[ implies f is_differentiable_in x ) )

proof

let x be Real; :: thesis: ( x in J implies ( ( x = inf J implies f | J is_right_differentiable_in x ) & ( x = sup J implies f | J is_left_differentiable_in x ) & ( x in ].(inf J),(sup J).[ implies f is_differentiable_in x ) ) )
assume A6: x in J ; :: thesis: ( ( x = inf J implies f | J is_right_differentiable_in x ) & ( x = sup J implies f | J is_left_differentiable_in x ) & ( x in ].(inf J),(sup J).[ implies f is_differentiable_in x ) )

hereby :: thesis: ( ( x = sup J implies f | J is_left_differentiable_in x ) & ( x in ].(inf J),(sup J).[ implies f is_differentiable_in x ) )

assume A7: x = inf J ; :: thesis: f | J is_right_differentiable_in x

per cases ( x = inf I or x <> inf I ) ;

suppose x = inf I ; :: thesis: f | J is_right_differentiable_in x

then f | I is_right_differentiable_in x by A1, A2, A6, Th11;
then (f | I) | J is_right_differentiable_in x by A6, A7, A3, Th4;
hence f | J is_right_differentiable_in x by A2, RELAT_1:74; :: thesis: verum

end;

suppose x <> inf I ; :: thesis: f | J is_right_differentiable_in x

then x in ].(inf I),(sup I).[ by A2, A7, A6, A5, A3, Th3;
then f is_differentiable_in x by A1, A2, A6, Th11;
then f is_right_differentiable_in x by FDIFF_3:22;
hence f | J is_right_differentiable_in x by A6, A7, A3, Th4; :: thesis: verum

end;

end;

end;

hereby :: thesis: ( x in ].(inf J),(sup J).[ implies f is_differentiable_in x )

assume A8: x = sup J ; :: thesis: f | J is_left_differentiable_in x

per cases ( x = sup I or x <> sup I ) ;

suppose x = sup I ; :: thesis: f | J is_left_differentiable_in x

then f | I is_left_differentiable_in x by A1, A2, A6, Th11;
then (f | I) | J is_left_differentiable_in x by A6, A8, A3, Th5;
hence f | J is_left_differentiable_in x by A2, RELAT_1:74; :: thesis: verum

end;

suppose x <> sup I ; :: thesis: f | J is_left_differentiable_in x

then x in ].(inf I),(sup I).[ by A3, A5, A2, A8, A6, Th3;
then f is_differentiable_in x by A1, A2, A6, Th11;
then f is_left_differentiable_in x by FDIFF_3:22;
hence f | J is_left_differentiable_in x by A6, A8, A3, Th5; :: thesis: verum

end;

end;

end;

hereby :: thesis: verum

assume x in ].(inf J),(sup J).[ ; :: thesis: f is_differentiable_in x
then ( inf J < x & x < sup J ) by XXREAL_1:4;
then ( inf I < x & x < sup I ) by A5, XXREAL_0:2;
then x in ].(inf I),(sup I).[ by XXREAL_1:4;
hence f is_differentiable_in x by A1, A2, A6, Th11; :: thesis: verum

end;

end;

hence A9: f is_differentiable_on_interval J by A4, Th11; :: thesis: for x being Real st x in J holds
(f `\ I) . x = (f `\ J) . x
thus for x being Real st x in J holds
(f `\ I) . x = (f `\ J) . x :: thesis: verum

proof

let x be Real; :: thesis: ( x in J implies (f `\ I) . x = (f `\ J) . x )
assume A10: x in J ; :: thesis: (f `\ I) . x = (f `\ J) . x
then A11: ( inf J <= x & x <= sup J ) by XXREAL_2:3, XXREAL_2:4;

per cases ( x = inf J or x = sup J or ( x <> inf J & x <> sup J ) ) ;

suppose A12: x = inf J ; :: thesis: (f `\ I) . x = (f `\ J) . x

per cases ( x = inf I or x <> inf I ) ;

suppose x = inf I ; :: thesis: (f `\ I) . x = (f `\ J) . x

then ( (f `\ I) . x = Rdiff (f,x) & (f `\ J) . x = Rdiff (f,x) ) by A1, A2, A10, A9, A12, Def2;
hence (f `\ I) . x = (f `\ J) . x ; :: thesis: verum

end;

suppose A13: x <> inf I ; :: thesis: (f `\ I) . x = (f `\ J) . x

then x in ].(inf I),(sup I).[ by A2, A10, A12, A3, A5, Th3;
then f is_differentiable_in x by A1, A2, A10, Th11;
then diff (f,x) = Rdiff (f,x) by FDIFF_3:22;
then ( (f `\ I) . x = Rdiff (f,x) & (f `\ J) . x = Rdiff (f,x) ) by A1, A2, A10, A9, A12, A13, Def2, A5;
hence (f `\ I) . x = (f `\ J) . x ; :: thesis: verum

end;

end;

end;

suppose A14: x = sup J ; :: thesis: (f `\ I) . x = (f `\ J) . x

per cases ( x = sup I or x <> sup I ) ;

suppose x = sup I ; :: thesis: (f `\ I) . x = (f `\ J) . x

then ( (f `\ I) . x = Ldiff (f,x) & (f `\ J) . x = Ldiff (f,x) ) by A1, A2, A9, A10, A14, Def2;
hence (f `\ I) . x = (f `\ J) . x ; :: thesis: verum

end;

suppose A15: x <> sup I ; :: thesis: (f `\ I) . x = (f `\ J) . x

then x in ].(inf I),(sup I).[ by A2, A10, A14, A3, A5, Th3;
then f is_differentiable_in x by A1, A2, A10, Th11;
then diff (f,x) = Ldiff (f,x) by FDIFF_3:22;
then ( (f `\ I) . x = Ldiff (f,x) & (f `\ J) . x = Ldiff (f,x) ) by A1, A2, A10, A9, A14, A15, Def2, A5;
hence (f `\ I) . x = (f `\ J) . x ; :: thesis: verum

end;

end;

end;

suppose ( x <> inf J & x <> sup J ) ; :: thesis: (f `\ I) . x = (f `\ J) . x

then ( inf J < x & x < sup J ) by A11, XXREAL_0:1;
then ( (f `\ I) . x = diff (f,x) & (f `\ J) . x = diff (f,x) ) by A1, A2, A10, A9, Def2, A5;
hence (f `\ I) . x = (f `\ J) . x ; :: thesis: verum

end;

end;

end;