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

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

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

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

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)) )
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;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

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

hence A18:
C c= A
by TARSKI:def 3; :: thesis: integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C))
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;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

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