let f be PartFunc of REAL,REAL; :: thesis: for A, B, C being non empty closed_interval Subset of REAL
for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds
( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )

let A, B, C be non empty closed_interval Subset of REAL; :: thesis: for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds
( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )

let X be set ; :: thesis: ( A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A implies ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) )
assume that
A1: ( A c= X & f is_differentiable_on X ) and
A2: (f `| X) | A is continuous and
A3: lower_bound A = lower_bound B and
A4: upper_bound B = lower_bound C and
A5: upper_bound C = upper_bound A ; :: thesis: ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
consider x being Element of REAL such that
A6: x in B by SUBSET_1:4;
( lower_bound B <= x & x <= upper_bound B ) by ;
then A7: lower_bound B <= upper_bound B by XXREAL_0:2;
consider x being Element of REAL such that
A8: x in C by SUBSET_1:4;
( lower_bound C <= x & x <= upper_bound C ) by ;
then A9: lower_bound C <= upper_bound C by XXREAL_0:2;
for x being object st x in B holds
x in A
proof
let x be object ; :: thesis: ( x in B implies x in A )
assume A10: x in B ; :: thesis: x in A
then reconsider x = x as Real ;
x <= upper_bound B by ;
then A11: x <= upper_bound A by ;
lower_bound A <= x by ;
hence x in A by ; :: thesis: verum
end;
hence A12: B c= A by TARSKI:def 3; :: thesis: ( C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
A13: A c= dom (f `| X) by ;
then A14: (f `| X) | A is bounded by ;
then A15: (f `| X) | B is bounded by ;
for x being object st x in C holds
x in A
proof
let x be object ; :: thesis: ( x in C implies x in A )
assume A16: x in C ; :: thesis: x in A
then reconsider x = x as Real ;
lower_bound C <= x by ;
then A17: lower_bound A <= x by ;
x <= upper_bound A by ;
hence x in A by ; :: thesis: verum
end;
hence A18: C c= A by TARSKI:def 3; :: thesis: integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C))
then A19: (f `| X) | C is bounded by ;
(f `| X) | C is continuous by ;
then f `| X is_integrable_on C by ;
then A20: integral ((f `| X),C) = (f . ()) - (f . ()) by ;
(f `| X) | B is continuous by ;
then f `| X is_integrable_on B by ;
then A21: integral ((f `| X),B) = (f . ()) - (f . ()) by ;
f `| X is_integrable_on A by ;
then integral ((f `| X),A) = (f . ()) - (f . ()) by A1, A2, A13, Th10, Th13;
hence integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) by A3, A4, A5, A21, A20; :: thesis: verum