:: INTEGRA5 semantic presentation begin theorem Th1: :: INTEGRA5:1 for F, F1, F2 being FinSequence of REAL for r1, r2 being Real st ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) holds Sum (F1 - F2) = r1 - r2 proof let F, F1, F2 be FinSequence of REAL ; ::_thesis: for r1, r2 being Real st ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) holds Sum (F1 - F2) = r1 - r2 let r1, r2 be Real; ::_thesis: ( ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) implies Sum (F1 - F2) = r1 - r2 ) assume that A1: ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) and A2: ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) ; ::_thesis: Sum (F1 - F2) = r1 - r2 len F1 = (len F) + (len <*r1*>) by A1, FINSEQ_1:22; then A3: len F1 = (len F) + 1 by FINSEQ_1:39; len F2 = (len <*r2*>) + (len F) by A2, FINSEQ_1:22; then A4: len F2 = 1 + (len F) by FINSEQ_1:39; F1 - F2 = diffreal .: (F1,F2) by RVSUM_1:def_6; then A5: len F1 = len (F1 - F2) by A3, A4, FINSEQ_2:72; for k being Element of NAT st k in dom F1 holds (F1 - F2) . k = (F1 /. k) - (F2 /. k) proof let k be Element of NAT ; ::_thesis: ( k in dom F1 implies (F1 - F2) . k = (F1 /. k) - (F2 /. k) ) assume A6: k in dom F1 ; ::_thesis: (F1 - F2) . k = (F1 /. k) - (F2 /. k) then A7: F1 . k = F1 /. k by PARTFUN1:def_6; A8: k in Seg (len F1) by A6, FINSEQ_1:def_3; then k in dom F2 by A3, A4, FINSEQ_1:def_3; then A9: F2 . k = F2 /. k by PARTFUN1:def_6; k in dom (F1 - F2) by A5, A8, FINSEQ_1:def_3; hence (F1 - F2) . k = (F1 /. k) - (F2 /. k) by A7, A9, VALUED_1:13; ::_thesis: verum end; then A10: Sum (F1 - F2) = (Sum F1) - (Sum F2) by A3, A4, A5, INTEGRA1:22; ( Sum F1 = r1 + (Sum F) & Sum F2 = (Sum F) + r2 ) by A1, A2, RVSUM_1:74, RVSUM_1:76; hence Sum (F1 - F2) = r1 - r2 by A10; ::_thesis: verum end; theorem Th2: :: INTEGRA5:2 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds ( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) ) proof let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies ( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) ) ) assume A1: len F1 = len F2 ; ::_thesis: ( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) ) F1 + F2 = addreal .: (F1,F2) by RVSUM_1:def_4; hence A2: len F1 = len (F1 + F2) by A1, FINSEQ_2:72; ::_thesis: ( len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) ) F1 - F2 = diffreal .: (F1,F2) by RVSUM_1:def_6; hence A3: len F1 = len (F1 - F2) by A1, FINSEQ_2:72; ::_thesis: ( Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) ) for k being Element of NAT st k in dom F1 holds (F1 + F2) . k = (F1 /. k) + (F2 /. k) proof let k be Element of NAT ; ::_thesis: ( k in dom F1 implies (F1 + F2) . k = (F1 /. k) + (F2 /. k) ) assume A4: k in dom F1 ; ::_thesis: (F1 + F2) . k = (F1 /. k) + (F2 /. k) then A5: F1 . k = F1 /. k by PARTFUN1:def_6; A6: k in Seg (len F1) by A4, FINSEQ_1:def_3; then k in dom F2 by A1, FINSEQ_1:def_3; then A7: F2 . k = F2 /. k by PARTFUN1:def_6; k in dom (F1 + F2) by A2, A6, FINSEQ_1:def_3; hence (F1 + F2) . k = (F1 /. k) + (F2 /. k) by A5, A7, VALUED_1:def_1; ::_thesis: verum end; hence Sum (F1 + F2) = (Sum F1) + (Sum F2) by A1, A2, INTEGRA1:21; ::_thesis: Sum (F1 - F2) = (Sum F1) - (Sum F2) for k being Element of NAT st k in dom F1 holds (F1 - F2) . k = (F1 /. k) - (F2 /. k) proof let k be Element of NAT ; ::_thesis: ( k in dom F1 implies (F1 - F2) . k = (F1 /. k) - (F2 /. k) ) assume A8: k in dom F1 ; ::_thesis: (F1 - F2) . k = (F1 /. k) - (F2 /. k) then A9: F1 . k = F1 /. k by PARTFUN1:def_6; A10: k in Seg (len F1) by A8, FINSEQ_1:def_3; then k in dom F2 by A1, FINSEQ_1:def_3; then A11: F2 . k = F2 /. k by PARTFUN1:def_6; k in dom (F1 - F2) by A3, A10, FINSEQ_1:def_3; hence (F1 - F2) . k = (F1 /. k) - (F2 /. k) by A9, A11, VALUED_1:13; ::_thesis: verum end; hence Sum (F1 - F2) = (Sum F1) - (Sum F2) by A1, A3, INTEGRA1:22; ::_thesis: verum end; theorem Th3: :: INTEGRA5:3 for F1, F2 being FinSequence of REAL st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds F1 . i <= F2 . i ) holds Sum F1 <= Sum F2 proof let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds F1 . i <= F2 . i ) implies Sum F1 <= Sum F2 ) assume that A1: len F1 = len F2 and A2: for i being Element of NAT st i in dom F1 holds F1 . i <= F2 . i ; ::_thesis: Sum F1 <= Sum F2 reconsider R1 = F1 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92; reconsider R2 = F2 as Element of (len F1) -tuples_on REAL by A1, FINSEQ_2:92; for i being Nat st i in Seg (len F1) holds R1 . i <= R2 . i proof let i be Nat; ::_thesis: ( i in Seg (len F1) implies R1 . i <= R2 . i ) assume i in Seg (len F1) ; ::_thesis: R1 . i <= R2 . i then i in dom F1 by FINSEQ_1:def_3; hence R1 . i <= R2 . i by A2; ::_thesis: verum end; hence Sum F1 <= Sum F2 by RVSUM_1:82; ::_thesis: verum end; begin notation let f be PartFunc of REAL,REAL; let C be non empty Subset of REAL; synonym f || C for f | C; end; definition let f be PartFunc of REAL,REAL; let C be non empty Subset of REAL; :: original: || redefine funcf || C -> PartFunc of C,REAL; correctness coherence f || C is PartFunc of C,REAL; by PARTFUN1:10; end; theorem Th4: :: INTEGRA5:4 for f, g being PartFunc of REAL,REAL for C being non empty Subset of REAL holds (f || C) (#) (g || C) = (f (#) g) || C proof let f, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds (f || C) (#) (g || C) = (f (#) g) || C let C be non empty Subset of REAL; ::_thesis: (f || C) (#) (g || C) = (f (#) g) || C A1: dom ((f (#) g) || C) = (dom (f (#) g)) /\ C by RELAT_1:61 .= ((dom f) /\ (dom g)) /\ C by VALUED_1:def_4 ; A2: dom ((f || C) (#) (g || C)) = (dom (f | C)) /\ (dom (g || C)) by VALUED_1:def_4 .= ((dom f) /\ C) /\ (dom (g | C)) by RELAT_1:61 .= ((dom f) /\ C) /\ ((dom g) /\ C) by RELAT_1:61 .= (((dom f) /\ C) /\ C) /\ (dom g) by XBOOLE_1:16 .= ((dom f) /\ (C /\ C)) /\ (dom g) by XBOOLE_1:16 .= ((dom f) /\ C) /\ (dom g) ; then A3: dom ((f || C) (#) (g || C)) = dom ((f (#) g) || C) by A1, XBOOLE_1:16; for c being Element of C st c in dom ((f || C) (#) (g || C)) holds ((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c proof let c be Element of C; ::_thesis: ( c in dom ((f || C) (#) (g || C)) implies ((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c ) A4: ((f || C) (#) (g || C)) . c = ((f | C) . c) * ((g | C) . c) by VALUED_1:5; assume A5: c in dom ((f || C) (#) (g || C)) ; ::_thesis: ((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c then A6: c in (dom (f || C)) /\ (dom (g || C)) by VALUED_1:def_4; then A7: c in dom (f || C) by XBOOLE_0:def_4; A8: c in dom (g || C) by A6, XBOOLE_0:def_4; ((f (#) g) || C) . c = (f (#) g) . c by A3, A5, FUNCT_1:47 .= (f . c) * (g . c) by VALUED_1:5 .= ((f | C) . c) * (g . c) by A7, FUNCT_1:47 ; hence ((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c by A8, A4, FUNCT_1:47; ::_thesis: verum end; hence (f || C) (#) (g || C) = (f (#) g) || C by A2, A1, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum end; theorem Th5: :: INTEGRA5:5 for f, g being PartFunc of REAL,REAL for C being non empty Subset of REAL holds (f + g) || C = (f || C) + (g || C) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds (f + g) || C = (f || C) + (g || C) let C be non empty Subset of REAL; ::_thesis: (f + g) || C = (f || C) + (g || C) A1: dom ((f || C) + (g || C)) = (dom (f | C)) /\ (dom (g || C)) by VALUED_1:def_1 .= ((dom f) /\ C) /\ (dom (g | C)) by RELAT_1:61 .= ((dom f) /\ C) /\ ((dom g) /\ C) by RELAT_1:61 .= (dom f) /\ (C /\ ((dom g) /\ C)) by XBOOLE_1:16 .= (dom f) /\ ((dom g) /\ (C /\ C)) by XBOOLE_1:16 .= (dom f) /\ ((dom g) /\ C) ; A2: dom ((f + g) || C) = (dom (f + g)) /\ C by RELAT_1:61 .= ((dom f) /\ (dom g)) /\ C by VALUED_1:def_1 ; then A3: dom ((f + g) || C) = dom ((f || C) + (g || C)) by A1, XBOOLE_1:16; for c being Element of C st c in dom ((f + g) || C) holds ((f + g) || C) . c = ((f || C) + (g || C)) . c proof let c be Element of C; ::_thesis: ( c in dom ((f + g) || C) implies ((f + g) || C) . c = ((f || C) + (g || C)) . c ) assume A4: c in dom ((f + g) || C) ; ::_thesis: ((f + g) || C) . c = ((f || C) + (g || C)) . c then c in (dom (f + g)) /\ C by RELAT_1:61; then A5: c in dom (f + g) by XBOOLE_0:def_4; A6: c in (dom (f || C)) /\ (dom (g || C)) by A3, A4, VALUED_1:def_1; then A7: c in dom (f || C) by XBOOLE_0:def_4; A8: ((f + g) || C) . c = (f + g) . c by A4, FUNCT_1:47 .= (f . c) + (g . c) by A5, VALUED_1:def_1 ; A9: c in dom (g || C) by A6, XBOOLE_0:def_4; ((f || C) + (g || C)) . c = ((f | C) . c) + ((g || C) . c) by A3, A4, VALUED_1:def_1 .= (f . c) + ((g | C) . c) by A7, FUNCT_1:47 ; hence ((f + g) || C) . c = ((f || C) + (g || C)) . c by A8, A9, FUNCT_1:47; ::_thesis: verum end; hence (f + g) || C = (f || C) + (g || C) by A2, A1, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,REAL; predf is_integrable_on A means :Def1: :: INTEGRA5:def 1 f || A is integrable ; end; :: deftheorem Def1 defines is_integrable_on INTEGRA5:def_1_:_ for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL holds ( f is_integrable_on A iff f || A is integrable ); definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,REAL; func integral (f,A) -> Real equals :: INTEGRA5:def 2 integral (f || A); correctness coherence integral (f || A) is Real; ; end; :: deftheorem defines integral INTEGRA5:def_2_:_ for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL holds integral (f,A) = integral (f || A); theorem Th6: :: INTEGRA5:6 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 total 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 total let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f implies f || A is total ) assume A1: A c= dom f ; ::_thesis: f || A is total dom (f || A) = (dom f) /\ A by RELAT_1:61 .= A by A1, XBOOLE_1:28 ; hence f || A is total by PARTFUN1:def_2; ::_thesis: verum end; theorem :: INTEGRA5:7 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st f | A is bounded_above holds (f || A) | A is bounded_above proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is bounded_above holds (f || A) | A is bounded_above let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded_above implies (f || A) | A is bounded_above ) assume f | A is bounded_above ; ::_thesis: (f || A) | A is bounded_above then consider r being real number such that A1: for x being set st x in A /\ (dom f) holds f . x <= r by RFUNCT_1:70; for x being set st x in A /\ (dom (f || A)) holds (f || A) . x <= r proof let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x <= r ) dom (f | A) = (dom f) /\ A by RELAT_1:61; then A2: A /\ (dom (f || A)) = (dom f) /\ A by XBOOLE_1:28; assume A3: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x <= r then x in dom (f | A) by XBOOLE_1:28; then (f || A) . x = f . x by FUNCT_1:47; hence (f || A) . x <= r by A1, A3, A2; ::_thesis: verum end; hence (f || A) | A is bounded_above by RFUNCT_1:70; ::_thesis: verum end; theorem :: INTEGRA5:8 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st f | A is bounded_below holds (f || A) | A is bounded_below proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is bounded_below holds (f || A) | A is bounded_below let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded_below implies (f || A) | A is bounded_below ) assume f | A is bounded_below ; ::_thesis: (f || A) | A is bounded_below then consider r being real number such that A1: for x being set st x in A /\ (dom f) holds f . x >= r by RFUNCT_1:71; for x being set st x in A /\ (dom (f || A)) holds (f || A) . x >= r proof let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x >= r ) dom (f | A) = (dom f) /\ A by RELAT_1:61; then A2: A /\ (dom (f || A)) = (dom f) /\ A by XBOOLE_1:28; assume A3: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x >= r then x in dom (f | A) by XBOOLE_1:28; then (f || A) . x = f . x by FUNCT_1:47; hence (f || A) . x >= r by A1, A3, A2; ::_thesis: verum end; hence (f || A) | A is bounded_below by RFUNCT_1:71; ::_thesis: verum end; theorem :: INTEGRA5:9 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st f | A is bounded holds (f || A) | A is bounded proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is bounded holds (f || A) | A is bounded let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded implies (f || A) | A is bounded ) assume f | A is bounded ; ::_thesis: (f || A) | A is bounded then ( (f || A) | A is bounded_above & (f || A) | A is bounded_below ) ; hence (f || A) | A is bounded ; ::_thesis: verum end; begin theorem Th10: :: INTEGRA5:10 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st A c= dom f & f | A is continuous holds f | A is bounded 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 | A is continuous holds f | A is bounded let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & f | A is continuous implies f | A is bounded ) assume A1: A c= dom f ; ::_thesis: ( not f | A is continuous or f | A is bounded ) assume f | A is continuous ; ::_thesis: f | A is bounded then A2: f .: A is real-bounded by A1, FCONT_1:29, RCOMP_1:10; then consider a being real number such that A3: a is UpperBound of f .: A by XXREAL_2:def_10; A4: for r being real number st r in f .: A holds r <= a by A3, XXREAL_2:def_1; consider b being real number such that A5: b is LowerBound of f .: A by A2, XXREAL_2:def_9; A6: for r being real number st r in f .: A holds b <= r by A5, XXREAL_2:def_2; for x being set st x in A /\ (dom f) holds b <= f . x proof let x be set ; ::_thesis: ( x in A /\ (dom f) implies b <= f . x ) assume x in A /\ (dom f) ; ::_thesis: b <= f . x then ( x in A & x in dom f ) by XBOOLE_0:def_4; then f . x in f .: A by FUNCT_1:def_6; hence b <= f . x by A6; ::_thesis: verum end; then A7: f | A is bounded_below by RFUNCT_1:71; for x being set st x in A /\ (dom f) holds f . x <= a proof let x be set ; ::_thesis: ( x in A /\ (dom f) implies f . x <= a ) assume x in A /\ (dom f) ; ::_thesis: f . x <= a then ( x in A & x in dom f ) by XBOOLE_0:def_4; then f . x in f .: A by FUNCT_1:def_6; hence f . x <= a by A4; ::_thesis: verum end; then f | A is bounded_above by RFUNCT_1:70; hence f | A is bounded by A7; ::_thesis: verum end; theorem Th11: :: INTEGRA5:11 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st A c= dom f & f | A is continuous holds f is_integrable_on 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 | A is continuous holds f is_integrable_on A let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & f | A is continuous implies f is_integrable_on A ) assume A1: A c= dom f ; ::_thesis: ( not f | A is continuous or f is_integrable_on A ) reconsider g = f | A as PartFunc of A,REAL by PARTFUN1:10; A2: dom g = (dom f) /\ A by RELAT_1:61 .= A by A1, XBOOLE_1:28 ; then A3: g is total by PARTFUN1:def_2; for y being set st y in f .: A holds y in rng g proof let y be set ; ::_thesis: ( y in f .: A implies y in rng g ) assume y in f .: A ; ::_thesis: y in rng g then consider x being set such that x in dom f and A4: x in A and A5: y = f . x by FUNCT_1:def_6; g . x in rng g by A2, A4, FUNCT_1:def_3; hence y in rng g by A2, A4, A5, FUNCT_1:47; ::_thesis: verum end; then A6: f .: A c= rng g by TARSKI:def_3; for y being set st y in rng g holds y in f .: A proof let y be set ; ::_thesis: ( y in rng g implies y in f .: A ) assume y in rng g ; ::_thesis: y in f .: A then consider x being set such that A7: x in dom g and A8: y = g . x by FUNCT_1:def_3; f . x in f .: A by A1, A2, A7, FUNCT_1:def_6; hence y in f .: A by A7, A8, FUNCT_1:47; ::_thesis: verum end; then rng g c= f .: A by TARSKI:def_3; then A9: rng g = f .: A by A6, XBOOLE_0:def_10; assume A10: f | A is continuous ; ::_thesis: f is_integrable_on A then f .: A is real-bounded by A1, FCONT_1:29, RCOMP_1:10; then A11: ( g | A is bounded_above & g | A is bounded_below ) by A9, INTEGRA1:12, INTEGRA1:14; reconsider g = g as Function of A,REAL by A3; A12: f | A is uniformly_continuous by A1, A10, FCONT_2:11; for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 proof let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 ) reconsider osc = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ; assume A13: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 A14: for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc . m) - 0) < r proof let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc . m) - 0) < r ) assume A15: r > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc . m) - 0) < r ex r1 being Real st ( r1 > 0 & r1 * (vol A) < r ) proof now__::_thesis:_ex_r1_being_Real_st_ (_r1_>_0_&_r1_*_(vol_A)_<_r_) percases ( vol A = 0 or vol A > 0 ) by INTEGRA1:9; supposeA16: vol A = 0 ; ::_thesis: ex r1 being Real st ( r1 > 0 & r1 * (vol A) < r ) consider r1 being Real such that A17: r1 = 1 ; r1 * (vol A) < r by A15, A16; hence ex r1 being Real st ( r1 > 0 & r1 * (vol A) < r ) by A17; ::_thesis: verum end; supposeA18: vol A > 0 ; ::_thesis: ex r1 being Real st ( r1 > 0 & r1 * (vol A) < r ) then r / (vol A) > 0 by A15, XREAL_1:139; then consider r1 being real number such that A19: 0 < r1 and A20: r1 < r / (vol A) by XREAL_1:5; reconsider r1 = r1 as Real by XREAL_0:def_1; r1 * (vol A) < r by A18, A20, XREAL_1:79; hence ex r1 being Real st ( r1 > 0 & r1 * (vol A) < r ) by A19; ::_thesis: verum end; end; end; hence ex r1 being Real st ( r1 > 0 & r1 * (vol A) < r ) ; ::_thesis: verum end; then consider r1 being Real such that A21: r1 > 0 and A22: r1 * (vol A) < r ; consider s being Real such that A23: 0 < s and A24: for x1, x2 being Real st x1 in dom (f | A) & x2 in dom (f | A) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r1 by A12, A21, FCONT_2:1; consider n being Element of NAT such that A25: for m being Element of NAT st n <= m holds abs (((delta T) . m) - 0) < s by A13, A23, SEQ_2:def_7; A26: for m being Element of NAT st n <= m holds ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) proof let m be Element of NAT ; ::_thesis: ( n <= m implies ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) ) reconsider D = T . m as Division of A ; len (upper_volume (g,D)) = len D by INTEGRA1:def_6; then reconsider UV = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; len (lower_volume (g,D)) = len D by INTEGRA1:def_7; then reconsider LV = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; reconsider OSC = UV - LV as Element of (len D) -tuples_on REAL ; len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def_6; then reconsider VOL = upper_volume ((chi (A,A)),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; assume A27: n <= m ; ::_thesis: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) A28: for k being Element of NAT st k in dom D holds ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) proof let k be Element of NAT ; ::_thesis: ( k in dom D implies ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) ) assume A29: k in dom D ; ::_thesis: ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) reconsider h = g | (divset (D,k)) as PartFunc of (divset (D,k)),REAL by PARTFUN1:10; dom g = A by PARTFUN1:def_2; then (dom g) /\ (divset (D,k)) = divset (D,k) by A29, INTEGRA1:8, XBOOLE_1:28; then dom h = divset (D,k) by RELAT_1:61; then h is total by PARTFUN1:def_2; then reconsider h = h as Function of (divset (D,k)),REAL ; A30: for x1, x2 being Real st x1 in divset (D,k) & x2 in divset (D,k) holds abs ((h . x1) - (h . x2)) <= r1 proof (upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A29, INTEGRA1:20; then A31: (upper_volume ((chi (A,A)),D)) . k >= 0 by INTEGRA1:9; k in Seg (len D) by A29, FINSEQ_1:def_3; then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then A32: (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; dom h = (dom g) /\ (divset (D,k)) by RELAT_1:61; then A33: dom h c= dom g by XBOOLE_1:17; let x1, x2 be Real; ::_thesis: ( x1 in divset (D,k) & x2 in divset (D,k) implies abs ((h . x1) - (h . x2)) <= r1 ) assume that A34: x1 in divset (D,k) and A35: x2 in divset (D,k) ; ::_thesis: abs ((h . x1) - (h . x2)) <= r1 A36: x2 in dom h by A35, PARTFUN1:def_2; then g . x2 = h . x2 by FUNCT_1:47; then A37: f . x2 = h . x2 by A36, A33, FUNCT_1:47; A38: abs (x1 - x2) <= (delta T) . m proof now__::_thesis:_abs_(x1_-_x2)_<=_(delta_T)_._m percases ( x1 >= x2 or x1 < x2 ) ; suppose x1 >= x2 ; ::_thesis: abs (x1 - x2) <= (delta T) . m then x1 - x2 >= 0 by XREAL_1:48; then A39: abs (x1 - x2) = x1 - x2 by ABSVALUE:def_1; ( x1 <= upper_bound (divset (D,k)) & x2 >= lower_bound (divset (D,k)) ) by A34, A35, INTEGRA2:1; then abs (x1 - x2) <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A39, XREAL_1:13; then A40: abs (x1 - x2) <= vol (divset (D,k)) by INTEGRA1:def_5; k in Seg (len D) by A29, FINSEQ_1:def_3; then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def_8; then A41: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def_1; (upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A29, INTEGRA1:20; then abs (x1 - x2) <= delta (T . m) by A40, A41, XXREAL_0:2; hence abs (x1 - x2) <= (delta T) . m by INTEGRA3:def_2; ::_thesis: verum end; suppose x1 < x2 ; ::_thesis: abs (x1 - x2) <= (delta T) . m then x1 - x2 < 0 by XREAL_1:49; then abs (x1 - x2) = - (x1 - x2) by ABSVALUE:def_1; then A42: abs (x1 - x2) = x2 - x1 ; ( x2 <= upper_bound (divset (D,k)) & x1 >= lower_bound (divset (D,k)) ) by A34, A35, INTEGRA2:1; then abs (x1 - x2) <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A42, XREAL_1:13; then A43: abs (x1 - x2) <= vol (divset (D,k)) by INTEGRA1:def_5; k in Seg (len D) by A29, FINSEQ_1:def_3; then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def_8; then A44: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def_1; (upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A29, INTEGRA1:20; then abs (x1 - x2) <= delta (T . m) by A43, A44, XXREAL_0:2; hence abs (x1 - x2) <= (delta T) . m by INTEGRA3:def_2; ::_thesis: verum end; end; end; hence abs (x1 - x2) <= (delta T) . m ; ::_thesis: verum end; (delta T) . m = delta D by INTEGRA3:def_2 .= max (rng (upper_volume ((chi (A,A)),D))) by INTEGRA3:def_1 ; then ((delta T) . m) - 0 >= 0 by A31, A32, XXREAL_2:def_8; then A45: abs (x1 - x2) <= abs (((delta T) . m) - 0) by A38, ABSVALUE:def_1; abs (((delta T) . m) - 0) < s by A25, A27; then A46: abs (x1 - x2) < s by A45, XXREAL_0:2; A47: x1 in dom h by A34, PARTFUN1:def_2; then g . x1 = h . x1 by FUNCT_1:47; then f . x1 = h . x1 by A47, A33, FUNCT_1:47; hence abs ((h . x1) - (h . x2)) <= r1 by A24, A46, A47, A36, A33, A37; ::_thesis: verum end; vol (divset (D,k)) >= 0 by INTEGRA1:9; then ((upper_bound (rng (g | (divset (D,k))))) - (lower_bound (rng (g | (divset (D,k)))))) * (vol (divset (D,k))) <= r1 * (vol (divset (D,k))) by A30, INTEGRA4:24, XREAL_1:64; then ((upper_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) ; then ((upper_volume (g,D)) . k) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) by A29, INTEGRA1:def_6; then ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * (vol (divset (D,k))) by A29, INTEGRA1:def_7; hence ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) by A29, INTEGRA1:20; ::_thesis: verum end; for k being Nat st k in Seg (len D) holds OSC . k <= (r1 * VOL) . k proof let k be Nat; ::_thesis: ( k in Seg (len D) implies OSC . k <= (r1 * VOL) . k ) assume k in Seg (len D) ; ::_thesis: OSC . k <= (r1 * VOL) . k then A48: k in dom D by FINSEQ_1:def_3; OSC . k = ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) by RVSUM_1:27; then OSC . k <= r1 * (VOL . k) by A28, A48; hence OSC . k <= (r1 * VOL) . k by RVSUM_1:45; ::_thesis: verum end; then Sum OSC <= Sum (r1 * VOL) by RVSUM_1:82; then Sum OSC <= r1 * (Sum VOL) by RVSUM_1:87; then (Sum UV) - (Sum LV) <= r1 * (Sum VOL) by RVSUM_1:90; then (upper_sum (g,D)) - (Sum LV) <= r1 * (Sum VOL) by INTEGRA1:def_8; then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (Sum VOL) by INTEGRA1:def_9; then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA1:24; then ((upper_sum (g,T)) . m) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA2:def_2; hence ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) by INTEGRA2:def_3; ::_thesis: verum end; for m being Element of NAT st n <= m holds abs ((osc . m) - 0) < r proof let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc . m) - 0) < r ) reconsider D = T . m as Division of A ; assume n <= m ; ::_thesis: abs ((osc . m) - 0) < r then ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) by A26; then A49: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) < r by A22, XXREAL_0:2; upper_sum (g,D) >= lower_sum (g,D) by A11, INTEGRA1:28; then (upper_sum (g,T)) . m >= lower_sum (g,D) by INTEGRA2:def_2; then (upper_sum (g,T)) . m >= (lower_sum (g,T)) . m by INTEGRA2:def_3; then A50: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) >= 0 by XREAL_1:48; osc . m = ((upper_sum (g,T)) . m) + ((- (lower_sum (g,T))) . m) by SEQ_1:7 .= ((upper_sum (g,T)) . m) + (- ((lower_sum (g,T)) . m)) by SEQ_1:10 .= ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) ; hence abs ((osc . m) - 0) < r by A49, A50, ABSVALUE:def_1; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc . m) - 0) < r ; ::_thesis: verum end; then osc is convergent by SEQ_2:def_6; then A51: lim osc = 0 by A14, SEQ_2:def_7; ( upper_sum (g,T) is convergent & lower_sum (g,T) is convergent ) by A11, A13, INTEGRA4:8, INTEGRA4:9; hence (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A51, SEQ_2:12; ::_thesis: verum end; then g is integrable by A11, INTEGRA4:12; hence f is_integrable_on A by Def1; ::_thesis: verum end; theorem Th12: :: INTEGRA5:12 for A being non empty closed_interval Subset of REAL for X being set for f being PartFunc of REAL,REAL for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set for f being PartFunc of REAL,REAL for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) let X be set ; ::_thesis: for f being PartFunc of REAL,REAL for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) let f be PartFunc of REAL,REAL; ::_thesis: for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) let D be Division of A; ::_thesis: ( A c= X & f is_differentiable_on X & (f `| X) | A is bounded implies ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) ) assume that A1: A c= X and A2: f is_differentiable_on X and A3: (f `| X) | A is bounded ; ::_thesis: ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) (len D) - 1 in NAT proof ex j being Nat st len D = 1 + j by NAT_1:10, NAT_1:14; hence (len D) - 1 in NAT by ORDINAL1:def_12; ::_thesis: verum end; then reconsider k1 = (len D) - 1 as Element of NAT ; deffunc H1( Nat) -> Element of REAL = f . (lower_bound (divset (D,($1 + 1)))); deffunc H2( Nat) -> Element of REAL = (f . (upper_bound (divset (D,$1)))) - (f . (lower_bound (divset (D,$1)))); consider p being FinSequence of REAL such that A4: ( len p = len D & ( for i being Nat st i in dom p holds p . i = H2(i) ) ) from FINSEQ_2:sch_1(); X c= dom f by A2, FDIFF_1:def_6; then A5: A c= dom f by A1, XBOOLE_1:1; A6: for k being Element of NAT st k in dom D holds ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) proof let k be Element of NAT ; ::_thesis: ( k in dom D implies ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) ) assume A7: k in dom D ; ::_thesis: ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) now__::_thesis:_ex_r_being_Real_st_ (_r_in_divset_(D,k)_&_(f_._(upper_bound_(divset_(D,k))))_-_(f_._(lower_bound_(divset_(D,k))))_=_(diff_(f,r))_*_(vol_(divset_(D,k)))_) percases ( lower_bound (divset (D,k)) = upper_bound (divset (D,k)) or lower_bound (divset (D,k)) <> upper_bound (divset (D,k)) ) ; supposeA8: lower_bound (divset (D,k)) = upper_bound (divset (D,k)) ; ::_thesis: ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) consider r being Real such that A9: r = upper_bound (divset (D,k)) ; A10: r in divset (D,k) proof ex a, b being Real st ( a <= b & a = lower_bound (divset (D,k)) & b = upper_bound (divset (D,k)) ) by SEQ_4:11; hence r in divset (D,k) by A9, INTEGRA2:1; ::_thesis: verum end; (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = 0 by A8; then vol (divset (D,k)) = 0 by INTEGRA1:def_5; then (diff (f,r)) * (vol (divset (D,k))) = 0 ; hence ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A8, A10; ::_thesis: verum end; supposeA11: lower_bound (divset (D,k)) <> upper_bound (divset (D,k)) ; ::_thesis: ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) ex r1, r2 being Real st ( r1 <= r2 & r1 = lower_bound (divset (D,k)) & r2 = upper_bound (divset (D,k)) ) by SEQ_4:11; then A12: lower_bound (divset (D,k)) < upper_bound (divset (D,k)) by A11, XXREAL_0:1; f | X is continuous by A2, FDIFF_1:25; then f | A is continuous by A1, FCONT_1:16; then A13: f | (divset (D,k)) is continuous by A7, FCONT_1:16, INTEGRA1:8; A14: divset (D,k) = [.(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).] by INTEGRA1:4; then A15: ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= divset (D,k) by XXREAL_1:25; A16: divset (D,k) c= A by A7, INTEGRA1:8; then ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= A by A15, XBOOLE_1:1; then f is_differentiable_on ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ by A1, A2, FDIFF_1:26, XBOOLE_1:1; then consider r being Real such that A17: r in ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ and A18: diff (f,r) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) / ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) by A5, A16, A13, A12, A14, ROLLE:3, XBOOLE_1:1; (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) > 0 by A12, XREAL_1:50; then (diff (f,r)) * ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by A18, XCMPLX_1:87; then (diff (f,r)) * (vol (divset (D,k))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by INTEGRA1:def_5; hence ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A15, A17; ::_thesis: verum end; end; end; hence ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) ; ::_thesis: verum end; A19: dom p = Seg (len D) by A4, FINSEQ_1:def_3; A20: for i being Element of NAT st i in Seg k1 holds upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) proof let i be Element of NAT ; ::_thesis: ( i in Seg k1 implies upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) ) assume A21: i in Seg k1 ; ::_thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) then i <= k1 by FINSEQ_1:1; then A22: i + 1 <= k1 + 1 by XREAL_1:7; 1 <= i by A21, FINSEQ_1:1; then 1 + 0 <= i + 1 by XREAL_1:7; then i + 1 in Seg (len D) by A22, FINSEQ_1:1; then A23: i + 1 in dom D by FINSEQ_1:def_3; k1 + 1 = len D ; then k1 <= len D by NAT_1:11; then Seg k1 c= Seg (len D) by FINSEQ_1:5; then i in Seg (len D) by A21; then A24: i in dom D by FINSEQ_1:def_3; A25: (i + 1) - 1 = i ; now__::_thesis:_upper_bound_(divset_(D,i))_=_lower_bound_(divset_(D,(i_+_1))) percases ( i = 1 or i <> 1 ) ; supposeA26: i = 1 ; ::_thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) then upper_bound (divset (D,i)) = D . i by A24, INTEGRA1:def_4; hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A26, INTEGRA1:def_4; ::_thesis: verum end; supposeA27: i <> 1 ; ::_thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) i >= 1 by A21, FINSEQ_1:1; then i + 1 >= 1 + 1 by XREAL_1:6; then A28: i + 1 <> 1 ; upper_bound (divset (D,i)) = D . i by A24, A27, INTEGRA1:def_4; hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A28, INTEGRA1:def_4; ::_thesis: verum end; end; end; hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) ; ::_thesis: verum end; consider s2 being FinSequence of REAL such that A29: ( len s2 = k1 & ( for i being Nat st i in dom s2 holds s2 . i = H1(i) ) ) from FINSEQ_2:sch_1(); A30: for k being Element of NAT st k in dom D holds rng (((f `| X) || A) | (divset (D,k))) is real-bounded proof dom (f `| X) = X by A2, FDIFF_1:def_7; then reconsider g = f `| X as PartFunc of X,REAL by RELSET_1:5; let k be Element of NAT ; ::_thesis: ( k in dom D implies rng (((f `| X) || A) | (divset (D,k))) is real-bounded ) assume k in dom D ; ::_thesis: rng (((f `| X) || A) | (divset (D,k))) is real-bounded consider r1 being real number such that A31: for x being set st x in A /\ (dom (f `| X)) holds (f `| X) . x <= r1 by A3, RFUNCT_1:70; consider r2 being real number such that A32: for x being set st x in A /\ (dom (f `| X)) holds (f `| X) . x >= r2 by A3, RFUNCT_1:71; A33: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61; for x being set st x in A /\ (dom ((f `| X) || A)) holds ((f `| X) || A) . x >= r2 proof let x be set ; ::_thesis: ( x in A /\ (dom ((f `| X) || A)) implies ((f `| X) || A) . x >= r2 ) A34: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16 .= A /\ (dom (f `| X)) ; reconsider y = g . x as Real ; assume A35: x in A /\ (dom ((f `| X) || A)) ; ::_thesis: ((f `| X) || A) . x >= r2 then y >= r2 by A32, A33, A34; hence ((f `| X) || A) . x >= r2 by A33, A35, A34, FUNCT_1:47; ::_thesis: verum end; then ((f `| X) || A) | A is bounded_below by RFUNCT_1:71; then A36: rng (((f `| X) || A) | (divset (D,k))) is bounded_below by INTEGRA4:19; for x being set st x in A /\ (dom ((f `| X) || A)) holds ((f `| X) || A) . x <= r1 proof let x be set ; ::_thesis: ( x in A /\ (dom ((f `| X) || A)) implies ((f `| X) || A) . x <= r1 ) A37: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16 .= A /\ (dom (f `| X)) ; reconsider y = g . x as Real ; assume A38: x in A /\ (dom ((f `| X) || A)) ; ::_thesis: ((f `| X) || A) . x <= r1 then y <= r1 by A31, A33, A37; hence ((f `| X) || A) . x <= r1 by A33, A38, A37, FUNCT_1:47; ::_thesis: verum end; then ((f `| X) || A) | A is bounded_above by RFUNCT_1:70; then rng (((f `| X) || A) | (divset (D,k))) is bounded_above by INTEGRA4:18; hence rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A36; ::_thesis: verum end; deffunc H3( Nat) -> Element of REAL = f . (upper_bound (divset (D,$1))); consider s1 being FinSequence of REAL such that A39: ( len s1 = k1 & ( for i being Nat st i in dom s1 holds s1 . i = H3(i) ) ) from FINSEQ_2:sch_1(); A40: dom s2 = Seg k1 by A29, FINSEQ_1:def_3; ( len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) & len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*(f . (upper_bound A))*>) holds p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ) ) proof dom <*(f . (upper_bound A))*> = Seg 1 by FINSEQ_1:def_8; then len <*(f . (upper_bound A))*> = 1 by FINSEQ_1:def_3; then A41: len (s1 ^ <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:22; dom <*(f . (lower_bound A))*> = Seg 1 by FINSEQ_1:def_8; then len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:def_3; hence A42: len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) by A29, A41, FINSEQ_1:22; ::_thesis: ( len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*(f . (upper_bound A))*>) holds p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ) ) thus len (s1 ^ <*(f . (upper_bound A))*>) = len p by A4, A41; ::_thesis: for i being Element of NAT st i in dom (s1 ^ <*(f . (upper_bound A))*>) holds p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) let i be Element of NAT ; ::_thesis: ( i in dom (s1 ^ <*(f . (upper_bound A))*>) implies p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ) assume A43: i in dom (s1 ^ <*(f . (upper_bound A))*>) ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) then A44: (s1 ^ <*(f . (upper_bound A))*>) /. i = (s1 ^ <*(f . (upper_bound A))*>) . i by PARTFUN1:def_6; i in Seg (len (s1 ^ <*(f . (upper_bound A))*>)) by A43, FINSEQ_1:def_3; then i in dom (<*(f . (lower_bound A))*> ^ s2) by A42, FINSEQ_1:def_3; then A45: (<*(f . (lower_bound A))*> ^ s2) /. i = (<*(f . (lower_bound A))*> ^ s2) . i by PARTFUN1:def_6; A46: ( len D = 1 or not len D is trivial ) by NAT_2:def_1; now__::_thesis:_p_._i_=_((s1_^_<*(f_._(upper_bound_A))*>)_/._i)_-_((<*(f_._(lower_bound_A))*>_^_s2)_/._i) percases ( len D = 1 or len D >= 2 ) by A46, NAT_2:29; supposeA47: len D = 1 ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) then A48: i in Seg 1 by A41, A43, FINSEQ_1:def_3; then A49: i = 1 by FINSEQ_1:2, TARSKI:def_1; s1 = {} by A39, A47; then s1 ^ <*(f . (upper_bound A))*> = <*(f . (upper_bound A))*> by FINSEQ_1:34; then A50: (s1 ^ <*(f . (upper_bound A))*>) /. i = f . (upper_bound A) by A44, A49, FINSEQ_1:def_8; A51: i in dom D by A47, A48, FINSEQ_1:def_3; s2 = {} by A29, A47; then <*(f . (lower_bound A))*> ^ s2 = <*(f . (lower_bound A))*> by FINSEQ_1:34; then A52: (<*(f . (lower_bound A))*> ^ s2) /. i = f . (lower_bound A) by A45, A49, FINSEQ_1:def_8; D . i = upper_bound A by A47, A49, INTEGRA1:def_2; then A53: upper_bound (divset (D,i)) = upper_bound A by A49, A51, INTEGRA1:def_4; p . i = (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) by A4, A19, A47, A48; hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A49, A51, A50, A52, A53, INTEGRA1:def_4; ::_thesis: verum end; supposeA54: len D >= 2 ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) 1 = 2 - 1 ; then A55: k1 >= 1 by A54, XREAL_1:9; now__::_thesis:_p_._i_=_((s1_^_<*(f_._(upper_bound_A))*>)_/._i)_-_((<*(f_._(lower_bound_A))*>_^_s2)_/._i) percases ( i = 1 or i = len D or ( i <> 1 & i <> len D ) ) ; supposeA56: i = 1 ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) then A57: i in Seg 1 by FINSEQ_1:2, TARSKI:def_1; then i in dom <*(f . (lower_bound A))*> by FINSEQ_1:def_8; then (<*(f . (lower_bound A))*> ^ s2) . i = <*(f . (lower_bound A))*> . i by FINSEQ_1:def_7; then A58: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound A) by A56, FINSEQ_1:def_8; Seg 1 c= Seg k1 by A55, FINSEQ_1:5; then i in Seg k1 by A57; then A59: i in dom s1 by A39, FINSEQ_1:def_3; then (s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by FINSEQ_1:def_7; then A60: (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) by A39, A59; A61: i in Seg 2 by A56, FINSEQ_1:2, TARSKI:def_2; A62: Seg 2 c= Seg (len D) by A54, FINSEQ_1:5; then i in Seg (len D) by A61; then A63: i in dom D by FINSEQ_1:def_3; p . i = (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) by A4, A19, A62, A61; hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A44, A45, A56, A63, A60, A58, INTEGRA1:def_4; ::_thesis: verum end; supposeA64: i = len D ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) then i - (len s1) in Seg 1 by A39, FINSEQ_1:2, TARSKI:def_1; then A65: i - (len s1) in dom <*(f . (upper_bound A))*> by FINSEQ_1:def_8; i = (i - (len s1)) + (len s1) ; then (s1 ^ <*(f . (upper_bound A))*>) . i = <*(f . (upper_bound A))*> . (i - (len s1)) by A65, FINSEQ_1:def_7; then A66: (s1 ^ <*(f . (upper_bound A))*>) /. i = f . (upper_bound A) by A39, A44, A64, FINSEQ_1:def_8; A67: i - (len <*(f . (lower_bound A))*>) = i - 1 by FINSEQ_1:40; A68: i <> 1 by A54, A64; i in Seg (len D) by A64, FINSEQ_1:3; then A69: i in dom D by FINSEQ_1:def_3; p . i = (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) by A4, A19, A64, FINSEQ_1:3; then p . i = (f . (upper_bound (divset (D,i)))) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def_4; then A70: p . i = (f . (D . i)) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def_4; i - 1 <> 0 by A54, A64; then i - 1 in Seg k1 by A64, FINSEQ_1:3; then A71: ( (len <*(f . (lower_bound A))*>) + (i - (len <*(f . (lower_bound A))*>)) = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) by A29, A67, FINSEQ_1:def_3; then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - (len <*(f . (lower_bound A))*>)) by FINSEQ_1:def_7; then (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) by A29, A67, A71; then (<*(f . (lower_bound A))*> ^ s2) . i = f . (D . (i - 1)) by A69, A68, INTEGRA1:def_4; hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A45, A64, A66, A70, INTEGRA1:def_2; ::_thesis: verum end; supposeA72: ( i <> 1 & i <> len D ) ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) (len s1) + (len <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:39; then A73: i in Seg (len D) by A43, FINSEQ_1:def_7; A74: ( i in dom s1 & i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) proof i <> 0 by A73, FINSEQ_1:1; then not i is trivial by A72, NAT_2:def_1; then i >= 1 + 1 by NAT_2:29; then A75: i - 1 >= 1 by XREAL_1:19; A76: 1 <= i by A73, FINSEQ_1:1; i <= len D by A73, FINSEQ_1:1; then A77: i < k1 + 1 by A72, XXREAL_0:1; then A78: i <= k1 by NAT_1:13; then i in Seg (len s1) by A39, A76, FINSEQ_1:1; hence i in dom s1 by FINSEQ_1:def_3; ::_thesis: ( i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) thus i in Seg k1 by A76, A78, FINSEQ_1:1; ::_thesis: ( i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) i <= k1 by A77, NAT_1:13; then i - 1 <= k1 - 1 by XREAL_1:9; then A79: (i - 1) + 0 <= (k1 - 1) + 1 by XREAL_1:7; ex j being Nat st i = 1 + j by A76, NAT_1:10; hence i - 1 in Seg k1 by A75, A79, FINSEQ_1:1; ::_thesis: ( (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) then A80: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by A29, FINSEQ_1:39; thus (i - 1) + 1 = i ; ::_thesis: i - (len <*(f . (lower_bound A))*>) in dom s2 thus i - (len <*(f . (lower_bound A))*>) in dom s2 by A80, FINSEQ_1:def_3; ::_thesis: verum end; then A81: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by FINSEQ_1:def_3; then i - (len <*(f . (lower_bound A))*>) <= len s2 by FINSEQ_1:1; then A82: i <= (len <*(f . (lower_bound A))*>) + (len s2) by XREAL_1:20; 1 <= i - (len <*(f . (lower_bound A))*>) by A81, FINSEQ_1:1; then (len <*(f . (lower_bound A))*>) + 1 <= i by XREAL_1:19; then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - (len <*(f . (lower_bound A))*>)) by A82, FINSEQ_1:23; then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:39; then A83: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) by A29, A40, A74; (s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by A74, FINSEQ_1:def_7; then (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) by A39, A74; hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A4, A19, A44, A45, A73, A83; ::_thesis: verum end; end; end; hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ; ::_thesis: verum end; end; end; hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ; ::_thesis: verum end; then Sum p = (Sum (s1 ^ <*(f . (upper_bound A))*>)) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by INTEGRA1:22; then Sum p = ((Sum s1) + (f . (upper_bound A))) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by RVSUM_1:74; then A84: Sum p = ((Sum s1) + (f . (upper_bound A))) - ((f . (lower_bound A)) + (Sum s2)) by RVSUM_1:76; A85: dom s1 = Seg k1 by A39, FINSEQ_1:def_3; A86: dom s1 = Seg k1 by A39, FINSEQ_1:def_3; for i being Nat st i in dom s1 holds s1 . i = s2 . i proof let i be Nat; ::_thesis: ( i in dom s1 implies s1 . i = s2 . i ) assume A87: i in dom s1 ; ::_thesis: s1 . i = s2 . i then s1 . i = f . (upper_bound (divset (D,i))) by A39; then s1 . i = f . (lower_bound (divset (D,(i + 1)))) by A20, A85, A87; hence s1 . i = s2 . i by A86, A29, A40, A87; ::_thesis: verum end; then A88: s1 = s2 by A39, A29, FINSEQ_2:9; A89: for k being Element of NAT for r being Real st k in dom D & r in divset (D,k) holds diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) proof A90: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61 .= X /\ A by A2, FDIFF_1:def_7 .= A by A1, XBOOLE_1:28 ; let k be Element of NAT ; ::_thesis: for r being Real st k in dom D & r in divset (D,k) holds diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) let r be Real; ::_thesis: ( k in dom D & r in divset (D,k) implies diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) ) assume that A91: k in dom D and A92: r in divset (D,k) ; ::_thesis: diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) A93: divset (D,k) c= A by A91, INTEGRA1:8; then divset (D,k) c= X by A1, XBOOLE_1:1; then (f `| X) . r = diff (f,r) by A2, A92, FDIFF_1:def_7; then A94: diff (f,r) = ((f `| X) || A) . r by A92, A93, A90, FUNCT_1:47; A95: dom (((f `| X) || A) | (divset (D,k))) = A /\ (divset (D,k)) by A90, RELAT_1:61 .= divset (D,k) by A91, INTEGRA1:8, XBOOLE_1:28 ; then (((f `| X) || A) | (divset (D,k))) . r in rng (((f `| X) || A) | (divset (D,k))) by A92, FUNCT_1:def_3; hence diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A92, A94, A95, FUNCT_1:47; ::_thesis: verum end; A96: for k being Element of NAT st k in dom D holds (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k proof let k be Element of NAT ; ::_thesis: ( k in dom D implies (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k ) A97: vol (divset (D,k)) >= 0 by INTEGRA1:9; assume A98: k in dom D ; ::_thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k then consider r being Real such that A99: r in divset (D,k) and A100: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6; A101: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A98; diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A89, A98, A99; then diff (f,r) <= upper_bound (rng (((f `| X) || A) | (divset (D,k)))) by A101, SEQ_4:def_1; then (diff (f,r)) * (vol (divset (D,k))) <= (upper_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) by A97, XREAL_1:64; hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k by A98, A100, INTEGRA1:def_6; ::_thesis: verum end; A102: (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) proof len (upper_volume (((f `| X) || A),D)) = len D by INTEGRA1:def_6; then reconsider q = upper_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; A103: for k being Nat st k in Seg (len D) holds p . k <= (upper_volume (((f `| X) || A),D)) . k proof let k be Nat; ::_thesis: ( k in Seg (len D) implies p . k <= (upper_volume (((f `| X) || A),D)) . k ) assume k in Seg (len D) ; ::_thesis: p . k <= (upper_volume (((f `| X) || A),D)) . k then ( (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = p . k & k in dom D ) by A4, A19, FINSEQ_1:def_3; hence p . k <= (upper_volume (((f `| X) || A),D)) . k by A96; ::_thesis: verum end; reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92; Sum p <= Sum q by A103, RVSUM_1:82; hence (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) by A88, A84, INTEGRA1:def_8; ::_thesis: verum end; A104: for k being Element of NAT st k in dom D holds (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k proof let k be Element of NAT ; ::_thesis: ( k in dom D implies (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k ) assume A105: k in dom D ; ::_thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k then A106: ( vol (divset (D,k)) >= 0 & (lower_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) = (lower_volume (((f `| X) || A),D)) . k ) by INTEGRA1:9, INTEGRA1:def_7; A107: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A105; consider r being Real such that A108: r in divset (D,k) and A109: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6, A105; diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A89, A105, A108; then diff (f,r) >= lower_bound (rng (((f `| X) || A) | (divset (D,k)))) by A107, SEQ_4:def_2; hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k by A109, A106, XREAL_1:64; ::_thesis: verum end; (f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D) proof len (lower_volume (((f `| X) || A),D)) = len D by INTEGRA1:def_7; then reconsider q = lower_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; A110: for k being Nat st k in Seg (len D) holds p . k >= (lower_volume (((f `| X) || A),D)) . k proof let k be Nat; ::_thesis: ( k in Seg (len D) implies p . k >= (lower_volume (((f `| X) || A),D)) . k ) assume k in Seg (len D) ; ::_thesis: p . k >= (lower_volume (((f `| X) || A),D)) . k then ( (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = p . k & k in dom D ) by A4, A19, FINSEQ_1:def_3; hence p . k >= (lower_volume (((f `| X) || A),D)) . k by A104; ::_thesis: verum end; reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92; Sum q <= Sum p by A110, RVSUM_1:82; hence (f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D) by A88, A84, INTEGRA1:def_9; ::_thesis: verum end; hence ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) by A102; ::_thesis: verum end; theorem Th13: :: INTEGRA5:13 for A being non empty closed_interval Subset of REAL for X being set for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: ( A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded implies integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) ) assume that A1: ( A c= X & f is_differentiable_on X ) and A2: f `| X is_integrable_on A and A3: (f `| X) | A is bounded ; ::_thesis: integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) (f `| X) || A is integrable by A2, Def1; then A4: upper_integral ((f `| X) || A) = lower_integral ((f `| X) || A) by INTEGRA1:def_16; A5: for r being real number st r in rng (upper_sum_set ((f `| X) || A)) holds (f . (upper_bound A)) - (f . (lower_bound A)) <= r proof let r be real number ; ::_thesis: ( r in rng (upper_sum_set ((f `| X) || A)) implies (f . (upper_bound A)) - (f . (lower_bound A)) <= r ) assume r in rng (upper_sum_set ((f `| X) || A)) ; ::_thesis: (f . (upper_bound A)) - (f . (lower_bound A)) <= r then consider D being Element of divs A such that A6: ( D in dom (upper_sum_set ((f `| X) || A)) & r = (upper_sum_set ((f `| X) || A)) . D ) by PARTFUN1:3; reconsider D = D as Division of A by INTEGRA1:def_3; r = upper_sum (((f `| X) || A),D) by A6, INTEGRA1:def_10; hence (f . (upper_bound A)) - (f . (lower_bound A)) <= r by A1, A3, Th12; ::_thesis: verum end; (f . (upper_bound A)) - (f . (lower_bound A)) <= lower_bound (rng (upper_sum_set ((f `| X) || A))) by A5, SEQ_4:43; then A7: upper_integral ((f `| X) || A) >= (f . (upper_bound A)) - (f . (lower_bound A)) by INTEGRA1:def_14; A8: for r being real number st r in rng (lower_sum_set ((f `| X) || A)) holds r <= (f . (upper_bound A)) - (f . (lower_bound A)) proof let r be real number ; ::_thesis: ( r in rng (lower_sum_set ((f `| X) || A)) implies r <= (f . (upper_bound A)) - (f . (lower_bound A)) ) assume r in rng (lower_sum_set ((f `| X) || A)) ; ::_thesis: r <= (f . (upper_bound A)) - (f . (lower_bound A)) then consider D being Element of divs A such that A9: ( D in dom (lower_sum_set ((f `| X) || A)) & r = (lower_sum_set ((f `| X) || A)) . D ) by PARTFUN1:3; reconsider D = D as Division of A by INTEGRA1:def_3; r = lower_sum (((f `| X) || A),D) by A9, INTEGRA1:def_11; hence r <= (f . (upper_bound A)) - (f . (lower_bound A)) by A1, A3, Th12; ::_thesis: verum end; upper_bound (rng (lower_sum_set ((f `| X) || A))) <= (f . (upper_bound A)) - (f . (lower_bound A)) by A8, SEQ_4:45; then upper_integral ((f `| X) || A) <= (f . (upper_bound A)) - (f . (lower_bound A)) by A4, INTEGRA1:def_15; then upper_integral ((f `| X) || A) = (f . (upper_bound A)) - (f . (lower_bound A)) by A7, XXREAL_0:1; hence integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) by INTEGRA1:def_17; ::_thesis: verum end; theorem Th14: :: INTEGRA5:14 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds rng (f | A) is real-bounded proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds rng (f | A) is real-bounded let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is non-decreasing & A c= dom f implies rng (f | A) is real-bounded ) assume that A1: f | A is non-decreasing and A2: A c= dom f ; ::_thesis: rng (f | A) is real-bounded A3: dom (f | A) = (dom f) /\ A by RELAT_1:61 .= A by A2, XBOOLE_1:28 ; f . (lower_bound A) is LowerBound of rng (f | A) proof lower_bound A <= upper_bound A by SEQ_4:11; then lower_bound A in dom (f | A) by A3, INTEGRA2:1; then A4: lower_bound A in (dom f) /\ A by RELAT_1:61; let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not y in rng (f | A) or f . (lower_bound A) <= y ) assume y in rng (f | A) ; ::_thesis: f . (lower_bound A) <= y then consider x being Real such that A5: x in dom (f | A) and A6: y = (f | A) . x by PARTFUN1:3; A7: x in (dom f) /\ A by A5, RELAT_1:61; ( y = f . x & x >= lower_bound A ) by A5, A6, FUNCT_1:47, INTEGRA2:1; hence f . (lower_bound A) <= y by A1, A7, A4, RFUNCT_2:24; ::_thesis: verum end; then A8: rng (f | A) is bounded_below by XXREAL_2:def_9; f . (upper_bound A) is UpperBound of rng (f | A) proof lower_bound A <= upper_bound A by SEQ_4:11; then upper_bound A in dom (f | A) by A3, INTEGRA2:1; then A9: upper_bound A in (dom f) /\ A by RELAT_1:61; let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not y in rng (f | A) or y <= f . (upper_bound A) ) assume y in rng (f | A) ; ::_thesis: y <= f . (upper_bound A) then consider x being Real such that A10: x in dom (f | A) and A11: y = (f | A) . x by PARTFUN1:3; A12: x in (dom f) /\ A by A10, RELAT_1:61; ( y = f . x & x <= upper_bound A ) by A10, A11, FUNCT_1:47, INTEGRA2:1; hence y <= f . (upper_bound A) by A1, A12, A9, RFUNCT_2:24; ::_thesis: verum end; then rng (f | A) is bounded_above by XXREAL_2:def_10; hence rng (f | A) is real-bounded by A8; ::_thesis: verum end; theorem Th15: :: INTEGRA5:15 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is non-decreasing & A c= dom f implies ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) ) assume that A1: f | A is non-decreasing and A2: A c= dom f ; ::_thesis: ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) A3: dom (f | A) = (dom f) /\ A by RELAT_1:61 .= A by A2, XBOOLE_1:28 ; then A4: rng (f | A) <> {} by RELAT_1:42; A5: lower_bound A <= upper_bound A by SEQ_4:11; then A6: upper_bound A in dom (f | A) by A3, INTEGRA2:1; then A7: upper_bound A in (dom f) /\ A by RELAT_1:61; A8: for x being real number st x in rng (f | A) holds x <= f . (upper_bound A) proof let y be real number ; ::_thesis: ( y in rng (f | A) implies y <= f . (upper_bound A) ) assume y in rng (f | A) ; ::_thesis: y <= f . (upper_bound A) then consider x being Real such that A9: x in dom (f | A) and A10: y = (f | A) . x by PARTFUN1:3; ( x in (dom f) /\ A & upper_bound A >= x ) by A9, INTEGRA2:1, RELAT_1:61; then f . (upper_bound A) >= f . x by A1, A7, RFUNCT_2:24; hence y <= f . (upper_bound A) by A9, A10, FUNCT_1:47; ::_thesis: verum end; A11: lower_bound A in dom (f | A) by A3, A5, INTEGRA2:1; then A12: lower_bound A in (dom f) /\ A by RELAT_1:61; A13: for y being real number st y in rng (f | A) holds y >= f . (lower_bound A) proof let y be real number ; ::_thesis: ( y in rng (f | A) implies y >= f . (lower_bound A) ) assume y in rng (f | A) ; ::_thesis: y >= f . (lower_bound A) then consider x being Real such that A14: x in dom (f | A) and A15: y = (f | A) . x by PARTFUN1:3; ( x in (dom f) /\ A & lower_bound A <= x ) by A14, INTEGRA2:1, RELAT_1:61; then f . (lower_bound A) <= f . x by A1, A12, RFUNCT_2:24; hence y >= f . (lower_bound A) by A14, A15, FUNCT_1:47; ::_thesis: verum end; for a being real number st ( for x being real number st x in rng (f | A) holds x >= a ) holds f . (lower_bound A) >= a proof let a be real number ; ::_thesis: ( ( for x being real number st x in rng (f | A) holds x >= a ) implies f . (lower_bound A) >= a ) assume A16: for x being real number st x in rng (f | A) holds x >= a ; ::_thesis: f . (lower_bound A) >= a ( f . (lower_bound A) = (f | A) . (lower_bound A) & (f | A) . (lower_bound A) in rng (f | A) ) by A11, FUNCT_1:47, FUNCT_1:def_3; hence f . (lower_bound A) >= a by A16; ::_thesis: verum end; hence lower_bound (rng (f | A)) = f . (lower_bound A) by A4, A13, SEQ_4:44; ::_thesis: upper_bound (rng (f | A)) = f . (upper_bound A) for a being real number st ( for x being real number st x in rng (f | A) holds x <= a ) holds f . (upper_bound A) <= a proof let a be real number ; ::_thesis: ( ( for x being real number st x in rng (f | A) holds x <= a ) implies f . (upper_bound A) <= a ) assume A17: for x being real number st x in rng (f | A) holds x <= a ; ::_thesis: f . (upper_bound A) <= a ( f . (upper_bound A) = (f | A) . (upper_bound A) & (f | A) . (upper_bound A) in rng (f | A) ) by A6, FUNCT_1:47, FUNCT_1:def_3; hence f . (upper_bound A) <= a by A17; ::_thesis: verum end; hence upper_bound (rng (f | A)) = f . (upper_bound A) by A4, A8, SEQ_4:46; ::_thesis: verum end; Lm1: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds f is_integrable_on A proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds f is_integrable_on A let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is non-decreasing & A c= dom f implies f is_integrable_on A ) assume that A1: f | A is non-decreasing and A2: A c= dom f ; ::_thesis: f is_integrable_on A A3: for D being Division of A for k being Element of NAT st k in dom D holds ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) ) proof let D be Division of A; ::_thesis: for k being Element of NAT st k in dom D holds ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) ) let k be Element of NAT ; ::_thesis: ( k in dom D implies ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) ) ) assume A4: k in dom D ; ::_thesis: ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) ) then A5: ( (upper_volume ((f || A),D)) . k = (upper_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) & (lower_volume ((f || A),D)) . k = (lower_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) ) by INTEGRA1:def_6, INTEGRA1:def_7; k in Seg (len D) by A4, FINSEQ_1:def_3; then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then A6: k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; vol (divset (D,k)) = (upper_volume ((chi (A,A)),D)) . k by A4, INTEGRA1:20; then vol (divset (D,k)) in rng (upper_volume ((chi (A,A)),D)) by A6, FUNCT_1:def_3; then vol (divset (D,k)) <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def_8; then A7: vol (divset (D,k)) <= delta D by INTEGRA3:def_1; A8: divset (D,k) c= A by A4, INTEGRA1:8; then A9: divset (D,k) c= dom f by A2, XBOOLE_1:1; f | (divset (D,k)) is non-decreasing by A1, A4, INTEGRA1:8, RFUNCT_2:30; then A10: ( lower_bound (rng (f | (divset (D,k)))) = f . (lower_bound (divset (D,k))) & upper_bound (rng (f | (divset (D,k)))) = f . (upper_bound (divset (D,k))) ) by A9, Th15; dom (f | (divset (D,k))) = (dom f) /\ (divset (D,k)) by RELAT_1:61 .= divset (D,k) by A2, A8, XBOOLE_1:1, XBOOLE_1:28 ; then A11: rng (f | (divset (D,k))) <> {} by RELAT_1:42; A12: rng (f | (divset (D,k))) = rng ((f || A) | (divset (D,k))) by A8, FUNCT_1:51; rng (f | A) is real-bounded by A1, A2, Th14; then rng (f | (divset (D,k))) is real-bounded by A12, RELAT_1:70, XXREAL_2:45; then A13: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= 0 by A10, A11, SEQ_4:11, XREAL_1:48; vol (divset (D,k)) >= 0 by INTEGRA1:9; then 0 * (vol (divset (D,k))) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A13; hence 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) by A10, A5, A12; ::_thesis: ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A10, A5, A12; hence ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A13, A7, XREAL_1:64; ::_thesis: verum end; A14: for D being Division of A holds ( (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 ) proof let D be Division of A; ::_thesis: ( (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 ) deffunc H1( Nat) -> Element of REAL = f . (upper_bound (divset (D,$1))); consider F1 being FinSequence of REAL such that A15: ( len F1 = len D & ( for i being Nat st i in dom F1 holds F1 . i = H1(i) ) ) from FINSEQ_2:sch_1(); (len D) - 1 in NAT proof ex j being Nat st len D = 1 + j by NAT_1:10, NAT_1:14; hence (len D) - 1 in NAT by ORDINAL1:def_12; ::_thesis: verum end; then consider k1 being Element of NAT such that A16: k1 = (len D) - 1 ; deffunc H2( Nat) -> Element of REAL = f . (lower_bound (divset (D,$1))); consider F2 being FinSequence of REAL such that A17: ( len F2 = len D & ( for i being Nat st i in dom F2 holds F2 . i = H2(i) ) ) from FINSEQ_2:sch_1(); deffunc H3( Nat) -> Element of REAL = f . (upper_bound (divset (D,$1))); A18: dom F2 = Seg (len D) by A17, FINSEQ_1:def_3; consider F being FinSequence of REAL such that A19: ( len F = k1 & ( for i being Nat st i in dom F holds F . i = H3(i) ) ) from FINSEQ_2:sch_1(); A20: dom F = Seg k1 by A19, FINSEQ_1:def_3; A21: for i being Nat st 1 <= i & i <= len F2 holds F2 . i = (<*(f . (lower_bound A))*> ^ F) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len F2 implies F2 . i = (<*(f . (lower_bound A))*> ^ F) . i ) assume that A22: 1 <= i and A23: i <= len F2 ; ::_thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i percases ( i = 1 or i <> 1 ) ; supposeA24: i = 1 ; ::_thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i A25: i in Seg (len D) by A17, A22, A23, FINSEQ_1:1; then A26: i in dom D by FINSEQ_1:def_3; F2 . i = f . (lower_bound (divset (D,i))) by A17, A18, A25 .= f . (lower_bound A) by A24, A26, INTEGRA1:def_4 ; hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A24, FINSEQ_1:41; ::_thesis: verum end; supposeA27: i <> 1 ; ::_thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i then A28: i > 1 by A22, XXREAL_0:1; then 1 + 1 <= i by NAT_1:13; then A29: (len <*(f . (lower_bound A))*>) + 1 <= i by FINSEQ_1:39; A30: i in Seg (len D) by A17, A22, A23, FINSEQ_1:1; then A31: i in dom D by FINSEQ_1:def_3; then reconsider k2 = i - 1 as Element of NAT by A27, INTEGRA1:7; 1 + 1 <= k2 + 1 by A28, NAT_1:13; then A32: 1 <= k2 by XREAL_1:19; k2 + 1 <= len F2 by A23; then A33: k2 <= (len D) - 1 by A17, XREAL_1:19; then A34: k2 in Seg k1 by A16, A32, FINSEQ_1:1; A35: upper_bound (divset (D,k2)) = D . (i - 1) proof len D <= (len D) + 1 by NAT_1:13; then (len D) - 1 <= len D by XREAL_1:20; then k2 <= len D by A33, XXREAL_0:2; then k2 in Seg (len D) by A32, FINSEQ_1:1; then A36: k2 in dom D by FINSEQ_1:def_3; percases ( k2 = 1 or k2 <> 1 ) ; suppose k2 = 1 ; ::_thesis: upper_bound (divset (D,k2)) = D . (i - 1) hence upper_bound (divset (D,k2)) = D . (i - 1) by A36, INTEGRA1:def_4; ::_thesis: verum end; suppose k2 <> 1 ; ::_thesis: upper_bound (divset (D,k2)) = D . (i - 1) hence upper_bound (divset (D,k2)) = D . (i - 1) by A36, INTEGRA1:def_4; ::_thesis: verum end; end; end; len F2 = 1 + ((len D) - 1) by A17 .= (len <*(f . (lower_bound A))*>) + (len F) by A16, A19, FINSEQ_1:39 ; then A37: (<*(f . (lower_bound A))*> ^ F) . i = F . (i - (len <*(f . (lower_bound A))*>)) by A23, A29, FINSEQ_1:23 .= F . (i - 1) by FINSEQ_1:39 ; F2 . i = f . (lower_bound (divset (D,i))) by A17, A18, A30 .= f . (D . (i - 1)) by A27, A31, INTEGRA1:def_4 ; hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A19, A20, A37, A34, A35; ::_thesis: verum end; end; end; len (<*(f . (lower_bound A))*> ^ F) = (len <*(f . (lower_bound A))*>) + (len F) by FINSEQ_1:22 .= 1 + ((len D) - 1) by A16, A19, FINSEQ_1:39 .= len D ; then A38: F2 = <*(f . (lower_bound A))*> ^ F by A17, A21, FINSEQ_1:14; ( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def_6, INTEGRA1:def_7; then A39: Sum ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = (Sum (upper_volume ((f || A),D))) - (Sum (lower_volume ((f || A),D))) by Th2 .= (upper_sum ((f || A),D)) - (Sum (lower_volume ((f || A),D))) by INTEGRA1:def_8 .= (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) by INTEGRA1:def_9 ; A40: dom F1 = Seg (len D) by A15, FINSEQ_1:def_3; A41: for i being Nat st 1 <= i & i <= len F1 holds F1 . i = (F ^ <*(f . (upper_bound A))*>) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len F1 implies F1 . i = (F ^ <*(f . (upper_bound A))*>) . i ) assume that A42: 1 <= i and A43: i <= len F1 ; ::_thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i now__::_thesis:_F1_._i_=_(F_^_<*(f_._(upper_bound_A))*>)_._i percases ( i <= len F or i > len F ) ; suppose i <= len F ; ::_thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i then i in Seg (len F) by A42, FINSEQ_1:1; then A44: ( F . i = f . (upper_bound (divset (D,i))) & i in dom F ) by A19, A20; i in Seg (len F1) by A42, A43, FINSEQ_1:1; then F1 . i = f . (upper_bound (divset (D,i))) by A15, A40; hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A44, FINSEQ_1:def_7; ::_thesis: verum end; suppose i > len F ; ::_thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i then A45: i >= (len F) + 1 by NAT_1:13; then A46: i = (len F) + 1 by A15, A16, A19, A43, XXREAL_0:1; A47: i in Seg (len F1) by A42, A43, FINSEQ_1:1; then A48: i in dom D by A15, FINSEQ_1:def_3; A49: upper_bound (divset (D,i)) = D . i proof now__::_thesis:_upper_bound_(divset_(D,i))_=_D_._i percases ( i = 1 or i <> 1 ) ; suppose i = 1 ; ::_thesis: upper_bound (divset (D,i)) = D . i hence upper_bound (divset (D,i)) = D . i by A48, INTEGRA1:def_4; ::_thesis: verum end; suppose i <> 1 ; ::_thesis: upper_bound (divset (D,i)) = D . i hence upper_bound (divset (D,i)) = D . i by A48, INTEGRA1:def_4; ::_thesis: verum end; end; end; hence upper_bound (divset (D,i)) = D . i ; ::_thesis: verum end; F1 . i = f . (upper_bound (divset (D,i))) by A15, A40, A47; then F1 . i = f . (D . (len D)) by A15, A16, A19, A43, A45, A49, XXREAL_0:1 .= f . (upper_bound A) by INTEGRA1:def_2 ; hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A46, FINSEQ_1:42; ::_thesis: verum end; end; end; hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i ; ::_thesis: verum end; ( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def_6, INTEGRA1:def_7; then A50: len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = len D by Th2; A51: len (F1 - F2) = len D by A15, A17, Th2; A52: for k being Element of NAT st k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) holds ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k proof let k be Element of NAT ; ::_thesis: ( k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) implies ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k ) assume A53: k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) ; ::_thesis: ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k then k in Seg (len (F1 - F2)) by A50, A51, FINSEQ_1:def_3; then A54: k in dom (F1 - F2) by FINSEQ_1:def_3; A55: k in Seg (len D) by A50, A53, FINSEQ_1:def_3; then k in dom D by FINSEQ_1:def_3; then ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A3; then A56: ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A53, VALUED_1:13; ( F1 . k = f . (upper_bound (divset (D,k))) & F2 . k = f . (lower_bound (divset (D,k))) ) by A15, A40, A17, A18, A55; then ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= (delta D) * ((F1 - F2) . k) by A56, A54, VALUED_1:13; hence ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k by RVSUM_1:44; ::_thesis: verum end; (delta D) * (F1 - F2) = ((delta D) multreal) * (F1 - F2) by RVSUM_1:def_7; then len ((delta D) * (F1 - F2)) = len (F1 - F2) by FINSEQ_2:33; then len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = len ((delta D) * (F1 - F2)) by A15, A17, A50, Th2; then A57: Sum ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) <= Sum ((delta D) * (F1 - F2)) by A52, Th3; len (F ^ <*(f . (upper_bound A))*>) = (len F) + (len <*(f . (upper_bound A))*>) by FINSEQ_1:22 .= ((len D) - 1) + 1 by A16, A19, FINSEQ_1:39 .= len D ; then F1 = F ^ <*(f . (upper_bound A))*> by A15, A41, FINSEQ_1:14; then Sum (F1 - F2) = (f . (upper_bound A)) - (f . (lower_bound A)) by A38, Th1; hence (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) by A39, A57, RVSUM_1:87; ::_thesis: (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 for k being Nat st k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) holds 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k proof let k be Nat; ::_thesis: ( k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) implies 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k ) set r = ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k; A58: ( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def_6, INTEGRA1:def_7; assume A59: k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) ; ::_thesis: 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k then k in Seg (len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D)))) by FINSEQ_1:def_3; then k in Seg (len D) by A58, Th2; then A60: k in dom D by FINSEQ_1:def_3; ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k = ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) by A59, VALUED_1:13; hence 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k by A3, A60; ::_thesis: verum end; hence (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 by A39, RVSUM_1:84; ::_thesis: verum end; A61: ( f || A is total & (f || A) | A is bounded ) proof consider x being Real such that A62: x in A by SUBSET_1:4; A63: dom (f || A) = (dom f) /\ A by RELAT_1:61 .= A by A2, XBOOLE_1:28 ; hence f || A is total by PARTFUN1:def_2; ::_thesis: (f || A) | A is bounded ( lower_bound A <= x & x <= upper_bound A ) by A62, INTEGRA2:1; then A64: lower_bound A <= upper_bound A by XXREAL_0:2; for x being set st x in A /\ (dom (f || A)) holds (f || A) . x >= (f || A) . (lower_bound A) proof lower_bound A in A by A64, INTEGRA2:1; then A65: ( lower_bound A in A /\ (dom f) & f . (lower_bound A) = (f | A) . (lower_bound A) ) by A2, A63, FUNCT_1:47, XBOOLE_1:28; let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x >= (f || A) . (lower_bound A) ) assume A66: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x >= (f || A) . (lower_bound A) then x in A ; then A67: x in A /\ (dom f) by A2, XBOOLE_1:28; reconsider x = x as Element of A by A66; ( x >= lower_bound A & f . x = (f | A) . x ) by A63, FUNCT_1:47, INTEGRA2:1; hence (f || A) . x >= (f || A) . (lower_bound A) by A1, A67, A65, RFUNCT_2:24; ::_thesis: verum end; then A68: (f || A) | A is bounded_below by RFUNCT_1:71; for x being set st x in A /\ (dom (f || A)) holds (f || A) . x <= (f || A) . (upper_bound A) proof upper_bound A in A by A64, INTEGRA2:1; then A69: ( upper_bound A in A /\ (dom f) & f . (upper_bound A) = (f | A) . (upper_bound A) ) by A2, A63, FUNCT_1:47, XBOOLE_1:28; let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x <= (f || A) . (upper_bound A) ) assume A70: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x <= (f || A) . (upper_bound A) then x in A ; then A71: x in A /\ (dom f) by A2, XBOOLE_1:28; reconsider x = x as Element of A by A70; ( x <= upper_bound A & f . x = (f | A) . x ) by A63, FUNCT_1:47, INTEGRA2:1; hence (f || A) . x <= (f || A) . (upper_bound A) by A1, A71, A69, RFUNCT_2:24; ::_thesis: verum end; then (f || A) | A is bounded_above by RFUNCT_1:70; hence (f || A) | A is bounded by A68; ::_thesis: verum end; for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 proof let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 ) assume A72: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 A73: for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r proof consider x being Real such that A74: x in A by SUBSET_1:4; A75: A = A /\ (dom f) by A2, XBOOLE_1:28; let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ) assume A76: 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ( lower_bound A <= x & x <= upper_bound A ) by A74, INTEGRA2:1; then A77: lower_bound A <= upper_bound A by XXREAL_0:2; then ( lower_bound A in A & upper_bound A in A ) by INTEGRA2:1; then A78: f . (lower_bound A) <= f . (upper_bound A) by A1, A77, A75, RFUNCT_2:24; now__::_thesis:_ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((((upper_sum_((f_||_A),T))_-_(lower_sum_((f_||_A),T)))_._m)_-_0)_<_r percases ( f . (lower_bound A) = f . (upper_bound A) or f . (lower_bound A) < f . (upper_bound A) ) by A78, XXREAL_0:1; supposeA79: f . (lower_bound A) = f . (upper_bound A) ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r for m being Element of NAT st 0 <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r proof let m be Element of NAT ; ::_thesis: ( 0 <= m implies abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ) assume 0 <= m ; ::_thesis: abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r reconsider D1 = T . m as Division of A ; A80: ((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m = ((upper_sum ((f || A),T)) . m) + ((- (lower_sum ((f || A),T))) . m) by SEQ_1:7 .= ((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m)) by SEQ_1:10 .= (upper_sum ((f || A),D1)) + (- ((lower_sum ((f || A),T)) . m)) by INTEGRA2:def_2 .= (upper_sum ((f || A),D1)) + (- (lower_sum ((f || A),D1))) by INTEGRA2:def_3 ; ( (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) <= (delta D1) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) >= 0 ) by A14; hence abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r by A76, A79, A80, ABSVALUE:def_1; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ; ::_thesis: verum end; suppose f . (lower_bound A) < f . (upper_bound A) ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r then A81: (f . (upper_bound A)) - (f . (lower_bound A)) > 0 by XREAL_1:50; then r / ((f . (upper_bound A)) - (f . (lower_bound A))) > 0 by A76, XREAL_1:139; then consider n being Element of NAT such that A82: for m being Element of NAT st n <= m holds abs (((delta T) . m) - 0) < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A72, SEQ_2:def_7; A83: for m being Element of NAT st n <= m holds (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) proof let m be Element of NAT ; ::_thesis: ( n <= m implies (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) ) assume n <= m ; ::_thesis: (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) then A84: abs (((delta T) . m) - 0) < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A82; (delta T) . m <= abs ((delta T) . m) by ABSVALUE:4; hence (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A84, XXREAL_0:2; ::_thesis: verum end; for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r proof let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ) reconsider D = T . m as Division of A ; A85: abs ((upper_sum ((f || A),D)) - (lower_sum ((f || A),D))) = abs ((((upper_sum ((f || A),T)) . m) - (lower_sum ((f || A),D))) - 0) by INTEGRA2:def_2 .= abs ((((upper_sum ((f || A),T)) . m) - ((lower_sum ((f || A),T)) . m)) - 0) by INTEGRA2:def_3 .= abs ((((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m))) - 0) .= abs ((((upper_sum ((f || A),T)) . m) + ((- (lower_sum ((f || A),T))) . m)) - 0) by SEQ_1:10 .= abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) by SEQ_1:7 ; assume n <= m ; ::_thesis: abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r then (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A83; then ((delta T) . m) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by A81, XREAL_1:79; then A86: (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by INTEGRA3:def_2; (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) by A14; then A87: (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) < r by A86, XXREAL_0:2; (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 by A14; hence abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r by A87, A85, ABSVALUE:def_1; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ; ::_thesis: verum end; end; end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ; ::_thesis: verum end; A88: ( upper_sum ((f || A),T) is convergent & lower_sum ((f || A),T) is convergent ) by A61, A72, INTEGRA4:8, INTEGRA4:9; then (upper_sum ((f || A),T)) - (lower_sum ((f || A),T)) is convergent ; then lim ((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) = 0 by A73, SEQ_2:def_7; hence (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 by A88, SEQ_2:12; ::_thesis: verum end; then f || A is integrable by A61, INTEGRA4:12; hence f is_integrable_on A by Def1; ::_thesis: verum end; theorem :: INTEGRA5:16 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st f | A is monotone & A c= dom f holds f is_integrable_on A proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is monotone & A c= dom f holds f is_integrable_on A let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is monotone & A c= dom f implies f is_integrable_on A ) assume that A1: f | A is monotone and A2: A c= dom f ; ::_thesis: f is_integrable_on A percases ( f | A is non-decreasing or f | A is non-increasing ) by A1, RFUNCT_2:def_5; suppose f | A is non-decreasing ; ::_thesis: f is_integrable_on A hence f is_integrable_on A by A2, Lm1; ::_thesis: verum end; suppose f | A is non-increasing ; ::_thesis: f is_integrable_on A then A3: ((- 1) (#) f) | A is non-decreasing by RFUNCT_2:35; A4: ( (- f) || A is total & ((- f) || A) | A is bounded ) proof consider x being Real such that A5: x in A by SUBSET_1:4; A6: dom ((- f) || A) = (dom (- f)) /\ A by RELAT_1:61 .= (dom f) /\ A by VALUED_1:8 .= A by A2, XBOOLE_1:28 ; hence (- f) || A is total by PARTFUN1:def_2; ::_thesis: ((- f) || A) | A is bounded ( lower_bound A <= x & x <= upper_bound A ) by A5, INTEGRA2:1; then A7: lower_bound A <= upper_bound A by XXREAL_0:2; for x being set st x in A /\ (dom ((- f) || A)) holds ((- f) || A) . x >= ((- f) || A) . (lower_bound A) proof let x be set ; ::_thesis: ( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x >= ((- f) || A) . (lower_bound A) ) assume x in A /\ (dom ((- f) || A)) ; ::_thesis: ((- f) || A) . x >= ((- f) || A) . (lower_bound A) then reconsider x = x as Element of A ; A8: ( x >= lower_bound A & (- f) . x = ((- f) | A) . x ) by A6, FUNCT_1:47, INTEGRA2:1; lower_bound A in A by A7, INTEGRA2:1; then A9: (- f) . (lower_bound A) = ((- f) | A) . (lower_bound A) by A6, FUNCT_1:47; A10: A = A /\ (dom f) by A2, XBOOLE_1:28 .= A /\ (dom (- f)) by VALUED_1:8 ; then lower_bound A in A /\ (dom (- f)) by A7, INTEGRA2:1; hence ((- f) || A) . x >= ((- f) || A) . (lower_bound A) by A3, A10, A8, A9, RFUNCT_2:24; ::_thesis: verum end; then A11: ((- f) || A) | A is bounded_below by RFUNCT_1:71; for x being set st x in A /\ (dom ((- f) || A)) holds ((- f) || A) . x <= ((- f) || A) . (upper_bound A) proof let x be set ; ::_thesis: ( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x <= ((- f) || A) . (upper_bound A) ) assume x in A /\ (dom ((- f) || A)) ; ::_thesis: ((- f) || A) . x <= ((- f) || A) . (upper_bound A) then reconsider x = x as Element of A ; A12: ( x <= upper_bound A & (- f) . x = ((- f) | A) . x ) by A6, FUNCT_1:47, INTEGRA2:1; upper_bound A in A by A7, INTEGRA2:1; then A13: (- f) . (upper_bound A) = ((- f) | A) . (upper_bound A) by A6, FUNCT_1:47; A14: A = A /\ (dom f) by A2, XBOOLE_1:28 .= A /\ (dom (- f)) by VALUED_1:8 ; then upper_bound A in A /\ (dom (- f)) by A7, INTEGRA2:1; hence ((- f) || A) . x <= ((- f) || A) . (upper_bound A) by A3, A14, A12, A13, RFUNCT_2:24; ::_thesis: verum end; then ((- f) || A) | A is bounded_above by RFUNCT_1:70; hence ((- f) || A) | A is bounded by A11; ::_thesis: verum end; dom f = dom (- f) by VALUED_1:8; then - f is_integrable_on A by A2, A3, Lm1; then (- f) || A is integrable by Def1; then A15: (- 1) (#) ((- f) || A) is integrable by A4, INTEGRA2:31; A16: dom ((- f) || A) = (dom (- f)) /\ A by RELAT_1:61 .= (dom f) /\ A by VALUED_1:8 .= A by A2, XBOOLE_1:28 ; then A17: A = dom ((- 1) (#) ((- f) || A)) by VALUED_1:def_5; A18: dom (f || A) = (dom f) /\ A by RELAT_1:61; then A19: dom (f || A) = A by A2, XBOOLE_1:28; A20: dom ((- 1) (#) ((- f) || A)) = A by A16, VALUED_1:def_5; A21: for z being Element of A st z in A holds ((- 1) (#) ((- f) || A)) . z = (f || A) . z proof let z be Element of A; ::_thesis: ( z in A implies ((- 1) (#) ((- f) || A)) . z = (f || A) . z ) assume z in A ; ::_thesis: ((- 1) (#) ((- f) || A)) . z = (f || A) . z ((- f) || A) . z = (- f) . z by A16, FUNCT_1:47 .= - (f . z) by VALUED_1:8 ; then ((- 1) (#) ((- f) || A)) . z = (- 1) * (- (f . z)) by A20, VALUED_1:def_5 .= f . z ; hence ((- 1) (#) ((- f) || A)) . z = (f || A) . z by A19, FUNCT_1:47; ::_thesis: verum end; A = dom (f || A) by A2, A18, XBOOLE_1:28; then (- 1) (#) ((- f) || A) = f || A by A21, A17, PARTFUN1:5; hence f is_integrable_on A by A15, Def1; ::_thesis: verum end; end; end; theorem :: INTEGRA5:17 for f being PartFunc of REAL,REAL for A, B being non empty closed_interval Subset of REAL st A c= dom f & f | A is continuous & B c= A holds f is_integrable_on B proof let f be PartFunc of REAL,REAL; ::_thesis: for A, B being non empty closed_interval Subset of REAL st A c= dom f & f | A is continuous & B c= A holds f is_integrable_on B let A, B be non empty closed_interval Subset of REAL; ::_thesis: ( A c= dom f & f | A is continuous & B c= A implies f is_integrable_on B ) assume that A1: A c= dom f and A2: f | A is continuous and A3: B c= A ; ::_thesis: f is_integrable_on B f | B is continuous by A2, A3, FCONT_1:16; hence f is_integrable_on B by A1, A3, Th11, XBOOLE_1:1; ::_thesis: verum end; theorem :: INTEGRA5:18 for f being PartFunc of REAL,REAL for A, B, C being non empty closed_interval Subset of REAL for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for A, B, C being non empty closed_interval Subset of REAL for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) let A, B, C be non empty closed_interval Subset of REAL; ::_thesis: for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) let X be set ; ::_thesis: ( A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A implies ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) ) assume that A1: ( A c= X & f is_differentiable_on X ) and A2: (f `| X) | A is continuous and A3: lower_bound A = lower_bound B and A4: upper_bound B = lower_bound C and A5: upper_bound C = upper_bound A ; ::_thesis: ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) consider x being Real such that A6: x in B by SUBSET_1:4; ( lower_bound B <= x & x <= upper_bound B ) by A6, INTEGRA2:1; then A7: lower_bound B <= upper_bound B by XXREAL_0:2; consider x being Real such that A8: x in C by SUBSET_1:4; ( lower_bound C <= x & x <= upper_bound C ) by A8, INTEGRA2:1; then A9: lower_bound C <= upper_bound C by XXREAL_0:2; for x being set st x in B holds x in A proof let x be set ; ::_thesis: ( x in B implies x in A ) assume A10: x in B ; ::_thesis: x in A then reconsider x = x as Real ; x <= upper_bound B by A10, INTEGRA2:1; then A11: x <= upper_bound A by A4, A5, A9, XXREAL_0:2; lower_bound A <= x by A3, A10, INTEGRA2:1; hence x in A by A11, INTEGRA2:1; ::_thesis: verum end; hence A12: B c= A by TARSKI:def_3; ::_thesis: ( C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) A13: A c= dom (f `| X) by A1, FDIFF_1:def_7; then A14: (f `| X) | A is bounded by A2, Th10; then A15: (f `| X) | B is bounded by A12, RFUNCT_1:74; for x being set st x in C holds x in A proof let x be set ; ::_thesis: ( x in C implies x in A ) assume A16: x in C ; ::_thesis: x in A then reconsider x = x as Real ; lower_bound C <= x by A16, INTEGRA2:1; then A17: lower_bound A <= x by A3, A4, A7, XXREAL_0:2; x <= upper_bound A by A5, A16, INTEGRA2:1; hence x in A by A17, INTEGRA2:1; ::_thesis: verum end; hence A18: C c= A by TARSKI:def_3; ::_thesis: integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) then A19: (f `| X) | C is bounded by A14, RFUNCT_1:74; (f `| X) | C is continuous by A2, A18, FCONT_1:16; then f `| X is_integrable_on C by A13, A18, Th11, XBOOLE_1:1; then A20: integral ((f `| X),C) = (f . (upper_bound C)) - (f . (lower_bound C)) by A1, A18, A19, Th13, XBOOLE_1:1; (f `| X) | B is continuous by A2, A12, FCONT_1:16; then f `| X is_integrable_on B by A13, A12, Th11, XBOOLE_1:1; then A21: integral ((f `| X),B) = (f . (upper_bound B)) - (f . (lower_bound B)) by A1, A12, A15, Th13, XBOOLE_1:1; f `| X is_integrable_on A by A2, A13, Th11; then integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) by A1, A2, A13, Th10, Th13; hence integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) by A3, A4, A5, A21, A20; ::_thesis: verum end; definition let a, b be real number ; assume A1: a <= b ; func['a,b'] -> non empty closed_interval Subset of REAL equals :Def3: :: INTEGRA5:def 3 [.a,b.]; correctness coherence [.a,b.] is non empty closed_interval Subset of REAL; proof ( a is Real & b is Real ) by XREAL_0:def_1; hence [.a,b.] is non empty closed_interval Subset of REAL by A1, MEASURE5:14; ::_thesis: verum end; end; :: deftheorem Def3 defines [' INTEGRA5:def_3_:_ for a, b being real number st a <= b holds ['a,b'] = [.a,b.]; definition let a, b be real number ; let f be PartFunc of REAL,REAL; func integral (f,a,b) -> Real equals :Def4: :: INTEGRA5:def 4 integral (f,['a,b']) if a <= b otherwise - (integral (f,['b,a'])); correctness coherence ( ( a <= b implies integral (f,['a,b']) is Real ) & ( not a <= b implies - (integral (f,['b,a'])) is Real ) ); consistency for b1 being Real holds verum; ; end; :: deftheorem Def4 defines integral INTEGRA5:def_4_:_ for a, b being real number for f being PartFunc of REAL,REAL holds ( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) ); theorem :: INTEGRA5:19 for f being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) proof let f be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) let a, b be Real; ::_thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) ) consider a1, b1 being Real such that A1: a1 <= b1 and A2: A = [.a1,b1.] by MEASURE5:14; assume A = [.a,b.] ; ::_thesis: integral (f,A) = integral (f,a,b) then A3: ( a1 = a & b1 = b ) by A2, INTEGRA1:5; then integral (f,a,b) = integral (f,['a,b']) by A1, Def4; hence integral (f,A) = integral (f,a,b) by A1, A2, A3, Def3; ::_thesis: verum end; theorem :: INTEGRA5:20 for f being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) proof let f be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) let a, b be Real; ::_thesis: ( A = [.b,a.] implies - (integral (f,A)) = integral (f,a,b) ) consider a1, b1 being Real such that A1: a1 <= b1 and A2: A = [.a1,b1.] by MEASURE5:14; assume A3: A = [.b,a.] ; ::_thesis: - (integral (f,A)) = integral (f,a,b) then A4: ( a1 = b & b1 = a ) by A2, INTEGRA1:5; now__::_thesis:_-_(integral_(f,A))_=_integral_(f,a,b) percases ( b < a or b = a ) by A1, A4, XXREAL_0:1; supposeA5: b < a ; ::_thesis: - (integral (f,A)) = integral (f,a,b) then integral (f,a,b) = - (integral (f,['b,a'])) by Def4; hence - (integral (f,A)) = integral (f,a,b) by A3, A5, Def3; ::_thesis: verum end; supposeA6: b = a ; ::_thesis: - (integral (f,A)) = integral (f,a,b) A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then ( lower_bound A = b & upper_bound A = a ) by A3, INTEGRA1:5; then vol A = (upper_bound A) - (upper_bound A) by A6, INTEGRA1:def_5 .= 0 ; then A7: integral (f,A) = 0 by INTEGRA4:6; integral (f,a,b) = integral (f,['a,b']) by A6, Def4; hence - (integral (f,A)) = integral (f,a,b) by A3, A6, A7, Def3; ::_thesis: verum end; end; end; hence - (integral (f,A)) = integral (f,a,b) ; ::_thesis: verum end; theorem :: INTEGRA5:21 for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) let f, g be PartFunc of REAL,REAL; ::_thesis: for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) let X be open Subset of REAL; ::_thesis: ( f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded implies integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) ) assume that A1: f is_differentiable_on X and A2: g is_differentiable_on X and A3: A c= X and A4: f `| X is_integrable_on A and A5: (f `| X) | A is bounded and A6: g `| X is_integrable_on A and A7: (g `| X) | A is bounded ; ::_thesis: integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) A8: (f (#) g) `| X = ((f `| X) (#) g) + (f (#) (g `| X)) by A1, A2, FDIFF_2:20; g | X is continuous by A2, FDIFF_1:25; then A9: g | A is continuous by A3, FCONT_1:16; X c= dom g by A2, FDIFF_1:def_6; then A10: A c= dom g by A3, XBOOLE_1:1; then A11: g || A is Function of A,REAL by Th6, FUNCT_2:68; X c= dom g by A2, FDIFF_1:def_6; then g is_integrable_on A by A3, A9, Th11, XBOOLE_1:1; then A12: g || A is integrable by Def1; A13: A c= dom (g `| X) by A2, A3, FDIFF_1:def_7; then A14: (g `| X) || A is Function of A,REAL by Th6, FUNCT_2:68; g | X is continuous by A2, FDIFF_1:25; then g | A is bounded by A3, A10, Th10, FCONT_1:16; then A15: ((f `| X) (#) g) | (A /\ A) is bounded by A5, RFUNCT_1:84; then A16: (((f `| X) (#) g) || A) | A is bounded ; f | X is continuous by A1, FDIFF_1:25; then A17: f | A is continuous by A3, FCONT_1:16; X c= dom f by A1, FDIFF_1:def_6; then f is_integrable_on A by A3, A17, Th11, XBOOLE_1:1; then A18: f || A is integrable by Def1; A19: A c= dom (f `| X) by A1, A3, FDIFF_1:def_7; then A20: (f `| X) || A is Function of A,REAL by Th6, FUNCT_2:68; A21: ( (g `| X) || A is integrable & ((g `| X) || A) | A is bounded ) by A6, A7, Def1; A22: ( (f `| X) || A is integrable & ((f `| X) || A) | A is bounded ) by A4, A5, Def1; dom ((f `| X) (#) g) = (dom (f `| X)) /\ (dom g) by VALUED_1:def_4; then A c= dom ((f `| X) (#) g) by A10, A19, XBOOLE_1:19; then A23: ((f `| X) (#) g) || A is Function of A,REAL by Th6, FUNCT_2:68; X c= dom f by A1, FDIFF_1:def_6; then A24: A c= dom f by A3, XBOOLE_1:1; then A25: f || A is Function of A,REAL by Th6, FUNCT_2:68; f | X is continuous by A1, FDIFF_1:25; then f | A is bounded by A3, A24, Th10, FCONT_1:16; then A26: (f (#) (g `| X)) | (A /\ A) is bounded by A7, RFUNCT_1:84; then A27: ((f (#) (g `| X)) || A) | A is bounded ; (((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A) is bounded by A15, A26, RFUNCT_1:83; then A28: ((f (#) g) `| X) | A is bounded by A1, A2, FDIFF_2:20; A29: ( (f (#) g) . (upper_bound A) = (f . (upper_bound A)) * (g . (upper_bound A)) & (f (#) g) . (lower_bound A) = (f . (lower_bound A)) * (g . (lower_bound A)) ) by VALUED_1:5; dom (f (#) (g `| X)) = (dom f) /\ (dom (g `| X)) by VALUED_1:def_4; then A c= dom (f (#) (g `| X)) by A24, A13, XBOOLE_1:19; then A30: (f (#) (g `| X)) || A is Function of A,REAL by Th6, FUNCT_2:68; (g || A) | A is bounded by A9, A10, Th10; then ((f `| X) || A) (#) (g || A) is integrable by A12, A11, A20, A22, INTEGRA4:29; then A31: ((f `| X) (#) g) || A is integrable by Th4; (f || A) | A is bounded by A17, A24, Th10; then (f || A) (#) ((g `| X) || A) is integrable by A18, A25, A14, A21, INTEGRA4:29; then A32: (f (#) (g `| X)) || A is integrable by Th4; then integral ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A)) = (integral (((f `| X) (#) g) || A)) + (integral ((f (#) (g `| X)) || A)) by A31, A23, A16, A30, A27, INTEGRA1:57; then A33: integral ((((f `| X) (#) g) + (f (#) (g `| X))) || A) = (integral (((f `| X) (#) g),A)) + (integral ((f (#) (g `| X)),A)) by Th5; (((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A) is integrable by A31, A32, A23, A16, A30, A27, INTEGRA1:57; then (((f `| X) (#) g) + (f (#) (g `| X))) || A is integrable by Th5; then A34: (f (#) g) `| X is_integrable_on A by A8, Def1; integral (((f (#) g) `| X) || A) = integral (((f (#) g) `| X),A) .= ((f (#) g) . (upper_bound A)) - ((f (#) g) . (lower_bound A)) by A1, A2, A3, A34, A28, Th13, FDIFF_2:20 ; hence integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) by A8, A29, A33; ::_thesis: verum end;