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 A6, INTEGRA2:1;
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 A8, INTEGRA2:1;
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 A10, INTEGRA2:1;
then A11: x <= upper_bound A by A4, A5, A9, XXREAL_0:2;
lower_bound 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 7;
then A14: (f `| X) | A is bounded by A2, Th10;
then A15: (f `| X) | B is bounded by A12, RFUNCT_1:74;
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 A16, INTEGRA2:1;
then A17: lower_bound A <= x by A3, A4, A7, XXREAL_0:2;
x <= upper_bound 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:74;
(f `| X) | C is continuous by A2, A18, FCONT_1:16;
then f `| X is_integrable_on C by A13, A18, Th11, XBOOLE_1:1;
then A20: integral ((f `| X),C) = (f . (upper_bound C)) - (f . (lower_bound C)) by A1, A18, A19, Th13, XBOOLE_1:1;
(f `| X) | B is continuous by A2, A12, FCONT_1:16;
then f `| X is_integrable_on B by A13, A12, Th11, XBOOLE_1:1;
then A21: integral ((f `| X),B) = (f . (upper_bound B)) - (f . (lower_bound 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 . (upper_bound A)) - (f . (lower_bound 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