theorem :: FDIFF_12:8

for f being PartFunc of REAL,REAL
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) ) )