let f be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval
for X being Subset of REAL st I c= X holds
( f is_differentiable_on_interval I iff f | X is_differentiable_on_interval I )
let I be non empty Interval; :: thesis: for X being Subset of REAL st I c= X holds
( f is_differentiable_on_interval I iff f | X is_differentiable_on_interval I )
let X be Subset of REAL; :: thesis: ( I c= X implies ( f is_differentiable_on_interval I iff f | X is_differentiable_on_interval I ) )
assume A1: I c= X ; :: thesis: ( f is_differentiable_on_interval I iff f | X is_differentiable_on_interval I )
reconsider J = ].(inf I),(sup I).[ as open Subset of REAL by FDIFF_12:2;
J c= I by FDIFF_12:2;
then A2: J c= X by A1;

hereby :: thesis: ( f | X is_differentiable_on_interval I implies f is_differentiable_on_interval I )

assume f is_differentiable_on_interval I ; :: thesis: f | X is_differentiable_on_interval I
then A3: ( I c= dom f & inf I < sup I & ( inf I in I implies f is_right_differentiable_in lower_bound I ) & ( sup I in I implies f is_left_differentiable_in upper_bound I ) & f is_differentiable_on ].(inf I),(sup I).[ ) by FDIFF_12:def 1;
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A4: I c= dom (f | X) by A1, A3, XBOOLE_1:19;

A5: now :: thesis: ( inf I in I implies f | X is_right_differentiable_in lower_bound I )

assume A6: inf I in I ; :: thesis: f | X is_right_differentiable_in lower_bound I
then inf I = lower_bound I by Th1;
hence f | X is_right_differentiable_in lower_bound I by A1, A6, A3, Th12; :: thesis: verum

end;

A7: now :: thesis: ( sup I in I implies f | X is_left_differentiable_in upper_bound I )

assume A8: sup I in I ; :: thesis: f | X is_left_differentiable_in upper_bound I
then sup I = upper_bound I by Th2;
hence f | X is_left_differentiable_in upper_bound I by A1, A8, A3, Th13; :: thesis: verum

end;

f | X is_differentiable_on J by A3, A2, Th14;
hence f | X is_differentiable_on_interval I by A3, A4, A5, A7, FDIFF_12:def 1; :: thesis: verum

end;

assume f | X is_differentiable_on_interval I ; :: thesis: f is_differentiable_on_interval I
then A9: ( I c= dom (f | X) & inf I < sup I & ( inf I in I implies f | X is_right_differentiable_in lower_bound I ) & ( sup I in I implies f | X is_left_differentiable_in upper_bound I ) & f | X is_differentiable_on ].(inf I),(sup I).[ ) by FDIFF_12:def 1;
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A10: ( I c= dom f & I c= X ) by A9, XBOOLE_1:18;

A11: now :: thesis: ( inf I in I implies f is_right_differentiable_in lower_bound I )

assume A12: inf I in I ; :: thesis: f is_right_differentiable_in lower_bound I
then inf I = lower_bound I by Th1;
hence f is_right_differentiable_in lower_bound I by A9, A10, A12, Th12; :: thesis: verum

end;

A13: now :: thesis: ( sup I in I implies f is_left_differentiable_in upper_bound I )

assume A14: sup I in I ; :: thesis: f is_left_differentiable_in upper_bound I
then sup I = upper_bound I by Th2;
hence f is_left_differentiable_in upper_bound I by A9, A10, A14, Th13; :: thesis: verum

end;

f is_differentiable_on ].(inf I),(sup I).[ by A9, A2, Th14;
hence f is_differentiable_on_interval I by A9, A10, A11, A13, FDIFF_12:def 1; :: thesis: verum