let f be PartFunc of REAL ,REAL ; :: thesis: for A, B, C being closed-interval Subset of REAL
for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & inf A = inf B & sup B = inf C & sup C = sup 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 closed-interval Subset of REAL ; :: thesis: for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & inf A = inf B & sup B = inf C & sup C = sup 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 & inf A = inf B & sup B = inf C & sup C = sup 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: inf A = inf B and
A4: sup B = inf C and
A5: sup C = sup A ; :: thesis: ( B c= A & C c= A & integral (f `| X),A = (integral (f `| X),B) + (integral (f `| X),C) )
consider x being Real such that
A6: x in B by SUBSET_1:10;
( inf B <= x & x <= sup B ) by A6, INTEGRA2:1;
then A7: inf B <= sup B by XXREAL_0:2;
consider x being Real such that
A8: x in C by SUBSET_1:10;
( inf C <= x & x <= sup C ) by A8, INTEGRA2:1;
then A9: inf C <= sup C by XXREAL_0:2;
for x being set st x in B holds
x in A

proof

let x be set ; :: thesis: ( x in B implies x in A )
assume A10: x in B ; :: thesis: x in A
then reconsider x = x as Real ;
x <= sup B by A10, INTEGRA2:1;
then A11: x <= sup A by A4, A5, A9, XXREAL_0:2;
inf A <= x by A3, A10, INTEGRA2:1;
hence x in A by A11, INTEGRA2:1; :: 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 A1, FDIFF_1:def 8;
then A14: (f `| X) | A is bounded by A2, Th10;
then A15: (f `| X) | B is bounded by A12, RFUNCT_1:91;
for x being set st x in C holds
x in A

proof

let x be set ; :: thesis: ( x in C implies x in A )
assume A16: x in C ; :: thesis: x in A
then reconsider x = x as Real ;
inf C <= x by A16, INTEGRA2:1;
then A17: inf A <= x by A3, A4, A7, XXREAL_0:2;
x <= sup A by A5, A16, INTEGRA2:1;
hence x in A by A17, INTEGRA2:1; :: 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 A14, RFUNCT_1:91;
(f `| X) | C is continuous by A2, A18, FCONT_1:17;
then f `| X is_integrable_on C by A13, A18, Th11, XBOOLE_1:1;
then A20: integral (f `| X),C = (f . (sup C)) - (f . (inf C)) by A1, A18, A19, Th13, XBOOLE_1:1;
(f `| X) | B is continuous by A2, A12, FCONT_1:17;
then f `| X is_integrable_on B by A13, A12, Th11, XBOOLE_1:1;
then A21: integral (f `| X),B = (f . (sup B)) - (f . (inf B)) by A1, A12, A15, Th13, XBOOLE_1:1;
f `| X is_integrable_on A by A2, A13, Th11;
then integral (f `| X),A = (f . (sup A)) - (f . (inf A)) 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