let f be PartFunc of REAL,REAL; :: thesis: for a being Real
for I being non empty Interval st f is_differentiable_on_interval I & a in I holds
integral ((f `\ I),a,a) = 0
let a be Real; :: thesis: for I being non empty Interval st f is_differentiable_on_interval I & a in I holds
integral ((f `\ I),a,a) = 0
let I be non empty Interval; :: thesis: ( f is_differentiable_on_interval I & a in I implies integral ((f `\ I),a,a) = 0 )
assume that
A1: f is_differentiable_on_interval I and
A2: a in I ; :: thesis: integral ((f `\ I),a,a) = 0
A3: dom (f `\ I) = I by A1, FDIFF_12:def 2;
A4: ['a,a'] = [.a,a.] by INTEGRA5:def 3;
then A5: ['a,a'] c= dom (f `\ I) by A3, A2, Th3;
for x being Real st x in ['a,a'] holds
(f `\ I) . x = (f `\ I) . a

proof

let x be Real; :: thesis: ( x in ['a,a'] implies (f `\ I) . x = (f `\ I) . a )
assume x in ['a,a'] ; :: thesis: (f `\ I) . x = (f `\ I) . a
then ( a <= x & x <= a ) by A4, XXREAL_1:1;
hence (f `\ I) . x = (f `\ I) . a by XXREAL_0:1; :: thesis: verum

end;

then integral ((f `\ I),a,a) = ((f `\ I) . a) * (a - a) by A5, INTEGRA6:26;
hence integral ((f `\ I),a,a) = 0 ; :: thesis: verum