let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f | ['a,b'] is bounded ; :: thesis:
A5: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then ( a in ['a,b'] & b in ['a,b'] ) by A1, XXREAL_1:1;
then A6: ( abs f is_integrable_on ['a,b'] & (abs f) | ['a,b'] is bounded ) by A1, A2, A3, A4, A5, INTEGRA6:22;
A7: dom (abs f) = dom f by VALUED_1:def 11;
set MF1 = 2 (#) (max+ f);
A8: 2 (#) (max+ f) = f + (abs f) by RFUNCT_3:34;
then A9: ( 2 (#) (max+ f) is_integrable_on ['a,b'] & (2 (#) (max+ f)) | ['a,b'] is bounded ) by A1, A2, A3, A4, A5, A6, A7, INTEGRA6:19;
A10: dom (max+ f) = dom f by RFUNCT_3:def 10;
then A11: dom (2 (#) (max+ f)) = dom f by VALUED_1:def 5;
(1 / 2) (#) (2 (#) (max+ f)) = ((1 / 2) * 2) (#) (max+ f) by RFUNCT_1:17;
hence A12: max+ f is_integrable_on ['a,b'] by A2, A5, A9, A11, INTEGRA6:9; :: thesis:
( f | ['a,b'] is bounded_above & f | ['a,b'] is bounded_below ) by A4, SEQ_2:def 8;
then ( (max+ f) | ['a,b'] is bounded_above & (max+ f) | ['a,b'] is bounded_below ) by INTEGRA4:14, INTEGRA4:15;
then A13: (max+ f) | ['a,b'] is bounded by SEQ_2:def 8;
A14: - f = (- 1) (#) f by VALUED_1:def 6;
then A15: - f is_integrable_on ['a,b'] by A2, A3, A4, A5, INTEGRA6:9;
A16: (- f) | ['a,b'] is bounded by A4, A14, RFUNCT_1:80;
A17: abs (- f) = |.(- 1).| (#) (abs f) by A14, RFUNCT_1:25
.= (- (- 1)) (#) (abs f) by COMPLEX1:70
.= abs f ;
A18: dom (- f) = dom f by A14, VALUED_1:def 5;
set MF2 = 2 (#) (max- f);
A19: max- f = max+ (- f) by INTEGRA4:21;
then A20: 2 (#) (max- f) = (- f) + (abs f) by A17, RFUNCT_3:34;
then A21: ( 2 (#) (max- f) is_integrable_on ['a,b'] & (2 (#) (max- f)) | ['a,b'] is bounded ) by A1, A2, A5, A7, A15, A16, A6, A18, INTEGRA6:19;
A22: dom (max- f) = dom f by RFUNCT_3:def 11;
then A23: ['a,b'] c= dom (2 (#) (max- f)) by A2, A5, VALUED_1:def 5;
(1 / 2) (#) (2 (#) (max- f)) = ((1 / 2) * 2) (#) (max- f) by RFUNCT_1:17;
hence A24: max- f is_integrable_on ['a,b'] by A21, A23, INTEGRA6:9; :: thesis:
( (- f) | ['a,b'] is bounded_above & (- f) | ['a,b'] is bounded_below ) by A16, SEQ_2:def 8;
then ( (max+ (- f)) | ['a,b'] is bounded_above & (max+ (- f)) | ['a,b'] is bounded_below ) by INTEGRA4:14, INTEGRA4:15;
then A25: (max- f) | ['a,b'] is bounded by A19, SEQ_2:def 8;
integral ((2 (#) (max+ f)),a,b) = (integral (f,a,b)) + (integral ((abs f),a,b)) by A1, A2, A3, A4, A5, A6, A7, A8, INTEGRA6:12;
hence A26: 2 * (integral ((max+ f),a,b)) = (integral (f,a,b)) + (integral ((abs f),a,b)) by A1, A2, A5, A12, A10, A13, INTEGRA6:10; :: thesis:
A27: integral ((- f),a,b) = (- 1) * (integral (f,a,b)) by A1, A2, A3, A4, A5, A14, INTEGRA6:10;
integral ((2 (#) (max- f)),a,b) = (integral ((- f),a,b)) + (integral ((abs f),a,b)) by A1, A2, A5, A15, A16, A18, A6, A7, A20, INTEGRA6:12;
hence 2 * (integral ((max- f),a,b)) = (- (integral (f,a,b))) + (integral ((abs f),a,b)) by A27, A1, A2, A5, A24, A22, A25, INTEGRA6:10; :: thesis:
hence integral (f,a,b) = (integral ((max+ f),a,b)) - (integral ((max- f),a,b)) by A26; :: thesis: