let f be PartFunc of REAL,REAL; :: thesis: for I being open Subset of REAL
for X being Subset of REAL st I c= X holds
( f is_differentiable_on I iff f | X is_differentiable_on I )
let I be open Subset of REAL; :: thesis: for X being Subset of REAL st I c= X holds
( f is_differentiable_on I iff f | X is_differentiable_on I )
let X be Subset of REAL; :: thesis: ( I c= X implies ( f is_differentiable_on I iff f | X is_differentiable_on I ) )
assume A1: I c= X ; :: thesis: ( f is_differentiable_on I iff f | X is_differentiable_on I )
A2: dom (f | X) = (dom f) /\ X by RELAT_1:61;

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

assume A3: f is_differentiable_on I ; :: thesis: f | X is_differentiable_on I

now :: thesis: for x being Real st x in I holds
(f | X) | I is_differentiable_in x

let x be Real; :: thesis: ( x in I implies (f | X) | I is_differentiable_in x )
assume x in I ; :: thesis: (f | X) | I is_differentiable_in x
then f | I is_differentiable_in x by A3;
hence (f | X) | I is_differentiable_in x by A1, RELAT_1:74; :: thesis: verum

end;

hence f | X is_differentiable_on I by A1, A3, A2, XBOOLE_1:19; :: thesis: verum

end;

assume A4: f | X is_differentiable_on I ; :: thesis: f is_differentiable_on I

now :: thesis: for x being Real st x in I holds
f | I is_differentiable_in x

let x be Real; :: thesis: ( x in I implies f | I is_differentiable_in x )
assume x in I ; :: thesis: f | I is_differentiable_in x
then (f | X) | I is_differentiable_in x by A4;
hence f | I is_differentiable_in x by A1, RELAT_1:74; :: thesis: verum

end;

hence f is_differentiable_on I by A4, A2, XBOOLE_1:18; :: thesis: verum