:: INTEGRA6 semantic presentation begin theorem Th1: :: INTEGRA6:1 for a, b, c, d being real number st a <= b & c <= d & a + c = b + d holds ( a = b & c = d ) proof let a, b, c, d be real number ; ::_thesis: ( a <= b & c <= d & a + c = b + d implies ( a = b & c = d ) ) assume that A1: ( a <= b & c <= d ) and A2: a + c = b + d ; ::_thesis: ( a = b & c = d ) assume ( not a = b or not c = d ) ; ::_thesis: contradiction then ( a < b or c < d ) by A1, XXREAL_0:1; hence contradiction by A1, A2, XREAL_1:8; ::_thesis: verum end; theorem Th2: :: INTEGRA6:2 for a, b, x being real number st a <= b holds ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ proof let a, b, x be real number ; ::_thesis: ( a <= b implies ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ ) assume a <= b ; ::_thesis: ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ then ( x - b <= x - a & x + a <= x + b ) by XREAL_1:7, XREAL_1:10; hence ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ by XXREAL_1:46; ::_thesis: verum end; theorem Th3: :: INTEGRA6:3 for R being Relation for A, B, C being set st A c= B & A c= C holds (R | B) | A = (R | C) | A proof let R be Relation; ::_thesis: for A, B, C being set st A c= B & A c= C holds (R | B) | A = (R | C) | A let A, B, C be set ; ::_thesis: ( A c= B & A c= C implies (R | B) | A = (R | C) | A ) assume that A1: A c= B and A2: A c= C ; ::_thesis: (R | B) | A = (R | C) | A (R | C) | A = R | A by A2, RELAT_1:74; hence (R | B) | A = (R | C) | A by A1, RELAT_1:74; ::_thesis: verum end; theorem Th4: :: INTEGRA6:4 for A, B, C being set st A c= B & A c= C holds (chi (B,B)) | A = (chi (C,C)) | A proof let A, B, C be set ; ::_thesis: ( A c= B & A c= C implies (chi (B,B)) | A = (chi (C,C)) | A ) assume that A1: A c= B and A2: A c= C ; ::_thesis: (chi (B,B)) | A = (chi (C,C)) | A A3: now__::_thesis:_(_not_A_is_empty_implies_(chi_(B,B))_|_A_=_(chi_(C,C))_|_A_) A4: dom ((chi (C,C)) | A) = (dom (chi (C,C))) /\ A by RELAT_1:61; assume A5: not A is empty ; ::_thesis: (chi (B,B)) | A = (chi (C,C)) | A then not C is empty by A2, XBOOLE_1:58, XBOOLE_1:61; then dom ((chi (C,C)) | A) = C /\ A by A4, RFUNCT_1:61; then A6: dom ((chi (C,C)) | A) = A by A2, XBOOLE_1:28; A7: dom ((chi (B,B)) | A) = (dom (chi (B,B))) /\ A by RELAT_1:61; not B is empty by A1, A5, XBOOLE_1:58, XBOOLE_1:61; then dom ((chi (B,B)) | A) = B /\ A by A7, RFUNCT_1:61; then A8: dom ((chi (B,B)) | A) = A by A1, XBOOLE_1:28; now__::_thesis:_for_x_being_set_st_x_in_A_holds_ ((chi_(B,B))_|_A)_._x_=_((chi_(C,C))_|_A)_._x let x be set ; ::_thesis: ( x in A implies ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x ) assume A9: x in A ; ::_thesis: ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x then ((chi (B,B)) | A) . x = (chi (B,B)) . x by A8, FUNCT_1:47; then ((chi (B,B)) | A) . x = 1 by A1, A9, RFUNCT_1:61; then ((chi (B,B)) | A) . x = (chi (C,C)) . x by A2, A9, RFUNCT_1:61; hence ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x by A6, A9, FUNCT_1:47; ::_thesis: verum end; hence (chi (B,B)) | A = (chi (C,C)) | A by A8, A6, FUNCT_1:2; ::_thesis: verum end; now__::_thesis:_(_A_is_empty_implies_(chi_(B,B))_|_A_=_(chi_(C,C))_|_A_) assume A10: A is empty ; ::_thesis: (chi (B,B)) | A = (chi (C,C)) | A then (chi (B,B)) | A = {} ; hence (chi (B,B)) | A = (chi (C,C)) | A by A10; ::_thesis: verum end; hence (chi (B,B)) | A = (chi (C,C)) | A by A3; ::_thesis: verum end; theorem Th5: :: INTEGRA6:5 for a, b being real number st a <= b holds vol ['a,b'] = b - a proof let a, b be real number ; ::_thesis: ( a <= b implies vol ['a,b'] = b - a ) assume a <= b ; ::_thesis: vol ['a,b'] = b - a then A1: ['a,b'] = [.a,b.] by INTEGRA5:def_3; then A2: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by INTEGRA1:4; then a = lower_bound [.a,b.] by A1, INTEGRA1:5; hence vol ['a,b'] = b - a by A1, A2, INTEGRA1:5; ::_thesis: verum end; theorem Th6: :: INTEGRA6:6 for a, b being real number holds vol ['(min (a,b)),(max (a,b))'] = abs (b - a) proof let a, b be real number ; ::_thesis: vol ['(min (a,b)),(max (a,b))'] = abs (b - a) percases ( a <= b or not a <= b ) ; supposeA1: a <= b ; ::_thesis: vol ['(min (a,b)),(max (a,b))'] = abs (b - a) then ( min (a,b) = a & max (a,b) = b ) by XXREAL_0:def_9, XXREAL_0:def_10; then A2: vol ['(min (a,b)),(max (a,b))'] = b - a by Th5, XXREAL_0:25; 0 <= b - a by A1, XREAL_1:48; hence vol ['(min (a,b)),(max (a,b))'] = abs (b - a) by A2, ABSVALUE:def_1; ::_thesis: verum end; supposeA3: not a <= b ; ::_thesis: vol ['(min (a,b)),(max (a,b))'] = abs (b - a) then 0 <= a - b by XREAL_1:48; then A4: a - b = abs (a - b) by ABSVALUE:def_1 .= abs (b - a) by COMPLEX1:60 ; ( min (a,b) = b & max (a,b) = a ) by A3, XXREAL_0:def_9, XXREAL_0:def_10; hence vol ['(min (a,b)),(max (a,b))'] = abs (b - a) by A4, Th5, XXREAL_0:17; ::_thesis: verum end; end; end; begin Lm1: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st A c= dom f holds f || A is Function of A,REAL proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st A c= dom f holds f || A is Function of A,REAL let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f implies f || A is Function of A,REAL ) rng f c= REAL ; then A1: f is Function of (dom f),REAL by FUNCT_2:2; assume A c= dom f ; ::_thesis: f || A is Function of A,REAL hence f || A is Function of A,REAL by A1, FUNCT_2:32; ::_thesis: verum end; theorem Th7: :: INTEGRA6:7 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st A c= dom f & f is_integrable_on A & f | A is bounded holds ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st A c= dom f & f is_integrable_on A & f | A is bounded holds ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) ) A1: abs (f || A) = (abs f) || A by RFUNCT_1:46; assume A c= dom f ; ::_thesis: ( not f is_integrable_on A or not f | A is bounded or ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) ) then A2: f || A is Function of A,REAL by Lm1; assume ( f is_integrable_on A & f | A is bounded ) ; ::_thesis: ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) then A3: ( f || A is integrable & (f || A) | A is bounded ) by INTEGRA5:def_1; thus ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) by A3, A2, A1, INTEGRA4:23, INTEGRA5:def_1; ::_thesis: verum end; theorem Th8: :: INTEGRA6:8 for a, b being real number for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds abs (integral (f,a,b)) <= integral ((abs f),a,b) proof let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds abs (integral (f,a,b)) <= integral ((abs f),a,b) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies abs (integral (f,a,b)) <= integral ((abs f),a,b) ) assume a <= b ; ::_thesis: ( not ['a,b'] c= dom f or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or abs (integral (f,a,b)) <= integral ((abs f),a,b) ) then ( integral (f,a,b) = integral (f,['a,b']) & integral ((abs f),a,b) = integral ((abs f),['a,b']) ) by INTEGRA5:def_4; hence ( not ['a,b'] c= dom f or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or abs (integral (f,a,b)) <= integral ((abs f),a,b) ) by Th7; ::_thesis: verum end; theorem Th9: :: INTEGRA6:9 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let f be PartFunc of REAL,REAL; ::_thesis: for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let r be Real; ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) ) assume that A1: A c= dom f and A2: ( f is_integrable_on A & f | A is bounded ) ; ::_thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) A3: ( f || A is integrable & (f || A) | A is bounded ) by A2, INTEGRA5:def_1; rng f c= REAL ; then f is Function of (dom f),REAL by FUNCT_2:2; then A4: f | A is Function of A,REAL by A1, FUNCT_2:32; r (#) (f || A) = (r (#) f) | A by RFUNCT_1:49; then (r (#) f) || A is integrable by A3, A4, INTEGRA2:31; hence r (#) f is_integrable_on A by INTEGRA5:def_1; ::_thesis: integral ((r (#) f),A) = r * (integral (f,A)) integral ((r (#) f),A) = integral (r (#) (f || A)) by RFUNCT_1:49; hence integral ((r (#) f),A) = r * (integral (f,A)) by A3, A4, INTEGRA2:31; ::_thesis: verum end; theorem Th10: :: INTEGRA6:10 for a, b, c being real number for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds integral ((c (#) f),a,b) = c * (integral (f,a,b)) proof let a, b, c be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds integral ((c (#) f),a,b) = c * (integral (f,a,b)) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies integral ((c (#) f),a,b) = c * (integral (f,a,b)) ) A1: c is Real by XREAL_0:def_1; assume that A2: a <= b and A3: ( ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ; ::_thesis: integral ((c (#) f),a,b) = c * (integral (f,a,b)) ( integral (f,a,b) = integral (f,['a,b']) & integral ((c (#) f),a,b) = integral ((c (#) f),['a,b']) ) by A2, INTEGRA5:def_4; hence integral ((c (#) f),a,b) = c * (integral (f,a,b)) by A1, A3, Th9; ::_thesis: verum end; theorem Th11: :: INTEGRA6:11 for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) let f, g be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded implies ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) ) assume that A1: ( A c= dom f & A c= dom g ) and A2: f is_integrable_on A and A3: f | A is bounded and A4: g is_integrable_on A and A5: g | A is bounded ; ::_thesis: ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) A6: ( (f || A) | A is bounded & (g || A) | A is bounded ) by A3, A5; A7: ( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1; A8: ( (f || A) + (g || A) = (f + g) || A & (f || A) - (g || A) = (f - g) || A ) by RFUNCT_1:44, RFUNCT_1:47; A9: ( f || A is integrable & g || A is integrable ) by A2, A4, INTEGRA5:def_1; then ( (f || A) + (g || A) is integrable & (f || A) - (g || A) is integrable ) by A6, A7, INTEGRA1:57, INTEGRA2:33; hence ( f + g is_integrable_on A & f - g is_integrable_on A ) by A8, INTEGRA5:def_1; ::_thesis: ( integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) thus ( integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) by A9, A6, A7, A8, INTEGRA1:57, INTEGRA2:33; ::_thesis: verum end; theorem Th12: :: INTEGRA6:12 for a, b being real number for f, g being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded holds ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) proof let a, b be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded holds ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded implies ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) ) assume that A1: a <= b and A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) ; ::_thesis: ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) A3: ( integral ((f + g),a,b) = integral ((f + g),['a,b']) & integral ((f - g),a,b) = integral ((f - g),['a,b']) ) by A1, INTEGRA5:def_4; ( integral (f,a,b) = integral (f,['a,b']) & integral (g,a,b) = integral (g,['a,b']) ) by A1, INTEGRA5:def_4; hence ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) by A2, A3, Th11; ::_thesis: verum end; theorem :: INTEGRA6:13 for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL st f | A is bounded & g | A is bounded holds (f (#) g) | A is bounded proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL st f | A is bounded & g | A is bounded holds (f (#) g) | A is bounded let f, g be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded & g | A is bounded implies (f (#) g) | A is bounded ) assume ( f | A is bounded & g | A is bounded ) ; ::_thesis: (f (#) g) | A is bounded then (f (#) g) | (A /\ A) is bounded by RFUNCT_1:84; hence (f (#) g) | A is bounded ; ::_thesis: verum end; theorem :: INTEGRA6:14 for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds f (#) g is_integrable_on A proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds f (#) g is_integrable_on A let f, g be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded implies f (#) g is_integrable_on A ) assume that A1: ( A c= dom f & A c= dom g ) and A2: ( f is_integrable_on A & f | A is bounded ) and A3: ( g is_integrable_on A & g | A is bounded ) ; ::_thesis: f (#) g is_integrable_on A A4: ( f || A is integrable & (f || A) | A is bounded ) by A2, INTEGRA5:def_1; A5: ( g || A is integrable & (g || A) | A is bounded ) by A3, INTEGRA5:def_1; A6: (f || A) (#) (g || A) = (f (#) g) || A by INTEGRA5:4; ( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1; then (f (#) g) || A is integrable by A4, A5, A6, INTEGRA4:29; hence f (#) g is_integrable_on A by INTEGRA5:def_1; ::_thesis: verum end; theorem Th15: :: INTEGRA6:15 for A being non empty closed_interval Subset of REAL for n being Element of NAT st n > 0 & vol A > 0 holds ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st n > 0 & vol A > 0 holds ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) let n be Element of NAT ; ::_thesis: ( n > 0 & vol A > 0 implies ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) ) assume that A1: n > 0 and A2: vol A > 0 ; ::_thesis: ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) deffunc H1( Nat) -> Element of REAL = (lower_bound A) + (((vol A) / n) * $1); consider D being FinSequence of REAL such that A3: ( len D = n & ( for i being Nat st i in dom D holds D . i = H1(i) ) ) from FINSEQ_2:sch_1(); A4: for i, j being Element of NAT st i in dom D & j in dom D & i < j holds D . i < D . j proof let i, j be Element of NAT ; ::_thesis: ( i in dom D & j in dom D & i < j implies D . i < D . j ) assume that A5: i in dom D and A6: j in dom D and A7: i < j ; ::_thesis: D . i < D . j (vol A) / n > 0 by A1, A2, XREAL_1:139; then ((vol A) / n) * i < ((vol A) / n) * j by A7, XREAL_1:68; then (lower_bound A) + (((vol A) / n) * i) < (lower_bound A) + (((vol A) / n) * j) by XREAL_1:6; then D . i < (lower_bound A) + (((vol A) / n) * j) by A3, A5; hence D . i < D . j by A3, A6; ::_thesis: verum end; A8: dom D = Seg n by A3, FINSEQ_1:def_3; reconsider D = D as non empty increasing FinSequence of REAL by A1, A3, A4, SEQM_3:def_1; D . (len D) = (lower_bound A) + (((vol A) / n) * n) by A3, A8, FINSEQ_1:3; then A9: D . (len D) = (lower_bound A) + (vol A) by A1, XCMPLX_1:87; for x1 being set st x1 in rng D holds x1 in A proof let x1 be set ; ::_thesis: ( x1 in rng D implies x1 in A ) assume x1 in rng D ; ::_thesis: x1 in A then consider i being Element of NAT such that A10: i in dom D and A11: D . i = x1 by PARTFUN1:3; A12: 1 <= i by A10, FINSEQ_3:25; i <= len D by A10, FINSEQ_3:25; then ((vol A) / n) * i <= ((vol A) / n) * n by A2, A3, XREAL_1:64; then ((vol A) / n) * i <= vol A by A1, XCMPLX_1:87; then A13: (lower_bound A) + (((vol A) / n) * i) <= (lower_bound A) + (vol A) by XREAL_1:6; (vol A) / n > 0 by A1, A2, XREAL_1:139; then A14: lower_bound A <= (lower_bound A) + (((vol A) / n) * i) by A12, XREAL_1:29, XREAL_1:129; x1 = (lower_bound A) + (((vol A) / n) * i) by A3, A10, A11; hence x1 in A by A14, A13, INTEGRA2:1; ::_thesis: verum end; then rng D c= A by TARSKI:def_3; then reconsider D = D as Division of A by A9, INTEGRA1:def_2; take D ; ::_thesis: ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) thus ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) by A3; ::_thesis: verum end; begin theorem Th16: :: INTEGRA6:16 for A being non empty closed_interval Subset of REAL st vol A > 0 holds ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( vol A > 0 implies ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) ) defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of A st ( n = $1 & e = $2 & e divide_into_equal n + 1 ); assume A1: vol A > 0 ; ::_thesis: ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) A2: for n being Element of NAT ex D being Element of divs A st S1[n,D] proof let n be Element of NAT ; ::_thesis: ex D being Element of divs A st S1[n,D] consider D being Division of A such that A3: ( len D = n + 1 & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / (n + 1)) * i) ) ) by A1, Th15; reconsider D1 = D as Element of divs A by INTEGRA1:def_3; take D1 ; ::_thesis: S1[n,D1] D divide_into_equal n + 1 by A3, INTEGRA4:def_1; hence S1[n,D1] ; ::_thesis: verum end; consider T being Function of NAT,(divs A) such that A4: for n being Element of NAT holds S1[n,T . n] from FUNCT_2:sch_3(A2); reconsider T = T as DivSequence of A ; A5: for n being Element of NAT ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) proof let n be Element of NAT ; ::_thesis: ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) ex n1 being Element of NAT ex Tn being Division of A st ( n1 = n & Tn = T . n & Tn divide_into_equal n1 + 1 ) by A4; hence ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) ; ::_thesis: verum end; A6: for i being Element of NAT holds (delta T) . i = (vol A) / (i + 1) proof let i be Element of NAT ; ::_thesis: (delta T) . i = (vol A) / (i + 1) for x1 being set st x1 in rng (upper_volume ((chi (A,A)),(T . i))) holds x1 in {((vol A) / (i + 1))} proof reconsider D = T . i as Division of A ; let x1 be set ; ::_thesis: ( x1 in rng (upper_volume ((chi (A,A)),(T . i))) implies x1 in {((vol A) / (i + 1))} ) assume x1 in rng (upper_volume ((chi (A,A)),(T . i))) ; ::_thesis: x1 in {((vol A) / (i + 1))} then consider k being Element of NAT such that A7: k in dom (upper_volume ((chi (A,A)),(T . i))) and A8: (upper_volume ((chi (A,A)),(T . i))) . k = x1 by PARTFUN1:3; k in Seg (len (upper_volume ((chi (A,A)),(T . i)))) by A7, FINSEQ_1:def_3; then k in Seg (len D) by INTEGRA1:def_6; then A9: k in dom D by FINSEQ_1:def_3; A10: ex n being Element of NAT ex e being Division of A st ( n = i & e = D & e divide_into_equal n + 1 ) by A4; A11: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) proof A12: now__::_thesis:_(_k_=_1_implies_(upper_bound_(divset_(D,k)))_-_(lower_bound_(divset_(D,k)))_=_(vol_A)_/_(i_+_1)_) A13: len D = i + 1 by A10, INTEGRA4:def_1; assume A14: k = 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) then upper_bound (divset (D,k)) = D . 1 by A9, INTEGRA1:def_4; then upper_bound (divset (D,k)) = (lower_bound A) + (((vol A) / (i + 1)) * 1) by A10, A9, A14, A13, INTEGRA4:def_1; then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = ((lower_bound A) + ((vol A) / (i + 1))) - (lower_bound A) by A9, A14, INTEGRA1:def_4; hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; ::_thesis: verum end; now__::_thesis:_(_k_<>_1_implies_(upper_bound_(divset_(D,k)))_-_(lower_bound_(divset_(D,k)))_=_(vol_A)_/_(i_+_1)_) assume A15: k <> 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) then k - 1 in dom D by A9, INTEGRA1:7; then A16: D . (k - 1) = (lower_bound A) + (((vol A) / (len D)) * (k - 1)) by A10, INTEGRA4:def_1; A17: D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A10, A9, INTEGRA4:def_1; ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by A9, A15, INTEGRA1:def_4; hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A10, A16, A17, INTEGRA4:def_1; ::_thesis: verum end; hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A12; ::_thesis: verum end; x1 = vol (divset (D,k)) by A8, A9, INTEGRA1:20; hence x1 in {((vol A) / (i + 1))} by A11, TARSKI:def_1; ::_thesis: verum end; then A18: rng (upper_volume ((chi (A,A)),(T . i))) c= {((vol A) / (i + 1))} by TARSKI:def_3; for x1 being set st x1 in {((vol A) / (i + 1))} holds x1 in rng (upper_volume ((chi (A,A)),(T . i))) proof reconsider D = T . i as Division of A ; let x1 be set ; ::_thesis: ( x1 in {((vol A) / (i + 1))} implies x1 in rng (upper_volume ((chi (A,A)),(T . i))) ) assume x1 in {((vol A) / (i + 1))} ; ::_thesis: x1 in rng (upper_volume ((chi (A,A)),(T . i))) then A19: x1 = (vol A) / (i + 1) by TARSKI:def_1; A20: ex n being Element of NAT ex e being Division of A st ( n = i & e = D & e divide_into_equal n + 1 ) by A4; rng D <> {} ; then A21: 1 in dom D by FINSEQ_3:32; then upper_bound (divset (D,1)) = D . 1 by INTEGRA1:def_4; then upper_bound (divset (D,1)) = (lower_bound A) + (((vol A) / (len D)) * 1) by A21, A20, INTEGRA4:def_1; then A22: vol (divset (D,1)) = ((lower_bound A) + ((vol A) / (len D))) - (lower_bound A) by A21, INTEGRA1:def_4; 1 in Seg (len D) by A21, FINSEQ_1:def_3; then 1 in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then A23: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; (upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by A21, INTEGRA1:20; hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by A19, A23, A20, A22, INTEGRA4:def_1; ::_thesis: verum end; then {((vol A) / (i + 1))} c= rng (upper_volume ((chi (A,A)),(T . i))) by TARSKI:def_3; then ( (delta T) . i = delta (T . i) & rng (upper_volume ((chi (A,A)),(T . i))) = {((vol A) / (i + 1))} ) by A18, INTEGRA3:def_2, XBOOLE_0:def_10; then (delta T) . i in {((vol A) / (i + 1))} by XXREAL_2:def_8; hence (delta T) . i = (vol A) / (i + 1) by TARSKI:def_1; ::_thesis: verum end; A24: for a being Real st 0 < a holds ex i being Element of NAT st abs (((delta T) . i) - 0) < a proof let a be Real; ::_thesis: ( 0 < a implies ex i being Element of NAT st abs (((delta T) . i) - 0) < a ) A25: vol A >= 0 by INTEGRA1:9; reconsider i1 = [\((vol A) / a)/] + 1 as Integer ; assume A26: 0 < a ; ::_thesis: ex i being Element of NAT st abs (((delta T) . i) - 0) < a then [\((vol A) / a)/] + 1 > 0 by A25, INT_1:29; then reconsider i1 = i1 as Element of NAT by INT_1:3; i1 < i1 + 1 by NAT_1:13; then (vol A) / a < 1 * (i1 + 1) by INT_1:29, XXREAL_0:2; then A27: (vol A) / (i1 + 1) < 1 * a by A26, XREAL_1:113; A28: (delta T) . i1 = (vol A) / (i1 + 1) by A6; ((vol A) / (i1 + 1)) - 0 = abs (((vol A) / (i1 + 1)) - 0) by A25, ABSVALUE:def_1; hence ex i being Element of NAT st abs (((delta T) . i) - 0) < a by A27, A28; ::_thesis: verum end; A29: for i, j being Element of NAT st i <= j holds (delta T) . i >= (delta T) . j proof let i, j be Element of NAT ; ::_thesis: ( i <= j implies (delta T) . i >= (delta T) . j ) assume i <= j ; ::_thesis: (delta T) . i >= (delta T) . j then A30: i + 1 <= j + 1 by XREAL_1:6; vol A >= 0 by INTEGRA1:9; then (vol A) / (i + 1) >= (vol A) / (j + 1) by A30, XREAL_1:118; then (delta T) . i >= (vol A) / (j + 1) by A6; hence (delta T) . i >= (delta T) . j by A6; ::_thesis: verum end; A31: for a being real number st 0 < a holds ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a proof let a be real number ; ::_thesis: ( 0 < a implies ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a ) assume A32: 0 < a ; ::_thesis: ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a a is Real by XREAL_0:def_1; then consider i being Element of NAT such that A33: abs (((delta T) . i) - 0) < a by A24, A32; (delta T) . i = delta (T . i) by INTEGRA3:def_2; then (delta T) . i >= 0 by INTEGRA3:9; then A34: (delta T) . i < a by A33, ABSVALUE:def_1; now__::_thesis:_for_j_being_Element_of_NAT_st_i_<=_j_holds_ abs_(((delta_T)_._j)_-_0)_<_a let j be Element of NAT ; ::_thesis: ( i <= j implies abs (((delta T) . j) - 0) < a ) assume i <= j ; ::_thesis: abs (((delta T) . j) - 0) < a then (delta T) . j <= (delta T) . i by A29; then A35: (delta T) . j < a by A34, XXREAL_0:2; (delta T) . j = delta (T . j) by INTEGRA3:def_2; then (delta T) . j >= 0 by INTEGRA3:9; hence abs (((delta T) . j) - 0) < a by A35, ABSVALUE:def_1; ::_thesis: verum end; hence ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a ; ::_thesis: verum end; then A36: delta T is convergent by SEQ_2:def_6; then lim (delta T) = 0 by A31, SEQ_2:def_7; hence ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) by A5, A36; ::_thesis: verum end; Lm2: for a, b, c being real number for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c holds ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) proof let a, b, c be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c holds ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c implies ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) ) 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 and A5: c in ['a,b'] and A6: b <> c ; ::_thesis: ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A8: c <= b by A5, XXREAL_1:1; then A9: ['c,b'] = [.c,b.] by INTEGRA5:def_3; then A10: [.c,b.] = [.(lower_bound [.c,b.]),(upper_bound [.c,b.]).] by INTEGRA1:4; then A11: upper_bound ['c,b'] = b by A9, INTEGRA1:5; set FAB = f || ['a,b']; set FAC = f || ['a,c']; set FCB = f || ['c,b']; A12: f || ['a,b'] is Function of ['a,b'],REAL by A2, Lm1; A13: a <= c by A5, A7, XXREAL_1:1; then A14: ['a,c'] = [.a,c.] by INTEGRA5:def_3; then A15: [.a,c.] = [.(lower_bound [.a,c.]),(upper_bound [.a,c.]).] by INTEGRA1:4; then A16: lower_bound ['a,c'] = a by A14, INTEGRA1:5; A17: ['c,b'] c= ['a,b'] by A7, A13, A9, XXREAL_1:34; then f | ['c,b'] is bounded by A4, RFUNCT_1:74; then A18: (f || ['c,b']) | ['c,b'] is bounded ; A19: lower_bound ['c,b'] = c by A9, A10, INTEGRA1:5; ex PS2 being DivSequence of ['c,b'] st ( delta PS2 is convergent & lim (delta PS2) = 0 & ex K being Element of NAT st for i being Element of NAT st K <= i holds ex S2i being Division of ['c,b'] st ( S2i = PS2 . i & 2 <= len S2i ) ) proof c < b by A6, A8, XXREAL_0:1; then vol ['c,b'] > 0 by A19, A11, XREAL_1:50; then consider T being DivSequence of ['c,b'] such that A20: ( delta T is convergent & lim (delta T) = 0 ) and A21: for n being Element of NAT ex Tn being Division of ['c,b'] st ( Tn divide_into_equal n + 1 & T . n = Tn ) by Th16; take T ; ::_thesis: ( delta T is convergent & lim (delta T) = 0 & ex K being Element of NAT st for i being Element of NAT st K <= i holds ex S2i being Division of ['c,b'] st ( S2i = T . i & 2 <= len S2i ) ) now__::_thesis:_for_i_being_Element_of_NAT_st_2_<=_i_holds_ ex_Tn_being_Division_of_['c,b']_st_ (_Tn_=_T_._i_&_2_<=_len_Tn_) let i be Element of NAT ; ::_thesis: ( 2 <= i implies ex Tn being Division of ['c,b'] st ( Tn = T . i & 2 <= len Tn ) ) assume A22: 2 <= i ; ::_thesis: ex Tn being Division of ['c,b'] st ( Tn = T . i & 2 <= len Tn ) consider Tn being Division of ['c,b'] such that A23: Tn divide_into_equal i + 1 and A24: T . i = Tn by A21; reconsider Tn = Tn as Division of ['c,b'] ; take Tn = Tn; ::_thesis: ( Tn = T . i & 2 <= len Tn ) thus Tn = T . i by A24; ::_thesis: 2 <= len Tn len Tn = i + 1 by A23, INTEGRA4:def_1; then i <= len Tn by NAT_1:11; hence 2 <= len Tn by A22, XXREAL_0:2; ::_thesis: verum end; hence ( delta T is convergent & lim (delta T) = 0 & ex K being Element of NAT st for i being Element of NAT st K <= i holds ex S2i being Division of ['c,b'] st ( S2i = T . i & 2 <= len S2i ) ) by A20; ::_thesis: verum end; then consider PS2 being DivSequence of ['c,b'] such that A25: ( delta PS2 is convergent & lim (delta PS2) = 0 ) and A26: ex K being Element of NAT st for i being Element of NAT st K <= i holds ex S2i being Division of ['c,b'] st ( S2i = PS2 . i & 2 <= len S2i ) ; consider K being Element of NAT such that A27: for i being Element of NAT st K <= i holds ex S2i being Division of ['c,b'] st ( S2i = PS2 . i & 2 <= len S2i ) by A26; defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of ['c,b'] st ( n = $1 & e = $2 & e = PS2 . (n + K) ); A28: for n being Element of NAT ex D being Element of divs ['c,b'] st S1[n,D] proof let n be Element of NAT ; ::_thesis: ex D being Element of divs ['c,b'] st S1[n,D] reconsider D = PS2 . (n + K) as Element of divs ['c,b'] by INTEGRA1:def_3; take D ; ::_thesis: S1[n,D] thus S1[n,D] ; ::_thesis: verum end; consider S2 being Function of NAT,(divs ['c,b']) such that A29: for n being Element of NAT holds S1[n,S2 . n] from FUNCT_2:sch_3(A28); reconsider S2 = S2 as DivSequence of ['c,b'] ; defpred S2[ Element of NAT , set ] means ex S being Division of ['c,b'] st ( S = S2 . $1 & $2 = S /^ 1 ); A30: now__::_thesis:_for_i_being_Element_of_NAT_ex_S2i_being_Division_of_['c,b']_st_ (_S2i_=_S2_._i_&_2_<=_len_S2i_) let i be Element of NAT ; ::_thesis: ex S2i being Division of ['c,b'] st ( S2i = S2 . i & 2 <= len S2i ) ex n being Element of NAT ex e being Division of ['c,b'] st ( n = i & e = S2 . i & e = PS2 . (n + K) ) by A29; hence ex S2i being Division of ['c,b'] st ( S2i = S2 . i & 2 <= len S2i ) by A27, NAT_1:11; ::_thesis: verum end; A31: for i being Element of NAT ex T being Element of divs ['c,b'] st S2[i,T] proof let i be Element of NAT ; ::_thesis: ex T being Element of divs ['c,b'] st S2[i,T] consider S being Division of ['c,b'] such that A32: S = S2 . i and A33: 2 <= len S by A30; set T = S /^ 1; A34: 1 <= len S by A33, XXREAL_0:2; 2 - 1 <= (len S) - 1 by A33, XREAL_1:13; then A35: 1 <= len (S /^ 1) by A34, RFINSEQ:def_1; then len (S /^ 1) in Seg (len (S /^ 1)) ; then len (S /^ 1) in dom (S /^ 1) by FINSEQ_1:def_3; then (S /^ 1) . (len (S /^ 1)) = S . ((len (S /^ 1)) + 1) by A34, RFINSEQ:def_1; then (S /^ 1) . (len (S /^ 1)) = S . (((len S) - 1) + 1) by A34, RFINSEQ:def_1; then A36: (S /^ 1) . (len (S /^ 1)) = upper_bound ['c,b'] by INTEGRA1:def_2; ( rng S c= ['c,b'] & rng (S /^ 1) c= rng S ) by FINSEQ_5:33, INTEGRA1:def_2; then A37: rng (S /^ 1) c= ['c,b'] by XBOOLE_1:1; ( not S /^ 1 is empty & S /^ 1 is increasing ) by A33, A35, INTEGRA1:34, XXREAL_0:2; then S /^ 1 is Division of ['c,b'] by A37, A36, INTEGRA1:def_2; then S /^ 1 is Element of divs ['c,b'] by INTEGRA1:def_3; hence ex T being Element of divs ['c,b'] st S2[i,T] by A32; ::_thesis: verum end; consider T2 being DivSequence of ['c,b'] such that A38: for i being Element of NAT holds S2[i,T2 . i] from FUNCT_2:sch_3(A31); A39: for n being Element of NAT ex D being Division of ['c,b'] st ( D = T2 . n & ( for i being Element of NAT st i in dom D holds c < D . i ) ) proof let n be Element of NAT ; ::_thesis: ex D being Division of ['c,b'] st ( D = T2 . n & ( for i being Element of NAT st i in dom D holds c < D . i ) ) reconsider D = T2 . n as Division of ['c,b'] ; take D ; ::_thesis: ( D = T2 . n & ( for i being Element of NAT st i in dom D holds c < D . i ) ) consider E being Division of ['c,b'] such that A40: E = S2 . n and A41: T2 . n = E /^ 1 by A38; A42: ex E1 being Division of ['c,b'] st ( E1 = S2 . n & 2 <= len E1 ) by A30; then A43: 2 - 1 <= (len E) - 1 by A40, XREAL_1:13; A44: 1 <= len E by A40, A42, XXREAL_0:2; then 1 in Seg (len E) ; then A45: 1 in dom E by FINSEQ_1:def_3; then ( rng E c= ['c,b'] & E . 1 in rng E ) by FUNCT_1:def_3, INTEGRA1:def_2; then A46: c <= E . 1 by A9, XXREAL_1:1; 2 in Seg (len E) by A40, A42; then 2 in dom E by FINSEQ_1:def_3; then A47: E . 1 < E . 2 by A45, SEQM_3:def_1; len D = (len E) - 1 by A41, A44, RFINSEQ:def_1; then 1 in Seg (len D) by A43; then A48: 1 in dom D by FINSEQ_1:def_3; then A49: D . 1 = E . (1 + 1) by A41, A44, RFINSEQ:def_1; then A50: c < D . 1 by A46, A47, XXREAL_0:2; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_D_holds_ (_(_i_<>_1_implies_c_<_D_._i_)_&_c_<_D_._i_) let i be Element of NAT ; ::_thesis: ( i in dom D implies ( ( i <> 1 implies c < D . i ) & c < D . i ) ) assume A51: i in dom D ; ::_thesis: ( ( i <> 1 implies c < D . i ) & c < D . i ) then A52: 1 <= i by FINSEQ_3:25; hereby ::_thesis: c < D . i assume i <> 1 ; ::_thesis: c < D . i then 1 < i by A52, XXREAL_0:1; then D . 1 < D . i by A48, A51, SEQM_3:def_1; hence c < D . i by A50, XXREAL_0:2; ::_thesis: verum end; hence c < D . i by A49, A46, A47, XXREAL_0:2; ::_thesis: verum end; hence ( D = T2 . n & ( for i being Element of NAT st i in dom D holds c < D . i ) ) ; ::_thesis: verum end; set XAC = chi (['a,c'],['a,c']); set XCB = chi (['c,b'],['c,b']); consider T1 being DivSequence of ['a,c'] such that A53: ( delta T1 is convergent & lim (delta T1) = 0 ) by INTEGRA4:11; A54: for n being Element of NAT ex D being Division of ['c,b'] st ( D = T2 . n & 1 <= len D ) proof let n be Element of NAT ; ::_thesis: ex D being Division of ['c,b'] st ( D = T2 . n & 1 <= len D ) reconsider D = T2 . n as Division of ['c,b'] ; take D ; ::_thesis: ( D = T2 . n & 1 <= len D ) consider E being Division of ['c,b'] such that A55: E = S2 . n and A56: T2 . n = E /^ 1 by A38; ex E1 being Division of ['c,b'] st ( E1 = S2 . n & 2 <= len E1 ) by A30; then ( 1 <= len E & 2 - 1 <= (len E) - 1 ) by A55, XREAL_1:13, XXREAL_0:2; hence ( D = T2 . n & 1 <= len D ) by A56, RFINSEQ:def_1; ::_thesis: verum end; A57: integral (f,c,b) = integral (f,['c,b']) by A8, INTEGRA5:def_4 .= integral (f || ['c,b']) ; A58: integral (f,a,c) = integral (f,['a,c']) by A13, INTEGRA5:def_4; defpred S3[ Element of NAT , set ] means ex S1 being Division of ['a,c'] ex S2 being Division of ['c,b'] st ( S1 = T1 . $1 & S2 = T2 . $1 & $2 = S1 ^ S2 ); A59: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by A7, INTEGRA1:4; then A60: upper_bound ['a,b'] = b by A7, INTEGRA1:5; A61: for i being Element of NAT ex T being Element of divs ['a,b'] st S3[i,T] proof let i0 be Element of NAT ; ::_thesis: ex T being Element of divs ['a,b'] st S3[i0,T] reconsider S1 = T1 . i0 as Division of ['a,c'] ; reconsider S2 = T2 . i0 as Division of ['c,b'] ; set T = S1 ^ S2; ex D being Division of ['c,b'] st ( D = T2 . i0 & 1 <= len D ) by A54; then len S2 in Seg (len S2) ; then A62: len S2 in dom S2 by FINSEQ_1:def_3; A63: rng S1 c= ['a,c'] by INTEGRA1:def_2; now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(S1_^_S2)_&_j_in_dom_(S1_^_S2)_&_i_<_j_holds_ (S1_^_S2)_._i_<_(S1_^_S2)_._j let i, j be Element of NAT ; ::_thesis: ( i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j implies (S1 ^ S2) . i < (S1 ^ S2) . j ) assume that A64: i in dom (S1 ^ S2) and A65: j in dom (S1 ^ S2) and A66: i < j ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j A67: 1 <= i by A64, FINSEQ_3:25; A68: j <= len (S1 ^ S2) by A65, FINSEQ_3:25; A69: i <= len (S1 ^ S2) by A64, FINSEQ_3:25; A70: now__::_thesis:_(_j_>_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_) j <= (len S1) + (len S2) by A68, FINSEQ_1:22; then A71: j - (len S1) <= len S2 by XREAL_1:20; assume A72: j > len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j then A73: (S1 ^ S2) . j = S2 . (j - (len S1)) by A68, FINSEQ_1:24; A74: (len S1) + 1 <= j by A72, NAT_1:13; then consider m being Nat such that A75: ((len S1) + 1) + m = j by NAT_1:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; 1 + m = j - (len S1) by A75; then 1 <= 1 + m by A74, XREAL_1:19; then 1 + m in Seg (len S2) by A75, A71; then A76: j - (len S1) in dom S2 by A75, FINSEQ_1:def_3; A77: now__::_thesis:_(_i_>_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_) i <= (len S1) + (len S2) by A69, FINSEQ_1:22; then A78: i - (len S1) <= len S2 by XREAL_1:20; A79: i - (len S1) < j - (len S1) by A66, XREAL_1:14; assume A80: i > len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j then A81: (len S1) + 1 <= i by NAT_1:13; then consider m being Nat such that A82: ((len S1) + 1) + m = i by NAT_1:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; 1 + m = i - (len S1) by A82; then 1 <= 1 + m by A81, XREAL_1:19; then 1 + m in Seg (len S2) by A82, A78; then A83: i - (len S1) in dom S2 by A82, FINSEQ_1:def_3; (S1 ^ S2) . i = S2 . (i - (len S1)) by A69, A80, FINSEQ_1:24; hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A79, A83, SEQM_3:def_1; ::_thesis: verum end; now__::_thesis:_(_i_<=_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_) assume i <= len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j then A84: i in dom S1 by A67, FINSEQ_3:25; then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def_7; then (S1 ^ S2) . i in rng S1 by A84, FUNCT_1:def_3; then A85: (S1 ^ S2) . i <= c by A14, A63, XXREAL_1:1; ex DD being Division of ['c,b'] st ( DD = T2 . i0 & ( for k being Element of NAT st k in dom DD holds c < DD . k ) ) by A39; hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A85, XXREAL_0:2; ::_thesis: verum end; hence (S1 ^ S2) . i < (S1 ^ S2) . j by A77; ::_thesis: verum end; A86: 1 <= j by A65, FINSEQ_3:25; now__::_thesis:_(_j_<=_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_) assume A87: j <= len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j then A88: j in dom S1 by A86, FINSEQ_3:25; then A89: (S1 ^ S2) . j = S1 . j by FINSEQ_1:def_7; i <= len S1 by A66, A87, XXREAL_0:2; then A90: i in dom S1 by A67, FINSEQ_3:25; then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def_7; hence (S1 ^ S2) . i < (S1 ^ S2) . j by A66, A90, A88, A89, SEQM_3:def_1; ::_thesis: verum end; hence (S1 ^ S2) . i < (S1 ^ S2) . j by A70; ::_thesis: verum end; then A91: S1 ^ S2 is non empty increasing FinSequence of REAL by SEQM_3:def_1; rng S2 c= ['c,b'] by INTEGRA1:def_2; then (rng S1) \/ (rng S2) c= ['a,c'] \/ ['c,b'] by A63, XBOOLE_1:13; then (rng S1) \/ (rng S2) c= [.a,b.] by A13, A8, A14, A9, XXREAL_1:174; then A92: rng (S1 ^ S2) c= ['a,b'] by A7, FINSEQ_1:31; (S1 ^ S2) . (len (S1 ^ S2)) = (S1 ^ S2) . ((len S1) + (len S2)) by FINSEQ_1:22 .= S2 . (len S2) by A62, FINSEQ_1:def_7 .= upper_bound ['a,b'] by A60, A11, INTEGRA1:def_2 ; then S1 ^ S2 is Division of ['a,b'] by A92, A91, INTEGRA1:def_2; then S1 ^ S2 is Element of divs ['a,b'] by INTEGRA1:def_3; hence ex T being Element of divs ['a,b'] st S3[i0,T] ; ::_thesis: verum end; consider T being DivSequence of ['a,b'] such that A93: for i being Element of NAT holds S3[i,T . i] from FUNCT_2:sch_3(A61); A94: lower_bound ['a,b'] = a by A7, A59, INTEGRA1:5; A95: for i, k being Element of NAT for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds divset ((T . i),k) = divset ((T1 . i),k) proof let i, k be Element of NAT ; ::_thesis: for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds divset ((T . i),k) = divset ((T1 . i),k) let S0 be Division of ['a,c']; ::_thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) ) assume A96: S0 = T1 . i ; ::_thesis: ( not k in Seg (len S0) or divset ((T . i),k) = divset ((T1 . i),k) ) reconsider S = T . i as Division of ['a,b'] ; A97: divset ((T1 . i),k) = [.(lower_bound (divset ((T1 . i),k))),(upper_bound (divset ((T1 . i),k))).] by INTEGRA1:4; consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that A98: S1 = T1 . i and S2 = T2 . i and A99: T . i = S1 ^ S2 by A93; assume A100: k in Seg (len S0) ; ::_thesis: divset ((T . i),k) = divset ((T1 . i),k) then A101: k in dom S1 by A96, A98, FINSEQ_1:def_3; len S = (len S1) + (len S2) by A99, FINSEQ_1:22; then len S1 <= len S by NAT_1:11; then Seg (len S1) c= Seg (len S) by FINSEQ_1:5; then k in Seg (len S) by A96, A100, A98; then A102: k in dom S by FINSEQ_1:def_3; A103: divset ((T . i),k) = [.(lower_bound (divset ((T . i),k))),(upper_bound (divset ((T . i),k))).] by INTEGRA1:4; A104: now__::_thesis:_(_k_<>_1_implies_divset_((T_._i),k)_=_divset_((T1_._i),k)_) ( k <= len S1 & k - 1 <= k - 0 ) by A96, A100, A98, FINSEQ_1:1, XREAL_1:10; then A105: k - 1 <= len S1 by XXREAL_0:2; assume A106: k <> 1 ; ::_thesis: divset ((T . i),k) = divset ((T1 . i),k) 1 <= k by A100, FINSEQ_1:1; then A107: 1 < k by A106, XXREAL_0:1; then 1 + 1 <= k by NAT_1:13; then A108: 2 - 1 <= k - 1 by XREAL_1:9; k - 1 is Element of NAT by A107, NAT_1:20; then k - 1 in Seg (len S1) by A105, A108; then A109: k - 1 in dom S1 by FINSEQ_1:def_3; thus divset ((T . i),k) = [.(S . (k - 1)),(upper_bound (divset ((T . i),k))).] by A102, A103, A106, INTEGRA1:def_4 .= [.(S . (k - 1)),(S . k).] by A102, A106, INTEGRA1:def_4 .= [.(S . (k - 1)),(S1 . k).] by A99, A101, FINSEQ_1:def_7 .= [.(S1 . (k - 1)),(S1 . k).] by A99, A109, FINSEQ_1:def_7 .= [.(lower_bound (divset ((T1 . i),k))),(S1 . k).] by A98, A101, A106, INTEGRA1:def_4 .= divset ((T1 . i),k) by A98, A101, A97, A106, INTEGRA1:def_4 ; ::_thesis: verum end; now__::_thesis:_(_k_=_1_implies_divset_((T_._i),k)_=_divset_((T1_._i),k)_) assume A110: k = 1 ; ::_thesis: divset ((T . i),k) = divset ((T1 . i),k) hence divset ((T . i),k) = [.(lower_bound ['a,b']),(upper_bound (divset ((T . i),k))).] by A102, A103, INTEGRA1:def_4 .= [.(lower_bound ['a,b']),(S . k).] by A102, A110, INTEGRA1:def_4 .= [.(lower_bound ['a,b']),(S1 . k).] by A99, A101, FINSEQ_1:def_7 .= [.(lower_bound (divset ((T1 . i),k))),(S1 . 1).] by A94, A16, A98, A101, A110, INTEGRA1:def_4 .= divset ((T1 . i),k) by A98, A101, A97, A110, INTEGRA1:def_4 ; ::_thesis: verum end; hence divset ((T . i),k) = divset ((T1 . i),k) by A104; ::_thesis: verum end; A111: upper_bound ['a,c'] = c by A14, A15, INTEGRA1:5; A112: for i, k being Element of NAT for S01 being Division of ['a,c'] for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) proof let i, k be Element of NAT ; ::_thesis: for S01 being Division of ['a,c'] for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) let S01 be Division of ['a,c']; ::_thesis: for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) let S02 be Division of ['c,b']; ::_thesis: ( S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) implies divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) ) assume that A113: S01 = T1 . i and A114: S02 = T2 . i ; ::_thesis: ( not k in Seg (len S02) or divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) ) reconsider S = T . i as Division of ['a,b'] ; consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that A115: S1 = T1 . i and A116: S2 = T2 . i and A117: T . i = S1 ^ S2 by A93; assume A118: k in Seg (len S02) ; ::_thesis: divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) then A119: k in dom S2 by A114, A116, FINSEQ_1:def_3; then A120: (len S1) + k in dom S by A117, FINSEQ_1:28; A121: divset ((T2 . i),k) = [.(lower_bound (divset ((T2 . i),k))),(upper_bound (divset ((T2 . i),k))).] by INTEGRA1:4; A122: divset ((T . i),((len S1) + k)) = [.(lower_bound (divset ((T . i),((len S1) + k)))),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:4; A123: now__::_thesis:_(_k_<>_1_implies_divset_((T_._i),((len_S1)_+_k))_=_divset_((T2_._i),k)_) ( k <= len S2 & k - 1 <= k - 0 ) by A114, A118, A116, FINSEQ_1:1, XREAL_1:10; then A124: k - 1 <= len S2 by XXREAL_0:2; assume A125: k <> 1 ; ::_thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) A126: 1 <= k by A118, FINSEQ_1:1; then A127: 1 < k by A125, XXREAL_0:1; then 1 + 1 <= k by NAT_1:13; then A128: 2 - 1 <= k - 1 by XREAL_1:9; k - 1 is Element of NAT by A127, NAT_1:20; then k - 1 in Seg (len S2) by A124, A128; then A129: k - 1 in dom S2 by FINSEQ_1:def_3; A130: 1 + 0 < k + (len S1) by A126, XREAL_1:8; hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A120, A122, INTEGRA1:def_4 .= [.(S . (((len S1) + k) - 1)),(S . ((len S1) + k)).] by A120, A130, INTEGRA1:def_4 .= [.(S . ((len S1) + (k - 1))),(S2 . k).] by A117, A119, FINSEQ_1:def_7 .= [.(S2 . (k - 1)),(S2 . k).] by A117, A129, FINSEQ_1:def_7 .= [.(lower_bound (divset ((T2 . i),k))),(S2 . k).] by A116, A119, A125, INTEGRA1:def_4 .= divset ((T2 . i),k) by A116, A119, A121, A125, INTEGRA1:def_4 ; ::_thesis: verum end; now__::_thesis:_(_k_=_1_implies_divset_((T_._i),((len_S1)_+_k))_=_divset_((T2_._i),k)_) len S1 in Seg (len S1) by FINSEQ_1:3; then A131: len S1 in dom S1 by FINSEQ_1:def_3; assume A132: k = 1 ; ::_thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) len S1 <> 0 ; then A133: (len S1) + k <> 1 by A132; hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A120, A122, INTEGRA1:def_4 .= [.(S1 . (len S1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A117, A132, A131, FINSEQ_1:def_7 .= [.(upper_bound ['a,c']),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:def_2 .= [.(lower_bound ['c,b']),(S . ((len S1) + k)).] by A19, A111, A120, A133, INTEGRA1:def_4 .= [.(lower_bound ['c,b']),(S2 . k).] by A117, A119, FINSEQ_1:def_7 .= [.(lower_bound (divset ((T2 . i),k))),(S2 . 1).] by A116, A119, A132, INTEGRA1:def_4 .= divset ((T2 . i),k) by A116, A119, A121, A132, INTEGRA1:def_4 ; ::_thesis: verum end; hence divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) by A113, A115, A123; ::_thesis: verum end; set XAB = chi (['a,b'],['a,b']); A134: for i, k being Element of NAT for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds divset ((T2 . i),k) c= ['c,b'] proof let i, k be Element of NAT ; ::_thesis: for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds divset ((T2 . i),k) c= ['c,b'] let S0 be Division of ['c,b']; ::_thesis: ( S0 = T2 . i & k in Seg (len S0) implies divset ((T2 . i),k) c= ['c,b'] ) assume that A135: S0 = T2 . i and A136: k in Seg (len S0) ; ::_thesis: divset ((T2 . i),k) c= ['c,b'] k in dom S0 by A136, FINSEQ_1:def_3; hence divset ((T2 . i),k) c= ['c,b'] by A135, INTEGRA1:8; ::_thesis: verum end; A137: ['a,c'] c= ['a,b'] by A7, A8, A14, XXREAL_1:34; then f | ['a,c'] is bounded by A4, RFUNCT_1:74; then A138: (f || ['a,c']) | ['a,c'] is bounded ; A139: for i, k being Element of NAT for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds divset ((T1 . i),k) c= ['a,c'] proof let i, k be Element of NAT ; ::_thesis: for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds divset ((T1 . i),k) c= ['a,c'] let S0 be Division of ['a,c']; ::_thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T1 . i),k) c= ['a,c'] ) assume that A140: S0 = T1 . i and A141: k in Seg (len S0) ; ::_thesis: divset ((T1 . i),k) c= ['a,c'] k in dom S0 by A141, FINSEQ_1:def_3; hence divset ((T1 . i),k) c= ['a,c'] by A140, INTEGRA1:8; ::_thesis: verum end; A142: for i being Element of NAT holds upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) proof let i be Element of NAT ; ::_thesis: upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) reconsider F = upper_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ; reconsider F1 = upper_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ; reconsider F2 = upper_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ; reconsider S = T . i as Division of ['a,b'] ; consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that A143: S1 = T1 . i and A144: S2 = T2 . i and A145: T . i = S1 ^ S2 by A93; A146: len F = len S by INTEGRA1:def_6 .= (len S1) + (len S2) by A145, FINSEQ_1:22 .= (len F1) + (len S2) by A143, INTEGRA1:def_6 .= (len F1) + (len F2) by A144, INTEGRA1:def_6 ; A147: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F2_holds_ F_._((len_F1)_+_k)_=_F2_._k let k be Nat; ::_thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k ) assume A148: k in dom F2 ; ::_thesis: F . ((len F1) + k) = F2 . k then A149: k in Seg (len F2) by FINSEQ_1:def_3; then 1 <= k by FINSEQ_1:1; then A150: 1 + (len F1) <= k + (len F1) by XREAL_1:6; k <= len F2 by A149, FINSEQ_1:1; then A151: (len F1) + k <= len F by A146, XREAL_1:6; 1 <= 1 + (len F1) by NAT_1:11; then 1 <= k + (len F1) by A150, XXREAL_0:2; then k + (len F1) in Seg (len F) by A151; then (len F1) + k in Seg (len S) by INTEGRA1:def_6; then (len F1) + k in dom S by FINSEQ_1:def_3; then A152: F . ((len F1) + k) = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def_6; k in Seg (len F2) by A148, FINSEQ_1:def_3; then A153: k in Seg (len S2) by A144, INTEGRA1:def_6; then A154: k in dom S2 by FINSEQ_1:def_3; len F1 = len S1 by A143, INTEGRA1:def_6; then A155: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A143, A144, A153; then A156: divset ((T . i),((len F1) + k)) c= ['c,b'] by A134, A144, A153; then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17, XBOOLE_1:1; then F . ((len F1) + k) = (upper_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A152, A155, A156, Th3; hence F . ((len F1) + k) = F2 . k by A144, A154, INTEGRA1:def_6; ::_thesis: verum end; A157: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_ F_._k_=_F1_._k let k be Nat; ::_thesis: ( k in dom F1 implies F . k = F1 . k ) assume k in dom F1 ; ::_thesis: F . k = F1 . k then A158: k in Seg (len F1) by FINSEQ_1:def_3; then A159: k in Seg (len S1) by A143, INTEGRA1:def_6; then A160: k in dom S1 by FINSEQ_1:def_3; len F1 <= len F by A146, NAT_1:11; then Seg (len F1) c= Seg (len F) by FINSEQ_1:5; then k in Seg (len F) by A158; then k in Seg (len S) by INTEGRA1:def_6; then k in dom S by FINSEQ_1:def_3; then A161: F . k = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by INTEGRA1:def_6; A162: divset ((T . i),k) = divset ((T1 . i),k) by A95, A143, A159; then A163: divset ((T . i),k) c= ['a,c'] by A139, A143, A159; then divset ((T . i),k) c= ['a,b'] by A137, XBOOLE_1:1; then F . k = (upper_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A161, A162, A163, Th3; hence F . k = F1 . k by A143, A160, INTEGRA1:def_6; ::_thesis: verum end; dom F = Seg ((len F1) + (len F2)) by A146, FINSEQ_1:def_3; hence upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A157, A147, FINSEQ_1:def_7; ::_thesis: verum end; A164: for i being Element of NAT holds Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) proof let i be Element of NAT ; ::_thesis: Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A142; hence Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_NAT_holds_(upper_sum_((f_||_['a,b']),T))_._i_=_((upper_sum_((f_||_['a,c']),T1))_._i)_+_((upper_sum_((f_||_['c,b']),T2))_._i) let i be Element of NAT ; ::_thesis: (upper_sum ((f || ['a,b']),T)) . i = ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i) thus (upper_sum ((f || ['a,b']),T)) . i = upper_sum ((f || ['a,b']),(T . i)) by INTEGRA2:def_2 .= (upper_sum ((f || ['a,c']),(T1 . i))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) by A164 .= ((upper_sum ((f || ['a,c']),T1)) . i) + (upper_sum ((f || ['c,b']),(T2 . i))) by INTEGRA2:def_2 .= ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def_2 ; ::_thesis: verum end; then A165: upper_sum ((f || ['a,b']),T) = (upper_sum ((f || ['a,c']),T1)) + (upper_sum ((f || ['c,b']),T2)) by SEQ_1:7; A166: f || ['c,b'] is Function of ['c,b'],REAL by A2, A17, Lm1, XBOOLE_1:1; then A167: lower_integral (f || ['c,b']) <= upper_integral (f || ['c,b']) by A18, INTEGRA1:49; A168: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ abs_(((delta_S2)_._n)_-_0)_<_e let e be real number ; ::_thesis: ( 0 < e implies ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((delta S2) . n) - 0) < e ) assume 0 < e ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((delta S2) . n) - 0) < e then consider m being Element of NAT such that A169: for n being Element of NAT st m <= n holds abs (((delta PS2) . n) - 0) < e by A25, SEQ_2:def_7; take m = m; ::_thesis: for n being Element of NAT st m <= n holds abs (((delta S2) . n) - 0) < e hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( m <= n implies abs (((delta S2) . n) - 0) < e ) A170: n <= n + K by NAT_1:11; assume m <= n ; ::_thesis: abs (((delta S2) . n) - 0) < e then m <= n + K by A170, XXREAL_0:2; then abs (((delta PS2) . (n + K)) - 0) < e by A169; then A171: abs ((delta (PS2 . (n + K))) - 0) < e by INTEGRA3:def_2; ex k being Element of NAT ex e1 being Division of ['c,b'] st ( k = n & e1 = S2 . n & e1 = PS2 . (k + K) ) by A29; hence abs (((delta S2) . n) - 0) < e by A171, INTEGRA3:def_2; ::_thesis: verum end; end; A172: now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ abs_(((delta_T2)_._n)_-_0)_<_e let e be real number ; ::_thesis: ( e > 0 implies ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((delta T2) . n) - 0) < e ) assume A173: e > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((delta T2) . n) - 0) < e then consider m being Element of NAT such that A174: for n being Element of NAT st m <= n holds abs (((delta S2) . n) - 0) < e / 2 by A168, XREAL_1:215; take m = m; ::_thesis: for n being Element of NAT st m <= n holds abs (((delta T2) . n) - 0) < e A175: e / 2 < e by A173, XREAL_1:216; now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_ abs_(((delta_T2)_._n)_-_0)_<_e let n be Element of NAT ; ::_thesis: ( m <= n implies abs (((delta T2) . n) - 0) < e ) assume m <= n ; ::_thesis: abs (((delta T2) . n) - 0) < e then abs (((delta S2) . n) - 0) < e / 2 by A174; then ( 0 <= delta (S2 . n) & abs (delta (S2 . n)) < e / 2 ) by INTEGRA3:9, INTEGRA3:def_2; then A176: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) < e / 2 by ABSVALUE:def_1; A177: for y being real number st y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) holds y < e proof reconsider D = T2 . n as Division of ['c,b'] ; let y be real number ; ::_thesis: ( y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) implies y < e ) assume y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) ; ::_thesis: y < e then consider x being set such that A178: x in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) and A179: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) . x by FUNCT_1:def_3; reconsider i = x as Element of NAT by A178; A180: x in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) by A178, FINSEQ_1:def_3; consider E1 being Division of ['c,b'] such that A181: E1 = S2 . n and A182: 2 <= len E1 by A30; set i1 = i + 1; consider E being Division of ['c,b'] such that A183: E = S2 . n and A184: T2 . n = E /^ 1 by A38; A185: 1 <= len E1 by A182, XXREAL_0:2; then A186: len D = (len E) - 1 by A183, A184, A181, RFINSEQ:def_1; A187: len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = len D by INTEGRA1:def_6; then A188: dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = dom D by FINSEQ_3:29; A189: now__::_thesis:_(_i_=_1_implies_y_<_e_) len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by A183, INTEGRA1:def_6; then 2 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A183, A181, A182; then 2 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def_3; then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def_3; then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def_8; then A190: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 < e / 2 by A176, XXREAL_0:2; assume A191: i = 1 ; ::_thesis: y < e then A192: 1 in dom D by A180, A187, FINSEQ_1:def_3; len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by A183, A186, INTEGRA1:def_6; then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def_6; then 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A180, A191, FINSEQ_2:8; then 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def_3; then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def_3; then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def_8; then A193: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 < e / 2 by A176, XXREAL_0:2; A194: 2 in dom E by A183, A181, A182, FINSEQ_3:25; 1 in Seg (len E) by A183, A181, A185; then A195: 1 in dom E by FINSEQ_1:def_3; divset ((S2 . n),1) = [.(lower_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),1))).] by INTEGRA1:4; then A196: divset ((S2 . n),1) = [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] by A183, A195, INTEGRA1:def_4; then A197: [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]).] by INTEGRA1:4; A198: divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),1))),(upper_bound (divset ((T2 . n),1))).] by A191, INTEGRA1:4 .= [.(lower_bound ['c,b']),(upper_bound (divset ((T2 . n),1))).] by A192, INTEGRA1:def_4 .= [.(lower_bound ['c,b']),(D . 1).] by A192, INTEGRA1:def_4 .= [.(lower_bound ['c,b']),(E . (1 + 1)).] by A183, A184, A181, A185, A192, RFINSEQ:def_1 .= [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] by A183, A194, INTEGRA1:def_4 ; then [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4; then A199: ( lower_bound ['c,b'] = lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] & upper_bound (divset ((S2 . n),2)) = upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] ) by A198, INTEGRA1:5; y = vol (divset ((T2 . n),1)) by A178, A179, A188, A191, INTEGRA1:20; then y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + ((upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]) - (lower_bound ['c,b'])) by A191, A198, A199, A196; then A200: y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + (vol (divset ((S2 . n),1))) by A196, A197, INTEGRA1:5; divset ((S2 . n),2) = [.(lower_bound (divset ((S2 . n),2))),(upper_bound (divset ((S2 . n),2))).] by INTEGRA1:4; then divset ((S2 . n),2) = [.(E . (2 - 1)),(upper_bound (divset ((S2 . n),2))).] by A183, A194, INTEGRA1:def_4; then A201: divset ((S2 . n),2) = [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] by A183, A195, INTEGRA1:def_4; then [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4; then y = (vol (divset ((S2 . n),2))) + (vol (divset ((S2 . n),1))) by A201, A200, INTEGRA1:5; then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + (vol (divset ((S2 . n),1))) by A183, A194, INTEGRA1:20; then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1) by A183, A195, INTEGRA1:20; then y < (e / 2) + (e / 2) by A190, A193, XREAL_1:8; hence y < e ; ::_thesis: verum end; A202: y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . n),i))))) * (vol (divset ((T2 . n),i))) by A178, A179, A188, INTEGRA1:def_6; now__::_thesis:_(_i_<>_1_implies_y_<_e_) len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by A183, A186, INTEGRA1:def_6; then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def_6; then A203: i + 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A180, FINSEQ_1:60; then A204: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def_3; A205: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A203, FINSEQ_1:def_3; A206: i in dom D by A180, A187, FINSEQ_1:def_3; Seg ((len D) + 1) = Seg (len E) by A186; then i + 1 in Seg (len E) by A180, A187, FINSEQ_1:60; then A207: i + 1 in dom E by FINSEQ_1:def_3; len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by A183, INTEGRA1:def_6; then A208: dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = dom E by FINSEQ_3:29; assume A209: i <> 1 ; ::_thesis: y < e i in Seg (len D) by A178, A187, FINSEQ_1:def_3; then 1 <= i by FINSEQ_1:1; then A210: 1 < i by A209, XXREAL_0:1; then A211: i - 1 in Seg (len D) by A180, A187, FINSEQ_3:12; then A212: i - 1 in dom D by FINSEQ_1:def_3; reconsider i9 = i - 1 as Element of NAT by A211; 1 + 1 < i + 1 by A210, XREAL_1:8; then A213: i + 1 <> 1 ; divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),i))),(upper_bound (divset ((T2 . n),i))).] by INTEGRA1:4 .= [.(D . (i - 1)),(upper_bound (divset ((T2 . n),i))).] by A209, A206, INTEGRA1:def_4 .= [.(D . (i - 1)),(D . i).] by A209, A206, INTEGRA1:def_4 .= [.(E . (i9 + 1)),(D . i).] by A183, A184, A181, A185, A212, RFINSEQ:def_1 .= [.(E . ((i - 1) + 1)),(E . (i + 1)).] by A183, A184, A181, A185, A206, RFINSEQ:def_1 .= [.(E . ((i + 1) - 1)),(upper_bound (divset ((S2 . n),(i + 1)))).] by A183, A213, A207, INTEGRA1:def_4 .= [.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).] by A183, A213, A207, INTEGRA1:def_4 .= divset ((S2 . n),(i + 1)) by INTEGRA1:4 ; then y = (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . (i + 1) by A202, A183, A204, A208, INTEGRA1:def_6; then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A205, FUNCT_1:def_3; then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def_8; then y < e / 2 by A176, XXREAL_0:2; hence y < e by A175, XXREAL_0:2; ::_thesis: verum end; hence y < e by A189; ::_thesis: verum end; max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) by XXREAL_2:def_8; then ( 0 <= delta (T2 . n) & delta (T2 . n) < e ) by A177, INTEGRA3:9; then abs (delta (T2 . n)) < e by ABSVALUE:def_1; hence abs (((delta T2) . n) - 0) < e by INTEGRA3:def_2; ::_thesis: verum end; hence for n being Element of NAT st m <= n holds abs (((delta T2) . n) - 0) < e ; ::_thesis: verum end; then A214: delta T2 is convergent by SEQ_2:def_6; then A215: lim (delta T2) = 0 by A172, SEQ_2:def_7; then A216: ( upper_sum ((f || ['c,b']),T2) is convergent & lim (upper_sum ((f || ['c,b']),T2)) = upper_integral (f || ['c,b']) ) by A166, A18, A214, INTEGRA4:9; A217: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_(((delta_T)_._m)_-_0)_<_e let e be real number ; ::_thesis: ( 0 < e implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((delta T) . m) - 0) < e ) assume A218: 0 < e ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((delta T) . m) - 0) < e then consider n1 being Element of NAT such that A219: for m being Element of NAT st n1 <= m holds abs (((delta T1) . m) - 0) < e by A53, SEQ_2:def_7; consider n2 being Element of NAT such that A220: for m being Element of NAT st n2 <= m holds abs (((delta T2) . m) - 0) < e by A172, A218; reconsider n = max (n1,n2) as Element of NAT by XXREAL_0:16; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs (((delta T) . m) - 0) < e now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_(((delta_T)_._m)_-_0)_<_e let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((delta T) . m) - 0) < e ) assume A221: n <= m ; ::_thesis: abs (((delta T) . m) - 0) < e n2 <= n by XXREAL_0:25; then n2 <= m by A221, XXREAL_0:2; then abs (((delta T2) . m) - 0) < e by A220; then A222: abs (delta (T2 . m)) < e by INTEGRA3:def_2; 0 <= delta (T2 . m) by INTEGRA3:9; then A223: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) < e by A222, ABSVALUE:def_1; n1 <= n by XXREAL_0:25; then n1 <= m by A221, XXREAL_0:2; then abs (((delta T1) . m) - 0) < e by A219; then A224: abs (delta (T1 . m)) < e by INTEGRA3:def_2; 0 <= delta (T1 . m) by INTEGRA3:9; then A225: max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) < e by A224, ABSVALUE:def_1; A226: for r being real number st r in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) holds r < e proof reconsider Tm = T . m as Division of ['a,b'] ; let y be real number ; ::_thesis: ( y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) implies y < e ) assume y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) ; ::_thesis: y < e then consider x being set such that A227: x in dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) and A228: y = (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) . x by FUNCT_1:def_3; reconsider i = x as Element of NAT by A227; A229: x in Seg (len (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) by A227, FINSEQ_1:def_3; then A230: 1 <= i by FINSEQ_1:1; A231: len (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = len Tm by INTEGRA1:def_6; then A232: i <= len Tm by A229, FINSEQ_1:1; dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = dom Tm by A231, FINSEQ_3:29; then A233: y = (upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((T . m),i))))) * (vol (divset ((T . m),i))) by A227, A228, INTEGRA1:def_6; consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that A234: S1 = T1 . m and A235: S2 = T2 . m and A236: T . m = S1 ^ S2 by A93; A237: len Tm = (len S1) + (len S2) by A236, FINSEQ_1:22; percases ( i <= len S1 or i > len S1 ) ; suppose i <= len S1 ; ::_thesis: y < e then A238: i in Seg (len S1) by A230; then A239: i in dom S1 by FINSEQ_1:def_3; len (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) = len S1 by A234, INTEGRA1:def_6; then A240: i in dom (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A238, FINSEQ_1:def_3; A241: divset ((T1 . m),i) = divset ((T . m),i) by A95, A234, A238; A242: divset ((T1 . m),i) c= ['a,c'] by A139, A234, A238; then divset ((T1 . m),i) c= ['a,b'] by A137, XBOOLE_1:1; then (chi (['a,c'],['a,c'])) | (divset ((T1 . m),i)) = (chi (['a,b'],['a,b'])) | (divset ((T . m),i)) by A241, A242, Th4; then y = (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) . i by A233, A234, A239, A241, INTEGRA1:def_6; then y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A240, FUNCT_1:def_3; then y <= max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) by XXREAL_2:def_8; hence y < e by A225, XXREAL_0:2; ::_thesis: verum end; suppose i > len S1 ; ::_thesis: y < e then A243: (len S1) + 1 <= i by NAT_1:13; then consider k being Nat such that A244: ((len S1) + 1) + k = i by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; set i1 = 1 + k; A245: i - (len S1) <= len S2 by A237, A232, XREAL_1:20; 1 + k = i - (len S1) by A244; then 1 <= 1 + k by A243, XREAL_1:19; then A246: 1 + k in Seg (len S2) by A244, A245; then A247: 1 + k in dom S2 by FINSEQ_1:def_3; A248: divset ((T2 . m),(1 + k)) = divset ((T . m),((len S1) + (1 + k))) by A112, A234, A235, A246; A249: divset ((T2 . m),(1 + k)) c= ['c,b'] by A134, A235, A246; then divset ((T2 . m),(1 + k)) c= ['a,b'] by A17, XBOOLE_1:1; then y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k)))) by A233, A244, A248, A249, Th4; then A250: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) . (1 + k) by A235, A247, INTEGRA1:def_6; len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) = len S2 by A235, INTEGRA1:def_6; then 1 + k in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A246, FINSEQ_1:def_3; then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A250, FUNCT_1:def_3; then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) by XXREAL_2:def_8; hence y < e by A223, XXREAL_0:2; ::_thesis: verum end; end; end; A251: 0 <= delta (T . m) by INTEGRA3:9; max (rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) by XXREAL_2:def_8; then delta (T . m) < e by A226; then abs (delta (T . m)) < e by A251, ABSVALUE:def_1; hence abs (((delta T) . m) - 0) < e by INTEGRA3:def_2; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds abs (((delta T) . m) - 0) < e ; ::_thesis: verum end; then A252: delta T is convergent by SEQ_2:def_6; then A253: lim (delta T) = 0 by A217, SEQ_2:def_7; (f || ['a,b']) | ['a,b'] is bounded by A4; then A254: upper_integral (f || ['a,b']) = lim (upper_sum ((f || ['a,b']),T)) by A12, A252, A253, INTEGRA4:9; A255: for i being Element of NAT holds lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) proof let i be Element of NAT ; ::_thesis: lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) reconsider F = lower_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ; reconsider F1 = lower_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ; reconsider F2 = lower_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ; reconsider S = T . i as Division of ['a,b'] ; consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that A256: S1 = T1 . i and A257: S2 = T2 . i and A258: T . i = S1 ^ S2 by A93; A259: len F = len S by INTEGRA1:def_7 .= (len S1) + (len S2) by A258, FINSEQ_1:22 .= (len F1) + (len S2) by A256, INTEGRA1:def_7 ; then A260: len F = (len F1) + (len F2) by A257, INTEGRA1:def_7; A261: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F2_holds_ F_._((len_F1)_+_k)_=_F2_._k let k be Nat; ::_thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k ) assume k in dom F2 ; ::_thesis: F . ((len F1) + k) = F2 . k then A262: k in Seg (len F2) by FINSEQ_1:def_3; then 1 <= k by FINSEQ_1:1; then A263: 1 + (len F1) <= k + (len F1) by XREAL_1:6; k <= len F2 by A262, FINSEQ_1:1; then A264: (len F1) + k <= len F by A260, XREAL_1:6; 1 <= 1 + (len F1) by NAT_1:11; then 1 <= k + (len F1) by A263, XXREAL_0:2; then k + (len F1) in Seg (len F) by A264; then (len F1) + k in Seg (len S) by INTEGRA1:def_7; then (len F1) + k in dom S by FINSEQ_1:def_3; then A265: F . ((len F1) + k) = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def_7; A266: k in Seg (len S2) by A257, A262, INTEGRA1:def_7; then A267: k in dom S2 by FINSEQ_1:def_3; len F1 = len S1 by A256, INTEGRA1:def_7; then A268: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A256, A257, A266; A269: divset ((T2 . i),k) c= ['c,b'] by A134, A257, A266; then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17, A268, XBOOLE_1:1; then F . ((len F1) + k) = (lower_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A265, A268, A269, Th3; hence F . ((len F1) + k) = F2 . k by A257, A267, INTEGRA1:def_7; ::_thesis: verum end; A270: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_ F_._k_=_F1_._k let k be Nat; ::_thesis: ( k in dom F1 implies F . k = F1 . k ) len (lower_volume ((f || ['a,b']),(T . i))) = len S by INTEGRA1:def_7; then A271: dom (lower_volume ((f || ['a,b']),(T . i))) = dom S by FINSEQ_3:29; assume A272: k in dom F1 ; ::_thesis: F . k = F1 . k then k in Seg (len F1) by FINSEQ_1:def_3; then A273: k in Seg (len S1) by A256, INTEGRA1:def_7; then A274: k in dom S1 by FINSEQ_1:def_3; len F1 <= len F by A259, NAT_1:11; then dom F1 c= dom F by FINSEQ_3:30; then A275: F . k = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by A272, A271, INTEGRA1:def_7; A276: ( divset ((T . i),k) = divset ((T1 . i),k) & divset ((T1 . i),k) c= ['a,c'] ) by A139, A95, A256, A273; then divset ((T . i),k) c= ['a,b'] by A137, XBOOLE_1:1; then F . k = (lower_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A275, A276, Th3; hence F . k = F1 . k by A256, A274, INTEGRA1:def_7; ::_thesis: verum end; dom F = Seg ((len F1) + (len F2)) by A260, FINSEQ_1:def_3; hence lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A270, A261, FINSEQ_1:def_7; ::_thesis: verum end; A277: for i being Element of NAT holds Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) proof let i be Element of NAT ; ::_thesis: Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A255; hence Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_NAT_holds_(lower_sum_((f_||_['a,b']),T))_._i_=_((lower_sum_((f_||_['a,c']),T1))_._i)_+_((lower_sum_((f_||_['c,b']),T2))_._i) let i be Element of NAT ; ::_thesis: (lower_sum ((f || ['a,b']),T)) . i = ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i) thus (lower_sum ((f || ['a,b']),T)) . i = lower_sum ((f || ['a,b']),(T . i)) by INTEGRA2:def_3 .= (lower_sum ((f || ['a,c']),(T1 . i))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) by A277 .= ((lower_sum ((f || ['a,c']),T1)) . i) + (lower_sum ((f || ['c,b']),(T2 . i))) by INTEGRA2:def_3 .= ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def_3 ; ::_thesis: verum end; then A278: lower_sum ((f || ['a,b']),T) = (lower_sum ((f || ['a,c']),T1)) + (lower_sum ((f || ['c,b']),T2)) by SEQ_1:7; A279: f || ['a,c'] is Function of ['a,c'],REAL by A2, A137, Lm1, XBOOLE_1:1; then A280: ( f || ['a,c'] is upper_integrable & f || ['a,c'] is lower_integrable ) by A138, INTEGRA4:10; A281: ( upper_sum ((f || ['a,c']),T1) is convergent & lim (upper_sum ((f || ['a,c']),T1)) = upper_integral (f || ['a,c']) ) by A279, A138, A53, INTEGRA4:9; then A282: (upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b']) by A165, A216, A254, SEQ_2:6; A283: ( lower_sum ((f || ['a,c']),T1) is convergent & lim (lower_sum ((f || ['a,c']),T1)) = lower_integral (f || ['a,c']) ) by A279, A138, A53, INTEGRA4:8; (f || ['a,b']) | ['a,b'] is bounded by A4; then A284: lower_integral (f || ['a,b']) = lim (lower_sum ((f || ['a,b']),T)) by A12, A252, A253, INTEGRA4:8; ( lower_sum ((f || ['c,b']),T2) is convergent & lim (lower_sum ((f || ['c,b']),T2)) = lower_integral (f || ['c,b']) ) by A166, A18, A214, A215, INTEGRA4:8; then A285: (lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b']) by A278, A283, A284, SEQ_2:6; integral (f,a,b) = integral (f,['a,b']) by A1, INTEGRA5:def_4 .= (integral (f || ['a,c'])) + (integral (f || ['c,b'])) by A165, A281, A216, A254, SEQ_2:6 ; hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A58, A57; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) f || ['a,b'] is integrable by A3, INTEGRA5:def_1; then A286: upper_integral (f || ['a,b']) = lower_integral (f || ['a,b']) by INTEGRA1:def_16; A287: ( f || ['c,b'] is upper_integrable & f || ['c,b'] is lower_integrable ) by A166, A18, INTEGRA4:10; A288: lower_integral (f || ['a,c']) <= upper_integral (f || ['a,c']) by A279, A138, INTEGRA1:49; then lower_integral (f || ['c,b']) = upper_integral (f || ['c,b']) by A286, A282, A285, A167, Th1; then A289: f || ['c,b'] is integrable by A287, INTEGRA1:def_16; lower_integral (f || ['a,c']) = upper_integral (f || ['a,c']) by A286, A282, A285, A288, A167, Th1; then f || ['a,c'] is integrable by A280, INTEGRA1:def_16; hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) by A289, INTEGRA5:def_1; ::_thesis: verum end; theorem Th17: :: INTEGRA6:17 for a, b, c being real number for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] holds ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) proof let a, b, c be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] holds ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] implies ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) ) assume that A1: a <= b and A2: f is_integrable_on ['a,b'] and A3: ( f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) ; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) now__::_thesis:_(_b_=_c_implies_(_f_is_integrable_on_['a,c']_&_f_is_integrable_on_['c,b']_&_integral_(f,a,b)_=_(integral_(f,a,c))_+_(integral_(f,c,b))_)_) assume A4: b = c ; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) then A5: ['c,b'] = [.c,b.] by INTEGRA5:def_3; thus f is_integrable_on ['a,c'] by A2, A4; ::_thesis: ( f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) ['c,b'] = [.(lower_bound ['c,b']),(upper_bound ['c,b']).] by INTEGRA1:4; then ( lower_bound ['c,b'] = c & upper_bound ['c,b'] = b ) by A5, INTEGRA1:5; then A6: vol ['c,b'] = 0 by A4; then f || ['c,b'] is integrable by INTEGRA4:6; hence f is_integrable_on ['c,b'] by INTEGRA5:def_1; ::_thesis: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ( c is Real & b is Real ) by XREAL_0:def_1; then integral (f,c,b) = integral (f,['c,b']) by A5, INTEGRA5:19; then integral (f,c,b) = 0 by A6, INTEGRA4:6; hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A4; ::_thesis: verum end; hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) by A1, A2, A3, Lm2; ::_thesis: verum end; Lm3: for a, b, c being real number st a <= c & c <= b holds ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) proof let a, b, c be real number ; ::_thesis: ( a <= c & c <= b implies ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) ) assume that A1: a <= c and A2: c <= b ; ::_thesis: ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) A3: c in [.a,b.] by A1, A2, XXREAL_1:1; hence c in ['a,b'] by A1, A2, INTEGRA5:def_3, XXREAL_0:2; ::_thesis: ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) A4: ['c,b'] = [.c,b.] by A2, INTEGRA5:def_3; a <= b by A1, A2, XXREAL_0:2; then A5: ( a in [.a,b.] & b in [.a,b.] ) by XXREAL_1:1; ( ['a,b'] = [.a,b.] & ['a,c'] = [.a,c.] ) by A1, A2, INTEGRA5:def_3, XXREAL_0:2; hence ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) by A4, A3, A5, XXREAL_2:def_12; ::_thesis: verum end; theorem Th18: :: INTEGRA6:18 for a, c, d, b being real number for f being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) proof let a, c, d, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) ) assume that A1: a <= c and A2: c <= d and A3: d <= b and A4: f is_integrable_on ['a,b'] and A5: f | ['a,b'] is bounded and A6: ['a,b'] c= dom f ; ::_thesis: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) a <= d by A1, A2, XXREAL_0:2; then A7: a <= b by A3, XXREAL_0:2; A8: c <= b by A2, A3, XXREAL_0:2; then c in ['a,b'] by A1, Lm3; then A9: f is_integrable_on ['c,b'] by A4, A5, A6, A7, Th17; A10: d in ['c,b'] by A2, A3, Lm3; A11: ['c,b'] c= ['a,b'] by A1, A8, Lm3; then ( ['c,b'] c= dom f & f | ['c,b'] is bounded ) by A5, A6, RFUNCT_1:74, XBOOLE_1:1; hence f is_integrable_on ['c,d'] by A8, A10, A9, Th17; ::_thesis: ( f | ['c,d'] is bounded & ['c,d'] c= dom f ) ['c,d'] c= ['c,b'] by A2, A3, Lm3; then A12: ['c,d'] c= ['a,b'] by A11, XBOOLE_1:1; hence f | ['c,d'] is bounded by A5, RFUNCT_1:74; ::_thesis: ['c,d'] c= dom f thus ['c,d'] c= dom f by A6, A12, XBOOLE_1:1; ::_thesis: verum end; theorem :: INTEGRA6:19 for a, c, d, b being real number for f, g being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded ) proof let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded ) let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded ) ) assume that A1: a <= c and A2: ( c <= d & d <= b ) and A3: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) and A4: ['a,b'] c= dom f and A5: ['a,b'] c= dom g ; ::_thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded ) A6: ['c,d'] c= ['c,b'] by A2, Lm3; A7: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A1, A2, A3, A4, A5, Th18; c <= b by A2, XXREAL_0:2; then A8: ['c,b'] c= ['a,b'] by A1, Lm3; then ['c,b'] c= dom f by A4, XBOOLE_1:1; then A9: ['c,d'] c= dom f by A6, XBOOLE_1:1; ['c,b'] c= dom g by A5, A8, XBOOLE_1:1; then A10: ['c,d'] c= dom g by A6, XBOOLE_1:1; ( f is_integrable_on ['c,d'] & g is_integrable_on ['c,d'] ) by A1, A2, A3, A4, A5, Th18; hence f + g is_integrable_on ['c,d'] by A7, A9, A10, Th11; ::_thesis: (f + g) | ['c,d'] is bounded (f + g) | (['c,d'] /\ ['c,d']) is bounded by A7, RFUNCT_1:83; hence (f + g) | ['c,d'] is bounded ; ::_thesis: verum end; Lm4: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) proof let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) and A4: ['a,b'] c= dom f and A5: c in ['a,b'] and A6: d in ['a,b'] ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) A7: f is_integrable_on ['a,d'] by A1, A3, A4, A6, Th17; A8: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A9: a <= d by A6, XXREAL_1:1; A10: d <= b by A6, A8, XXREAL_1:1; then ['a,d'] c= ['a,b'] by A9, Lm3; then A11: ['a,d'] c= dom f by A4, XBOOLE_1:1; a <= c by A5, A8, XXREAL_1:1; then A12: c in ['a,d'] by A2, Lm3; f | ['a,d'] is bounded by A3, A4, A9, A10, Th18; hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A9, A12, A11, A7, Th17; ::_thesis: verum end; theorem Th20: :: INTEGRA6:20 for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) proof let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) now__::_thesis:_(_not_c_<=_d_implies_integral_(f,a,d)_=_(integral_(f,a,c))_+_(integral_(f,c,d))_) assume A2: not c <= d ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) then integral (f,a,c) = (integral (f,a,d)) + (integral (f,d,c)) by A1, Lm4; then A3: integral (f,a,d) = (integral (f,a,c)) - (integral (f,d,c)) ; integral (f,c,d) = - (integral (f,['d,c'])) by A2, INTEGRA5:def_4; hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A2, A3, INTEGRA5:def_4; ::_thesis: verum end; hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A1, Lm4; ::_thesis: verum end; Lm5: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) proof let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) and A4: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A5: ( a <= c & d <= b ) by A4, XXREAL_1:1; then A6: f | ['c,d'] is bounded by A2, A3, Th18; ( ['c,d'] c= dom f & f is_integrable_on ['c,d'] ) by A2, A3, A5, Th18; hence ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) by A2, A6, Th7, Th8, RFUNCT_1:82, VALUED_1:def_11; ::_thesis: verum end; theorem Th21: :: INTEGRA6:21 for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) proof let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) A2: now__::_thesis:_(_not_c_<=_d_implies_(_['(min_(c,d)),(max_(c,d))']_c=_dom_(abs_f)_&_abs_f_is_integrable_on_['(min_(c,d)),(max_(c,d))']_&_(abs_f)_|_['(min_(c,d)),(max_(c,d))']_is_bounded_&_abs_(integral_(f,c,d))_<=_integral_((abs_f),(min_(c,d)),(max_(c,d)))_)_) assume A3: not c <= d ; ::_thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) then integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def_4; then integral (f,c,d) = - (integral (f,d,c)) by A3, INTEGRA5:def_4; then A4: abs (integral (f,c,d)) = abs (integral (f,d,c)) by COMPLEX1:52; ( d = min (c,d) & c = max (c,d) ) by A3, XXREAL_0:def_9, XXREAL_0:def_10; hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A3, A4, Lm5; ::_thesis: verum end; now__::_thesis:_(_c_<=_d_implies_(_['(min_(c,d)),(max_(c,d))']_c=_dom_(abs_f)_&_abs_f_is_integrable_on_['(min_(c,d)),(max_(c,d))']_&_(abs_f)_|_['(min_(c,d)),(max_(c,d))']_is_bounded_&_abs_(integral_(f,c,d))_<=_integral_((abs_f),(min_(c,d)),(max_(c,d)))_)_) assume A5: c <= d ; ::_thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) then ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10; hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A5, Lm5; ::_thesis: verum end; hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A2; ::_thesis: verum end; Lm6: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) proof let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) ( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10; hence ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) by A1, A3, Th21; ::_thesis: verum end; Lm7: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds abs (integral (f,d,c)) <= integral ((abs f),c,d) proof let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds abs (integral (f,d,c)) <= integral ((abs f),c,d) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies abs (integral (f,d,c)) <= integral ((abs f),c,d) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and A4: d in ['a,b'] ; ::_thesis: abs (integral (f,d,c)) <= integral ((abs f),c,d) A5: ( abs (integral (f,c,d)) <= integral ((abs f),c,d) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, Lm6, INTEGRA5:def_4; percases ( c = d or c <> d ) ; suppose c = d ; ::_thesis: abs (integral (f,d,c)) <= integral ((abs f),c,d) hence abs (integral (f,d,c)) <= integral ((abs f),c,d) by A1, A3, Lm6; ::_thesis: verum end; suppose c <> d ; ::_thesis: abs (integral (f,d,c)) <= integral ((abs f),c,d) then c < d by A2, XXREAL_0:1; then integral (f,d,c) = - (integral (f,['c,d'])) by INTEGRA5:def_4; hence abs (integral (f,d,c)) <= integral ((abs f),c,d) by A5, COMPLEX1:52; ::_thesis: verum end; end; end; theorem :: INTEGRA6:22 for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) & abs (integral (f,d,c)) <= integral ((abs f),c,d) ) by Lm6, Lm7; Lm8: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ) holds abs (integral (f,c,d)) <= e * (abs (d - c)) proof let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ) holds abs (integral (f,c,d)) <= e * (abs (d - c)) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ) implies abs (integral (f,c,d)) <= e * (abs (d - c)) ) set A = ['(min (c,d)),(max (c,d))']; assume that A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) and A2: for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ; ::_thesis: abs (integral (f,c,d)) <= e * (abs (d - c)) rng (abs f) c= REAL ; then A3: abs f is Function of (dom (abs f)),REAL by FUNCT_2:2; ['(min (c,d)),(max (c,d))'] c= dom (abs f) by A1, Th21; then reconsider g = (abs f) || ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32; A4: vol ['(min (c,d)),(max (c,d))'] = abs (d - c) by Th6; abs f is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, Th21; then A5: g is integrable by INTEGRA5:def_1; reconsider e = e as Real by XREAL_0:def_1; consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that A6: rng h = {e} and A7: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5; A8: now__::_thesis:_for_x_being_Real_st_x_in_['(min_(c,d)),(max_(c,d))']_holds_ g_._x_<=_h_._x let x be Real; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x ) assume A9: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: g . x <= h . x then g . x = (abs f) . x by FUNCT_1:49; then A10: g . x = abs (f . x) by VALUED_1:18; h . x in {e} by A6, A9, FUNCT_2:4; then h . x = e by TARSKI:def_1; hence g . x <= h . x by A2, A9, A10; ::_thesis: verum end; A11: abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) by A1, Th21; ( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25; then min (c,d) <= max (c,d) by XXREAL_0:2; then A12: integral ((abs f),(min (c,d)),(max (c,d))) = integral ((abs f),['(min (c,d)),(max (c,d))']) by INTEGRA5:def_4; (abs f) | ['(min (c,d)),(max (c,d))'] is bounded by A1, Th21; then A13: g | ['(min (c,d)),(max (c,d))'] is bounded ; ( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by A6, INTEGRA4:4; then integral ((abs f),(min (c,d)),(max (c,d))) <= e * (abs (d - c)) by A12, A7, A8, A5, A13, A4, INTEGRA2:34; hence abs (integral (f,c,d)) <= e * (abs (d - c)) by A11, XXREAL_0:2; ::_thesis: verum end; Lm9: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) holds abs (integral (f,c,d)) <= e * (d - c) proof let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) holds abs (integral (f,c,d)) <= e * (d - c) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) implies abs (integral (f,c,d)) <= e * (d - c) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) ) ; ::_thesis: abs (integral (f,c,d)) <= e * (d - c) 0 <= d - c by A2, XREAL_1:48; then A4: abs (d - c) = d - c by ABSVALUE:def_1; ( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10; hence abs (integral (f,c,d)) <= e * (d - c) by A1, A3, A4, Lm8; ::_thesis: verum end; Lm10: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) holds abs (integral (f,d,c)) <= e * (d - c) proof let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) holds abs (integral (f,d,c)) <= e * (d - c) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) implies abs (integral (f,d,c)) <= e * (d - c) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and A4: d in ['a,b'] and A5: for x being real number st x in ['c,d'] holds abs (f . x) <= e ; ::_thesis: abs (integral (f,d,c)) <= e * (d - c) A6: ( abs (integral (f,c,d)) <= e * (d - c) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, A5, Lm9, INTEGRA5:def_4; percases ( c = d or c <> d ) ; suppose c = d ; ::_thesis: abs (integral (f,d,c)) <= e * (d - c) hence abs (integral (f,d,c)) <= e * (d - c) by A1, A3, A5, Lm9; ::_thesis: verum end; suppose c <> d ; ::_thesis: abs (integral (f,d,c)) <= e * (d - c) then c < d by A2, XXREAL_0:1; then integral (f,d,c) = - (integral (f,['c,d'])) by INTEGRA5:def_4; hence abs (integral (f,d,c)) <= e * (d - c) by A6, COMPLEX1:52; ::_thesis: verum end; end; end; theorem :: INTEGRA6:23 for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds abs (f . x) <= e ) holds ( abs (integral (f,c,d)) <= e * (d - c) & abs (integral (f,d,c)) <= e * (d - c) ) by Lm9, Lm10; Lm11: for a, b, c, d being real number for f, g being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) proof let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) ) assume that A1: a <= b and A2: c <= d and A3: f is_integrable_on ['a,b'] and A4: g is_integrable_on ['a,b'] and A5: f | ['a,b'] is bounded and A6: g | ['a,b'] is bounded and A7: ['a,b'] c= dom f and A8: ['a,b'] c= dom g and A9: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A10: ( a <= c & d <= b ) by A9, XXREAL_1:1; then A11: ( f is_integrable_on ['c,d'] & ['c,d'] c= dom f ) by A2, A3, A5, A7, Th18; A12: ( g is_integrable_on ['c,d'] & ['c,d'] c= dom g ) by A2, A4, A6, A8, A10, Th18; A13: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A2, A3, A4, A5, A6, A7, A8, A10, Th18; then (f + g) | (['c,d'] /\ ['c,d']) is bounded by RFUNCT_1:83; hence ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) by A2, A11, A13, A12, Th11, Th12, RFUNCT_1:84; ::_thesis: verum end; theorem Th24: :: INTEGRA6:24 for a, b, c, d being real number for f, g being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) proof let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) now__::_thesis:_(_not_c_<=_d_implies_(_integral_((f_+_g),c,d)_=_(integral_(f,c,d))_+_(integral_(g,c,d))_&_integral_((f_-_g),c,d)_=_(integral_(f,c,d))_-_(integral_(g,c,d))_)_) assume A2: not c <= d ; ::_thesis: ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) then A3: integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def_4; A4: integral (g,c,d) = - (integral (g,['d,c'])) by A2, INTEGRA5:def_4; integral ((f + g),c,d) = - (integral ((f + g),['d,c'])) by A2, INTEGRA5:def_4; hence integral ((f + g),c,d) = - (integral ((f + g),d,c)) by A2, INTEGRA5:def_4 .= - ((integral (f,d,c)) + (integral (g,d,c))) by A1, A2, Lm11 .= (- (integral (f,d,c))) - (integral (g,d,c)) .= (integral (f,c,d)) - (integral (g,d,c)) by A2, A3, INTEGRA5:def_4 .= (integral (f,c,d)) + (integral (g,c,d)) by A2, A4, INTEGRA5:def_4 ; ::_thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) integral ((f - g),c,d) = - (integral ((f - g),['d,c'])) by A2, INTEGRA5:def_4; hence integral ((f - g),c,d) = - (integral ((f - g),d,c)) by A2, INTEGRA5:def_4 .= - ((integral (f,d,c)) - (integral (g,d,c))) by A1, A2, Lm11 .= - ((integral (f,d,c)) + (integral (g,c,d))) by A2, A4, INTEGRA5:def_4 .= (- (integral (f,d,c))) - (integral (g,c,d)) .= (integral (f,c,d)) - (integral (g,c,d)) by A2, A3, INTEGRA5:def_4 ; ::_thesis: verum end; hence ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) by A1, Lm11; ::_thesis: verum end; Lm12: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((e (#) f),c,d) = e * (integral (f,c,d)) proof let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((e (#) f),c,d) = e * (integral (f,c,d)) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((e (#) f),c,d) = e * (integral (f,c,d)) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) and A4: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((e (#) f),c,d) = e * (integral (f,c,d)) ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A5: ( a <= c & d <= b ) by A4, XXREAL_1:1; then A6: ['c,d'] c= dom f by A2, A3, Th18; ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) by A2, A3, A5, Th18; hence integral ((e (#) f),c,d) = e * (integral (f,c,d)) by A2, A6, Th10; ::_thesis: verum end; theorem :: INTEGRA6:25 for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((e (#) f),c,d) = e * (integral (f,c,d)) proof let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((e (#) f),c,d) = e * (integral (f,c,d)) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((e (#) f),c,d) = e * (integral (f,c,d)) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((e (#) f),c,d) = e * (integral (f,c,d)) now__::_thesis:_(_not_c_<=_d_implies_integral_((e_(#)_f),c,d)_=_e_*_(integral_(f,c,d))_) assume A2: not c <= d ; ::_thesis: integral ((e (#) f),c,d) = e * (integral (f,c,d)) then A3: integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def_4; thus integral ((e (#) f),c,d) = - (integral ((e (#) f),['d,c'])) by A2, INTEGRA5:def_4 .= - (integral ((e (#) f),d,c)) by A2, INTEGRA5:def_4 .= - (e * (integral (f,d,c))) by A1, A2, Lm12 .= e * (- (integral (f,d,c))) .= e * (integral (f,c,d)) by A2, A3, INTEGRA5:def_4 ; ::_thesis: verum end; hence integral ((e (#) f),c,d) = e * (integral (f,c,d)) by A1, Lm12; ::_thesis: verum end; theorem Th26: :: INTEGRA6:26 for a, b, e being real number for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = e ) holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) ) proof let a, b, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = e ) holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = e ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) ) ) assume that A1: a <= b and A2: ['a,b'] c= dom f and A3: for x being real number st x in ['a,b'] holds f . x = e ; ::_thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) ) rng f c= REAL ; then f is Function of (dom f),REAL by FUNCT_2:2; then reconsider g = f || ['a,b'] as Function of ['a,b'],REAL by A2, FUNCT_2:32; reconsider e1 = e as Real by XREAL_0:def_1; consider h being Function of ['a,b'],REAL such that A4: rng h = {e1} and A5: h | ['a,b'] is bounded by INTEGRA4:5; integral h = e1 * (vol ['a,b']) by A4, INTEGRA4:4; then A6: integral h = e * (b - a) by A1, Th5; A7: for x being set st x in ['a,b'] holds g . x = h . x proof let x0 be set ; ::_thesis: ( x0 in ['a,b'] implies g . x0 = h . x0 ) assume A8: x0 in ['a,b'] ; ::_thesis: g . x0 = h . x0 then reconsider x = x0 as real number ; g . x0 = f . x by A8, FUNCT_1:49; then A9: g . x0 = e by A3, A8; h . x in {e1} by A4, A8, FUNCT_2:4; hence g . x0 = h . x0 by A9, TARSKI:def_1; ::_thesis: verum end; then A10: h = g by FUNCT_2:12; h is integrable by A4, INTEGRA4:4; hence f is_integrable_on ['a,b'] by A10, INTEGRA5:def_1; ::_thesis: ( f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) ) thus f | ['a,b'] is bounded ::_thesis: integral (f,a,b) = e * (b - a) proof consider r being real number such that A11: for c being set st c in ['a,b'] /\ (dom g) holds abs (g . c) <= r by A5, A10, RFUNCT_1:73; now__::_thesis:_for_c_being_set_st_c_in_['a,b']_/\_(dom_f)_holds_ abs_(f_._c)_<=_r let c be set ; ::_thesis: ( c in ['a,b'] /\ (dom f) implies abs (f . c) <= r ) ['a,b'] /\ (dom g) = ['a,b'] /\ ((dom f) /\ ['a,b']) by RELAT_1:61; then A12: ['a,b'] /\ (dom g) = (['a,b'] /\ ['a,b']) /\ (dom f) by XBOOLE_1:16; assume c in ['a,b'] /\ (dom f) ; ::_thesis: abs (f . c) <= r then ( abs (g . c) <= r & c in dom g ) by A11, A12, XBOOLE_0:def_4; hence abs (f . c) <= r by FUNCT_1:47; ::_thesis: verum end; hence f | ['a,b'] is bounded by RFUNCT_1:73; ::_thesis: verum end; integral (f,a,b) = integral (f,['a,b']) by A1, INTEGRA5:def_4; hence integral (f,a,b) = e * (b - a) by A7, A6, FUNCT_2:12; ::_thesis: verum end; theorem Th27: :: INTEGRA6:27 for a, b, e, c, d being real number for f being PartFunc of REAL,REAL st a <= b & ( for x being real number st x in ['a,b'] holds f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = e * (d - c) proof let a, b, e, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ( for x being real number st x in ['a,b'] holds f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = e * (d - c) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ( for x being real number st x in ['a,b'] holds f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = e * (d - c) ) assume that A1: a <= b and A2: for x being real number st x in ['a,b'] holds f . x = e and A3: ['a,b'] c= dom f and A4: c in ['a,b'] and A5: d in ['a,b'] ; ::_thesis: integral (f,c,d) = e * (d - c) A6: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A2, A3, Th26; A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A8: c <= b by A4, XXREAL_1:1; A9: a <= c by A4, A7, XXREAL_1:1; then A10: ['c,b'] c= ['a,b'] by A8, Lm3; A11: d <= b by A5, A7, XXREAL_1:1; A12: a <= d by A5, A7, XXREAL_1:1; A13: ['a,c'] c= ['a,b'] by A9, A8, Lm3; percases ( c <= d or not c <= d ) ; supposeA14: c <= d ; ::_thesis: integral (f,c,d) = e * (d - c) then ['c,d'] c= ['c,b'] by A11, Lm3; then ['c,d'] c= ['a,b'] by A10, XBOOLE_1:1; then A15: for x being real number st x in ['c,d'] holds f . x = e by A2; ['c,d'] c= dom f by A3, A9, A11, A6, A14, Th18; hence integral (f,c,d) = e * (d - c) by A14, A15, Th26; ::_thesis: verum end; supposeA16: not c <= d ; ::_thesis: integral (f,c,d) = e * (d - c) then ['d,c'] c= ['a,c'] by A12, Lm3; then ['d,c'] c= ['a,b'] by A13, XBOOLE_1:1; then A17: for x being real number st x in ['d,c'] holds f . x = e by A2; integral (f,c,d) = - (integral (f,['d,c'])) by A16, INTEGRA5:def_4; then A18: integral (f,c,d) = - (integral (f,d,c)) by A16, INTEGRA5:def_4; ['d,c'] c= dom f by A3, A12, A8, A6, A16, Th18; then integral (f,d,c) = e * (c - d) by A16, A17, Th26; hence integral (f,c,d) = e * (d - c) by A18; ::_thesis: verum end; end; end; begin theorem Th28: :: INTEGRA6:28 for a, b being real number for f being PartFunc of REAL,REAL for x0 being real number for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) proof let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL for x0 being real number for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) let f be PartFunc of REAL,REAL; ::_thesis: for x0 being real number for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) deffunc H1( set ) -> Element of NAT = 0 ; let x0 be real number ; ::_thesis: for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) let F be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 implies ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) ) assume that A1: a <= b and A2: f is_integrable_on ['a,b'] and A3: f | ['a,b'] is bounded and A4: ['a,b'] c= dom f and A5: ].a,b.[ c= dom F and A6: for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) and A7: x0 in ].a,b.[ and A8: f is_continuous_in x0 ; ::_thesis: ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) defpred S1[ set ] means x0 + (R_id $1) in ].a,b.[; deffunc H2( Element of REAL ) -> Element of REAL = (f . x0) * $1; consider L being Function of REAL,REAL such that A9: for h being Real holds L . h = H2(h) from FUNCT_2:sch_4(); reconsider L = L as PartFunc of REAL,REAL ; deffunc H3( set ) -> Element of REAL = ((F . (x0 + (R_id $1))) - (F . x0)) - (L . (R_id $1)); reconsider L = L as LinearFunc by A9, FDIFF_1:def_3; consider R being Function such that A10: ( dom R = REAL & ( for x being set st x in REAL holds ( ( S1[x] implies R . x = H3(x) ) & ( not S1[x] implies R . x = H1(x) ) ) ) ) from PARTFUN1:sch_1(); rng R c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng R or y in REAL ) assume y in rng R ; ::_thesis: y in REAL then consider x being set such that A11: x in dom R and A12: y = R . x by FUNCT_1:def_3; A13: ( not S1[x] implies R . x = H1(x) ) by A10, A11; ( S1[x] implies R . x = H3(x) ) by A10, A11; hence y in REAL by A12, A13; ::_thesis: verum end; then reconsider R = R as PartFunc of REAL,REAL by A10, RELSET_1:4; A14: R is total by A10, PARTFUN1:def_2; A15: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; A16: for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) proof let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) A17: for e being real number st 0 < e holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((h ") (#) (R /* h)) . m) - 0) < e proof set g = REAL --> (f . x0); let e0 be real number ; ::_thesis: ( 0 < e0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((h ") (#) (R /* h)) . m) - 0) < e0 ) set e = e0 / 2; A18: ( h is convergent & lim h = 0 ) ; assume A19: 0 < e0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((h ") (#) (R /* h)) . m) - 0) < e0 then 0 < e0 / 2 by XREAL_1:215; then consider p being real number such that A20: 0 < p and A21: for t being real number st t in dom f & abs (t - x0) < p holds abs ((f . t) - (f . x0)) < e0 / 2 by A8, FCONT_1:3; A22: 0 < p / 2 by A20, XREAL_1:215; A23: p / 2 < p by A20, XREAL_1:216; consider N being Neighbourhood of x0 such that A24: N c= ].a,b.[ by A7, RCOMP_1:18; consider q being real number such that A25: 0 < q and A26: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def_6; A27: q / 2 < q by A25, XREAL_1:216; set r = min ((p / 2),(q / 2)); 0 < q / 2 by A25, XREAL_1:215; then 0 < min ((p / 2),(q / 2)) by A22, XXREAL_0:15; then consider n being Element of NAT such that A28: for m being Element of NAT st n <= m holds abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A18, SEQ_2:def_7; take n ; ::_thesis: for m being Element of NAT st n <= m holds abs ((((h ") (#) (R /* h)) . m) - 0) < e0 let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((((h ") (#) (R /* h)) . m) - 0) < e0 ) min ((p / 2),(q / 2)) <= q / 2 by XXREAL_0:17; then A29: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A27, Th2, XXREAL_0:2; assume n <= m ; ::_thesis: abs ((((h ") (#) (R /* h)) . m) - 0) < e0 then A30: abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A28; then abs ((x0 + (h . m)) - x0) < min ((p / 2),(q / 2)) ; then x0 + (h . m) in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1; then A31: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A29; then A32: x0 + (h . m) in ].a,b.[ by A24, A26; then x0 + (R_id (h . m)) in ].a,b.[ by RSSPACE:def_3; then R . (h . m) = ((F . (x0 + (R_id (h . m)))) - (F . x0)) - (L . (R_id (h . m))) by A10; then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (R_id (h . m))) by RSSPACE:def_3; then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (h . m)) by RSSPACE:def_3; then A33: R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - ((f . x0) * (h . m)) by A9; F . (x0 + (h . m)) = integral (f,a,(x0 + (h . m))) by A6, A24, A26, A31; then A34: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((f . x0) * (h . m)) by A6, A7, A33; A35: dom (REAL --> (f . x0)) = REAL by FUNCT_2:def_1; then ['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> (f . x0))) by A4, XBOOLE_1:27; then A36: ['a,b'] c= dom (f - (REAL --> (f . x0))) by VALUED_1:12; A37: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A38: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A15, A32, Th20; A39: min ((p / 2),(q / 2)) <= p / 2 by XXREAL_0:17; A40: for x being real number st x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] holds abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 proof let x be real number ; ::_thesis: ( x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] implies abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 ) reconsider x1 = x as Real by XREAL_0:def_1; A41: ( min (x0,(x0 + (h . m))) <= x0 & x0 <= max (x0,(x0 + (h . m))) ) by XXREAL_0:17, XXREAL_0:25; assume x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] ; ::_thesis: abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 then A42: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A41, INTEGRA5:def_3, XXREAL_0:2; abs (x - x0) <= abs (h . m) proof percases ( x0 <= x0 + (h . m) or not x0 <= x0 + (h . m) ) ; suppose x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m) then ( x0 = min (x0,(x0 + (h . m))) & x0 + (h . m) = max (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10; then x in { z where z is Real : ( x0 <= z & z <= x0 + (h . m) ) } by A42, RCOMP_1:def_1; then A43: ex z being Real st ( x = z & x0 <= z & z <= x0 + (h . m) ) ; then 0 <= x - x0 by XREAL_1:48; then A44: abs (x - x0) = x - x0 by ABSVALUE:def_1; A45: x - x0 <= (x0 + (h . m)) - x0 by A43, XREAL_1:9; then 0 <= h . m by A43, XREAL_1:48; hence abs (x - x0) <= abs (h . m) by A45, A44, ABSVALUE:def_1; ::_thesis: verum end; supposeA46: not x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m) then ( x0 = max (x0,(x0 + (h . m))) & x0 + (h . m) = min (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10; then x in { z where z is Real : ( x0 + (h . m) <= z & z <= x0 ) } by A42, RCOMP_1:def_1; then A47: ex z being Real st ( x = z & x0 + (h . m) <= z & z <= x0 ) ; then A48: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:9; percases ( x - x0 <> 0 or x - x0 = 0 ) ; supposeA49: x - x0 <> 0 ; ::_thesis: abs (x - x0) <= abs (h . m) (x0 + (h . m)) - x0 < x0 - x0 by A46, XREAL_1:14; then A50: abs (h . m) = - (h . m) by ABSVALUE:def_1; x - x0 < 0 by A47, A49, XREAL_1:47; then abs (x - x0) = - (x - x0) by ABSVALUE:def_1; hence abs (x - x0) <= abs (h . m) by A48, A50, XREAL_1:24; ::_thesis: verum end; suppose x - x0 = 0 ; ::_thesis: abs (x - x0) <= abs (h . m) then abs (x - x0) = 0 by ABSVALUE:def_1; hence abs (x - x0) <= abs (h . m) by COMPLEX1:46; ::_thesis: verum end; end; end; end; end; then A51: abs (x - x0) < min ((p / 2),(q / 2)) by A30, XXREAL_0:2; then x in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1; then x in ].(x0 - q),(x0 + q).[ by A29; then x in ].a,b.[ by A24, A26; then A52: x in [.a,b.] by A37; abs (x - x0) < p / 2 by A39, A51, XXREAL_0:2; then abs (x - x0) < p by A23, XXREAL_0:2; then abs ((f . x) - (f . x0)) <= e0 / 2 by A4, A15, A21, A52; then abs ((f . x1) - ((REAL --> (f . x0)) . x1)) <= e0 / 2 by FUNCOP_1:7; hence abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 by A15, A36, A52, VALUED_1:13; ::_thesis: verum end; A53: for x being real number st x in ['a,b'] holds (REAL --> (f . x0)) . x = f . x0 by FUNCOP_1:7; then A54: (REAL --> (f . x0)) | ['a,b'] is bounded by A1, A35, Th26; then A55: (f - (REAL --> (f . x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, RFUNCT_1:84; rng h c= dom R by A10; then (R . (h . m)) / (h . m) = ((R /* h) . m) / (h . m) by FUNCT_2:108; then (R . (h . m)) / (h . m) = ((R /* h) . m) * ((h ") . m) by VALUED_1:10; then A56: (R . (h . m)) / (h . m) = ((h ") (#) (R /* h)) . m by SEQ_1:8; h . m <> 0 by SEQ_1:4; then A57: 0 < abs (h . m) by COMPLEX1:47; A58: REAL --> (f . x0) is_integrable_on ['a,b'] by A1, A35, A53, Th26; then f - (REAL --> (f . x0)) is_integrable_on ['a,b'] by A2, A3, A4, A35, A54, Th11; then A59: abs (integral ((f - (REAL --> (f . x0))),x0,(x0 + (h . m)))) <= (e0 / 2) * (abs ((x0 + (h . m)) - x0)) by A1, A7, A15, A37, A32, A55, A36, A40, Lm8; integral ((REAL --> (f . x0)),x0,(x0 + (h . m))) = (f . x0) * ((x0 + (h . m)) - x0) by A1, A7, A15, A37, A32, A35, A53, Th27; then R . (h . m) = integral ((f - (REAL --> (f . x0))),x0,(x0 + (h . m))) by A1, A2, A3, A4, A7, A15, A37, A32, A34, A35, A58, A54, A38, Th24; then ( abs ((R . (h . m)) / (h . m)) = (abs (R . (h . m))) / (abs (h . m)) & (abs (R . (h . m))) / (abs (h . m)) <= ((e0 / 2) * (abs (h . m))) / (abs (h . m)) ) by A59, A57, COMPLEX1:67, XREAL_1:72; then A60: abs ((R . (h . m)) / (h . m)) <= e0 / 2 by A57, XCMPLX_1:89; e0 / 2 < e0 by A19, XREAL_1:216; hence abs ((((h ") (#) (R /* h)) . m) - 0) < e0 by A60, A56, XXREAL_0:2; ::_thesis: verum end; hence (h ") (#) (R /* h) is convergent by SEQ_2:def_6; ::_thesis: lim ((h ") (#) (R /* h)) = 0 hence lim ((h ") (#) (R /* h)) = 0 by A17, SEQ_2:def_7; ::_thesis: verum end; consider N being Neighbourhood of x0 such that A61: N c= ].a,b.[ by A7, RCOMP_1:18; reconsider R = R as RestFunc by A14, A16, FDIFF_1:def_2; A62: for x being Real st x in N holds (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) ) assume x in N ; ::_thesis: (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) then x0 + (x - x0) in N ; then x0 + (R_id (x - x0)) in N by RSSPACE:def_3; then ( x0 + (R_id (x - x0)) = x0 + (x - x0) & R . (x - x0) = H3(x - x0) ) by A10, A61, RSSPACE:def_3; hence (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) ; ::_thesis: verum end; A63: N c= dom F by A5, A61, XBOOLE_1:1; hence A64: F is_differentiable_in x0 by A62, FDIFF_1:def_4; ::_thesis: diff (F,x0) = f . x0 L . 1 = (f . x0) * 1 by A9; hence diff (F,x0) = f . x0 by A63, A62, A64, FDIFF_1:def_5; ::_thesis: verum end; Lm13: for a, b being real number for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) proof deffunc H1( real number ) -> Element of NAT = 0 ; let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) defpred S1[ set ] means $1 in ].a,b.[; deffunc H2( real number ) -> Element of REAL = integral (f,a,$1); consider F being Function such that A1: ( dom F = REAL & ( for x being Element of REAL holds ( ( S1[x] implies F . x = H2(x) ) & ( not S1[x] implies F . x = H1(x) ) ) ) ) from PARTFUN1:sch_4(); now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng F implies y in REAL ) assume y in rng F ; ::_thesis: y in REAL then consider x being set such that A2: x in dom F and A3: y = F . x by FUNCT_1:def_3; reconsider x = x as Element of REAL by A1, A2; A4: now__::_thesis:_(_not_x_in_].a,b.[_implies_y_in_REAL_) assume not x in ].a,b.[ ; ::_thesis: y in REAL then F . x = 0 by A1; hence y in REAL by A3; ::_thesis: verum end; now__::_thesis:_(_x_in_].a,b.[_implies_y_in_REAL_) assume x in ].a,b.[ ; ::_thesis: y in REAL then F . x = integral (f,a,x) by A1; hence y in REAL by A3; ::_thesis: verum end; hence y in REAL by A4; ::_thesis: verum end; then rng F c= REAL by TARSKI:def_3; then reconsider F = F as PartFunc of REAL,REAL by A1, RELSET_1:4; take F ; ::_thesis: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) thus ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) by A1; ::_thesis: verum end; theorem :: INTEGRA6:29 for a, b being real number for f being PartFunc of REAL,REAL for x0 being real number st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) proof let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL for x0 being real number st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) let f be PartFunc of REAL,REAL; ::_thesis: for x0 being real number st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) let x0 be real number ; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 implies ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) ) consider F being PartFunc of REAL,REAL such that A1: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) by Lm13; assume ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 ) ; ::_thesis: ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) then ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) by A1, Th28; hence ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) by A1; ::_thesis: verum end;