let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & f is_differentiable_on_interval ['a,b'] holds
f is_differentiable_on ].a,b.[
let a, b be Real; :: thesis: ( a < b & f is_differentiable_on_interval ['a,b'] implies f is_differentiable_on ].a,b.[ )
assume that
A1: a < b and
A2: f is_differentiable_on_interval ['a,b'] ; :: thesis: f is_differentiable_on ].a,b.[
A3: [.a,b.] = ['a,b'] by A1, INTEGRA5:def 3;
( a = inf [.a,b.] & b = sup [.a,b.] ) by A1, XXREAL_2:25, XXREAL_2:29;
hence f is_differentiable_on ].a,b.[ by A2, A3; :: thesis: verum