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

proof

let x be Real; :: thesis: ( x in I implies ( ( x = inf I implies f | I is_right_differentiable_in x ) & ( x = sup I implies f | I is_left_differentiable_in x ) & ( x in ].(inf I),(sup I).[ implies f is_differentiable_in x ) ) )
assume A5: x in I ; :: thesis: ( ( x = inf I implies f | I is_right_differentiable_in x ) & ( x = sup I implies f | I is_left_differentiable_in x ) & ( x in ].(inf I),(sup I).[ implies f is_differentiable_in x ) )
then f is_differentiable_in x by A1, A3, FDIFF_1:9;
then A6: ( f is_right_differentiable_in x & f is_left_differentiable_in x ) by FDIFF_3:22;
hence ( x = inf I implies f | I is_right_differentiable_in x ) by A5, A2, Th4; :: thesis: ( ( x = sup I implies f | I is_left_differentiable_in x ) & ( x in ].(inf I),(sup I).[ implies f is_differentiable_in x ) )
thus ( x = sup I implies f | I is_left_differentiable_in x ) by A5, A6, A2, Th5; :: thesis: ( x in ].(inf I),(sup I).[ implies f is_differentiable_in x )
assume x in ].(inf I),(sup I).[ ; :: thesis: f is_differentiable_in x
thus f is_differentiable_in x by A5, A1, A3, FDIFF_1:9; :: thesis: verum

end;

hence f is_differentiable_on_interval I by A4, Th11; :: thesis: verum