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 `\ ['a,b']) . a = Rdiff (f,a) & (f `\ ['a,b']) . b = Ldiff (f,b) & ( for x being Real st x in ].a,b.[ holds
(f `\ ['a,b']) . x = diff (f,x) ) )
let a, b be Real; :: thesis: ( a <= b & f is_differentiable_on_interval ['a,b'] implies ( (f `\ ['a,b']) . a = Rdiff (f,a) & (f `\ ['a,b']) . b = Ldiff (f,b) & ( for x being Real st x in ].a,b.[ holds
(f `\ ['a,b']) . x = diff (f,x) ) ) )
assume that
A1: a <= b and
A2: f is_differentiable_on_interval ['a,b'] ; :: thesis: ( (f `\ ['a,b']) . a = Rdiff (f,a) & (f `\ ['a,b']) . b = Ldiff (f,b) & ( for x being Real st x in ].a,b.[ holds
(f `\ ['a,b']) . x = diff (f,x) ) )
A3: ( a = inf [.a,b.] & b = sup [.a,b.] ) by A1, XXREAL_2:25, XXREAL_2:29;
then reconsider I = [.a,b.] as non empty real-membered left_end right_end set by A1, XXREAL_1:1, XXREAL_2:def 5, XXREAL_2:def 6;
A4: I = ['a,b'] by A1, INTEGRA5:def 3;
A5: ( a in I & b in I ) by A1, XXREAL_1:1;
hence (f `\ ['a,b']) . a = Rdiff (f,a) by A3, A2, A4, Def2; :: thesis: ( (f `\ ['a,b']) . b = Ldiff (f,b) & ( for x being Real st x in ].a,b.[ holds
(f `\ ['a,b']) . x = diff (f,x) ) )
thus (f `\ ['a,b']) . b = Ldiff (f,b) by A2, A5, A4, A3, Def2; :: thesis: for x being Real st x in ].a,b.[ holds
(f `\ ['a,b']) . x = diff (f,x)
thus for x being Real st x in ].a,b.[ holds
(f `\ ['a,b']) . x = diff (f,x) :: thesis: verum

proof

let x be Real; :: thesis: ( x in ].a,b.[ implies (f `\ ['a,b']) . x = diff (f,x) )
assume A6: x in ].a,b.[ ; :: thesis: (f `\ ['a,b']) . x = diff (f,x)
then A7: ( x <> a & x <> b ) by XXREAL_1:4;
].a,b.[ c= [.a,b.] by XXREAL_1:37;
hence (f `\ ['a,b']) . x = diff (f,x) by A2, A3, A7, A4, A6, Def2; :: thesis: verum

end;