let f be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st I is open_interval holds
( f is_differentiable_on I iff f is_differentiable_on_interval I )
let I be non empty Interval; :: thesis: ( I is open_interval implies ( f is_differentiable_on I iff f is_differentiable_on_interval I ) )
assume I is open_interval ; :: thesis: ( f is_differentiable_on I iff f is_differentiable_on_interval I )
then consider a, b being R_eal such that
A1: I = ].a,b.[ by MEASURE5:def 2;
A2: ( a = inf I & b = sup I ) by A1, XXREAL_1:28, XXREAL_2:28, XXREAL_2:32;
hence ( f is_differentiable_on I implies f is_differentiable_on_interval I ) by A1, XXREAL_1:4, XXREAL_1:28; :: thesis: ( f is_differentiable_on_interval I implies f is_differentiable_on I )
assume f is_differentiable_on_interval I ; :: thesis: f is_differentiable_on I
hence f is_differentiable_on I by A1, A2; :: thesis: verum