:: The Definition of Riemann Definite Integral and some Related Lemmas :: by Noboru Endou and Artur Korni{\l}owicz :: :: Received March 13, 1999 :: Copyright (c) 1999-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, RCOMP_1, ORDINAL2, ARYTM_1, RELAT_1, FUNCT_1, PARTFUN1, CARD_3, XBOOLE_0, FUNCT_3, ZFMISC_1, XXREAL_0, REAL_1, SUBSET_1, FINSEQ_2, RFINSEQ, JORDAN3, SEQ_4, CARD_1, INTEGRA1, FUNCOP_1, VALUED_0, NUMBERS, MEASURE7, ORDINAL4, XXREAL_1, XXREAL_2, NAT_1, ARYTM_3, TARSKI, MEMBER_1, MEASURE5, FUNCT_7, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, RELSET_1, VALUED_0, MEMBERED, MEMBER_1, VALUED_1, SEQ_4, XXREAL_2, COMSEQ_2, SEQ_2, RCOMP_1, FINSEQ_2, PARTFUN2, RFUNCT_1, RVSUM_1, RFINSEQ, FINSEQ_6, PARTFUN1, FINSEQ_1, FUNCT_2, MEASURE5, MEASURE6; constructors PARTFUN1, REAL_1, NAT_1, RCOMP_1, FINSOP_1, PARTFUN2, RFUNCT_1, REALSET1, RFINSEQ, BINARITH, FINSEQ_5, SEQM_3, MEASURE6, FINSEQ_6, BINOP_2, XXREAL_2, NAT_D, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, MEMBER_1, XXREAL_3, MEASURE5, COMSEQ_2, NUMBERS; registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, SEQM_3, VALUED_0, VALUED_1, FINSET_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, MEMBER_1, MEASURE5; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, XBOOLE_0, XXREAL_2, FUNCT_2; equalities XBOOLE_0, RVSUM_1; expansions TARSKI, XBOOLE_0, XXREAL_2; theorems TARSKI, RCOMP_1, FINSEQ_1, FINSEQ_2, SEQ_4, FUNCT_1, NAT_1, NAT_2, SUBSET_1, PARTFUN1, RFUNCT_1, MEASURE6, RVSUM_1, PARTFUN2, ZFMISC_1, FUNCT_3, FINSEQ_4, RFINSEQ, RELAT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, FUNCOP_1, XREAL_1, XXREAL_0, FINSOP_1, ORDINAL1, XXREAL_1, VALUED_1, FINSEQ_3, XXREAL_2, SEQM_3, NAT_D, FINSEQ_6, MEMBER_1, MEMBERED, CARD_1, MEASURE5, XREAL_0; schemes FINSEQ_2, NAT_1, FUNCT_2, XFAMILY; begin :: Definition of closed interval and its properties reserve a,a1,b,b1,x,y for Real, F,G,H for FinSequence of REAL, i,j,k,n,m for Element of NAT, I for Subset of REAL, X for non empty set, x1,R,s for set; reserve A for non empty closed_interval Subset of REAL; registration cluster closed_interval -> compact for Subset of REAL; coherence proof let IT be Subset of REAL; assume IT is closed_interval; then ex a,b being Real st IT = [.a,b.] by MEASURE5:def 3; hence thesis by RCOMP_1:6; end; end; ::$CT 2 theorem Th1: A is bounded_below bounded_above proof A is real-bounded by RCOMP_1:10; hence thesis; end; registration cluster non empty closed_interval -> real-bounded for Subset of REAL; coherence by Th1; end; reserve A, B for non empty closed_interval Subset of REAL; theorem Th2: A = [. lower_bound A, upper_bound A .] proof consider a,b being Real such that A1: a <= b and A2: A=[.a,b.] by MEASURE5:14; A3: for y be Real st 0 non empty increasing FinSequence of REAL means :Def1: rng it c= A & it.(len it) = upper_bound A; existence proof reconsider a = upper_bound A as Element of REAL by XREAL_0:def 1; reconsider p = Seg 1 --> a as Function of Seg 1, REAL by FUNCOP_1:45; A1: dom p = Seg 1 by FUNCOP_1:13; rng p c= REAL; then reconsider p as FinSequence of REAL by FINSEQ_1:def 4; A2: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1; for n,m being Nat st n in dom p & m in dom p & n set means :Def2: x1 in it iff x1 is Division of A; existence proof defpred P[set] means $1 is Division of A; consider R such that A1: x1 in R iff x1 in bool [:NAT,REAL:] & P[x1] from XFAMILY:sch 1; take R; let x1; thus x1 in R implies x1 is Division of A by A1; assume x1 is Division of A; then reconsider p = x1 as Division of A; p c= [:NAT,REAL:]; hence thesis by A1; end; uniqueness proof let D1,D2 be set such that A2: x1 in D1 iff x1 is Division of A and A3: x1 in D2 iff x1 is Division of A; now let x1 be object; thus x1 in D1 implies x1 in D2 proof assume x1 in D1; then x1 is Division of A by A2; hence thesis by A3; end; assume x1 in D2; then x1 is Division of A by A3; hence x1 in D1 by A2; end; hence thesis by TARSKI:2; end; end; registration let A be non empty compact Subset of REAL; cluster divs A -> non empty; coherence proof the Division of A in divs A by Def2; hence thesis; end; end; registration let A be non empty compact Subset of REAL; cluster -> Function-like Relation-like for Element of divs A; coherence by Def2; end; registration let A be non empty compact Subset of REAL; cluster -> real-valued FinSequence-like for Element of divs A; coherence by Def2; end; reserve r for Real; reserve D, D1, D2 for Division of A; reserve f, g for Function of A,REAL; theorem Th4: i in dom D implies D.i in A proof assume i in dom D; then A1: D.i in rng D by FUNCT_1:def 3; rng D c= A by Def1; hence thesis by A1; end; theorem Th5: i in dom D & i<>1 implies i-1 in dom D & D.(i-1) in A & i-1 in NAT proof assume that A1: i in dom D and A2: i<>1; consider j be Nat such that A3: dom D = Seg j by FINSEQ_1:def 2; i<>0 by A1,A3,FINSEQ_1:1; then A4: i is non trivial by A2,NAT_2:def 1; then consider l being Nat such that A5: i=2+l by NAT_1:10,NAT_2:29; reconsider l as Element of NAT by ORDINAL1:def 12; i >= 2 by A4,NAT_2:29; then A6: 1+1-1 <= i-1 by XREAL_1:9; i<=j by A1,A3,FINSEQ_1:1; then A7: i-1<=j-0 by XREAL_1:13; A8: rng D c= A by Def1; A9: l+1=i-(2-1) by A5; then i-1 in dom D by A3,A6,A7,FINSEQ_1:1; then D.(i-1) in rng D by FUNCT_1:def 3; hence thesis by A3,A6,A7,A9,A8,FINSEQ_1:1; end; definition let A be non empty closed_interval Subset of REAL; let D be Division of A; let i be Nat; assume A1: i in dom D; func divset(D,i) -> non empty closed_interval Subset of REAL means :Def3: lower_bound it = lower_bound A & upper_bound it = D.i if i=1 otherwise lower_bound it = D.(i-1) & upper_bound it = D.i; existence proof hereby assume i=1; thus ex IT being non empty closed_interval Subset of REAL st lower_bound IT = lower_bound A & upper_bound IT = D.i proof consider I such that A2: I=[.lower_bound A,D.i .]; D.i in A by A1,Th4; then lower_bound A <= D.i by SEQ_4:def 2; then A3: I is non empty closed_interval Subset of REAL by A2,MEASURE5:14; then A4: I = [.lower_bound I,upper_bound I.] by Th2; then A5: upper_bound I = D.i by A2,A3,Th3; lower_bound I = lower_bound A by A2,A3,A4,Th3; hence thesis by A3,A5; end; end; assume that A6: i<>1; thus ex IT being non empty closed_interval Subset of REAL st lower_bound IT = D.(i-1 ) & upper_bound IT = D.i proof reconsider j=i-1 as Element of NAT by A1,A6,Th5; A7: i+-1< i+(1+-1) by XREAL_1:6; consider a1,b1 such that A8: a1=D.(i-1) and A9: b1=D.i; consider I such that A10: I=[.a1,b1.]; i-1 in dom D by A1,A6,Th5; then D.j < D.i by A1,A7,SEQM_3:def 1; then A11: I is non empty closed_interval Subset of REAL by A8,A9,A10,MEASURE5:14; then A12: I=[.lower_bound I,upper_bound I.] by Th2; then A13: upper_bound I=D.i by A9,A10,A11,Th3; lower_bound I=D.(i-1) by A8,A10,A11,A12,Th3; hence thesis by A11,A13; end; end; uniqueness proof let A1,A2 be non empty closed_interval Subset of REAL; hereby consider b such that A14: b=D.i; assume that i=1 and A15: lower_bound A1 =lower_bound A and A16: upper_bound A1 = D.i and A17: lower_bound A2 =lower_bound A and A18: upper_bound A2 = D.i; A1=[. lower_bound A, b .] by A15,A16,A14,Th2; hence A1=A2 by A17,A18,A14,Th2; end; assume that i<>1 and A19: lower_bound A1 = D.(i-1) and A20: upper_bound A1 = D.i and A21: lower_bound A2 = D.(i-1) and A22: upper_bound A2 = D.i; consider a,b such that A23: a=D.(i-1) and A24: b=D.i; A1=[.a,b.] by A19,A20,A23,A24,Th2; hence thesis by A21,A22,A23,A24,Th2; end; correctness; end; theorem Th6: i in dom D implies divset(D,i) c= A proof assume A1: i in dom D; now per cases; suppose A2: i=1; lower_bound A in A by RCOMP_1:14; then A3: lower_bound A in [.lower_bound A,upper_bound A.] by Th2; A4: lower_bound divset(D,i) = lower_bound A by A1,A2,Def3; consider b such that A5: b=D.i; upper_bound divset(D,i) = b by A1,A2,A5,Def3; then A6: divset(D,i)=[. lower_bound A,b .] by A4,Th2; b in A by A1,A5,Th4; then b in [.lower_bound A,upper_bound A.] by Th2; then [. lower_bound A,b .] c= [.lower_bound A,upper_bound A.] by A3,XXREAL_2:def 12; hence thesis by A6,Th2; end; suppose A7: i<>1; set b=D.i; b in A by A1,Th4; then A8: b in [.lower_bound A,upper_bound A.] by Th2; set a=D.(i-1); D.(i-1) in A by A1,A7,Th5; then a in [.lower_bound A,upper_bound A.] by Th2; then A9: [.a,b.] c= [.lower_bound A,upper_bound A.] by A8,XXREAL_2:def 12; A10: upper_bound divset(D,i) = b by A1,A7,Def3; lower_bound divset(D,i) = a by A1,A7,Def3; then divset(D,i)=[.a,b.] by A10,Th2; hence thesis by A9,Th2; end; end; hence thesis; end; definition let A be Subset of REAL; func vol(A) -> Real equals upper_bound A - lower_bound A; correctness; end; theorem for A be real-bounded non empty Subset of REAL holds 0 <= vol(A) by SEQ_4:11,XREAL_1:48; begin :: Definitions of integrability and related topics definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; let D be Division of A; func upper_volume(f,D) -> FinSequence of REAL means :Def5: len it = len D & for i be Nat st i in dom D holds it.i=(upper_bound rng (f|divset(D,i)))*vol divset(D,i); existence proof deffunc F(Nat)= In(upper_bound (rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL); consider IT being FinSequence of REAL such that A1: len IT = len D & for i be Nat st i in dom IT holds IT.i=F(i) from FINSEQ_2:sch 1; take IT; thus len IT = len D by A1; let i be Nat; A2: F(i)= upper_bound (rng (f|divset(D,i)))*vol(divset(D,i)); assume i in dom D; then i in dom IT by A1,FINSEQ_3:29; hence thesis by A1,A2; end; uniqueness proof let s1,s2 be FinSequence of REAL such that A3: len s1 = len D and A4: for i be Nat st i in dom D holds s1.i=(upper_bound (rng (f|divset( D, i))))*vol(divset(D,i)) and A5: len s2 = len D and A6: for i be Nat st i in dom D holds s2.i=(upper_bound (rng (f|divset( D, i))))*vol(divset(D,i)); A7: dom s1 = dom D by A3,FINSEQ_3:29; for i being Nat st i in dom s1 holds s1.i=s2.i proof let i be Nat; assume A8: i in dom s1; then s1.i=(upper_bound (rng (f|divset(D,i))))*vol(divset(D,i)) by A4,A7; hence thesis by A6,A7,A8; end; hence thesis by A3,A5,FINSEQ_2:9; end; func lower_volume(f,D) -> FinSequence of REAL means :Def6: len it = len D & for i be Nat st i in dom D holds it.i=(lower_bound rng (f|divset(D,i)))*vol divset(D,i); existence proof deffunc F(Nat)= In((lower_bound (rng (f|divset(D,$1))))*vol(divset(D,$1)),REAL); consider IT being FinSequence of REAL such that A9: len IT = len D & for i be Nat st i in dom IT holds IT.i=F(i) from FINSEQ_2:sch 1; take IT; thus len IT = len D by A9; let i be Nat; A10: In((lower_bound (rng (f|divset(D,i))))*vol(divset(D,i)),REAL) = (lower_bound (rng (f|divset(D,i))))*vol(divset(D,i)); assume i in dom D; then i in dom IT by A9,FINSEQ_3:29; hence thesis by A9,A10; end; uniqueness proof let s1,s2 be FinSequence of REAL such that A11: len s1 = len D and A12: for i be Nat st i in dom D holds s1.i=(lower_bound (rng (f|divset (D,i))))*vol(divset(D,i)) and A13: len s2 = len D and A14: for i be Nat st i in dom D holds s2.i=(lower_bound (rng (f|divset (D,i))))*vol(divset(D,i)); A15: dom s1 = dom D by A11,FINSEQ_3:29; for i being Nat st i in dom s1 holds s1.i=s2.i proof let i be Nat; assume A16: i in dom s1; then s1.i=(lower_bound (rng (f|divset(D,i))))*vol(divset(D,i)) by A12,A15 ; hence thesis by A14,A15,A16; end; hence thesis by A11,A13,FINSEQ_2:9; end; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; let D be Division of A; func upper_sum(f,D) -> Real equals Sum(upper_volume(f,D)); correctness; func lower_sum(f,D) -> Real equals Sum(lower_volume(f,D)); correctness; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; set S = divs A; func upper_sum_set(f) -> Function of divs A,REAL means :Def9: for D be Division of A holds it.D=upper_sum(f,D); existence proof defpred P[Element of S,set] means ex D being Division of A st D = $1 & $2 = upper_sum(f,D); A1: for x being Element of S ex y being Element of REAL st P[x,y] proof let x be Element of S; reconsider x as Division of A by Def2; take upper_sum(f,x); thus thesis; end; consider g being Function of S,REAL such that A2: for x being Element of S holds P[x,g.x] from FUNCT_2:sch 3(A1); take g; let D be Division of A; reconsider D1 = D as Element of S by Def2; P[D1,g.D1] by A2; hence thesis; end; uniqueness proof let g1,g2 be Function of S,REAL such that A3: for D be Division of A holds g1.D = upper_sum(f,D) and A4: for D be Division of A holds g2.D = upper_sum(f,D); let a be Element of S; reconsider d = a as Division of A by Def2; thus g1.a = upper_sum(f,d) by A3 .= g2.a by A4; end; func lower_sum_set(f) -> Function of divs A,REAL means :Def10: for D be Division of A holds it.D=lower_sum(f,D); existence proof defpred P[Element of S,set] means ex D being Division of A st D = $1 & $2 = lower_sum(f,D); A5: for x being Element of S ex y being Element of REAL st P[x,y] proof let x be Element of S; reconsider x as Division of A by Def2; take lower_sum(f,x); thus thesis; end; consider g being Function of S,REAL such that A6: for x being Element of S holds P[x,g.x] from FUNCT_2:sch 3(A5); take g; let D be Division of A; reconsider D1 = D as Element of S by Def2; P[D1,g.D1] by A6; hence thesis; end; uniqueness proof let g1,g2 be Function of S,REAL such that A7: for D be Division of A holds g1.D = lower_sum(f,D) and A8: for D be Division of A holds g2.D = lower_sum(f,D); let a be Element of S; reconsider d = a as Division of A by Def2; thus g1.a = lower_sum(f,d) by A7 .= g2.a by A8; end; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; attr f is upper_integrable means rng upper_sum_set(f) is bounded_below; attr f is lower_integrable means rng lower_sum_set(f) is bounded_above; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; func upper_integral(f) -> Real equals lower_bound rng upper_sum_set(f); correctness; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; func lower_integral(f) -> Real equals upper_bound rng lower_sum_set(f); coherence; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; attr f is integrable means f is upper_integrable lower_integrable & upper_integral(f) = lower_integral(f); end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; func integral(f) -> Real equals upper_integral(f); coherence; end; begin :: Real function's properties theorem Th8: for f,g be PartFunc of X,REAL holds rng(f+g) c= rng f ++ rng g proof let f,g be PartFunc of X,REAL; let y be object; assume y in rng(f+g); then consider x1 being object such that A1: x1 in dom(f+g) and A2: y=(f+g).x1 by FUNCT_1:def 3; A3: dom(f+g)=dom f /\ dom g by VALUED_1:def 1; then x1 in dom f by A1,XBOOLE_0:def 4; then A4: f.x1 in rng f by FUNCT_1:def 3; x1 in dom g by A1,A3,XBOOLE_0:def 4; then A5: g.x1 in rng g by FUNCT_1:def 3; (f+g).x1=f.x1+g.x1 by A1,VALUED_1:def 1; hence thesis by A2,A4,A5,MEMBER_1:46; end; theorem Th9: for f be real-valued Function holds f is bounded_below implies rng f is bounded_below proof let f be real-valued Function; set X = dom f; AA: f|X = f; assume f is bounded_below; then consider a be Real such that A1: for x1 being object st x1 in X /\ dom f holds a <= f.x1 by AA,RFUNCT_1:71; a is LowerBound of rng f proof let y be ExtReal; assume y in rng f; then ex s being object st s in dom f & y = f.s by FUNCT_1:def 3; hence thesis by A1; end; hence thesis; end; theorem for f be real-valued Function st rng f is bounded_below holds f is bounded_below proof let f be real-valued Function; set X = dom f; assume rng f is bounded_below; then consider a be Real such that A1: a is LowerBound of rng f; AA: f|X = f; for x1 being object st x1 in X /\ dom f holds a <= f.x1 proof let x1 be object; assume x1 in X /\ dom f; then f.x1 in rng f by FUNCT_1:def 3; hence thesis by A1,XXREAL_2:def 2; end; hence thesis by AA,RFUNCT_1:71; end; theorem Th11: for f be real-valued Function st f is bounded_above holds rng f is bounded_above proof let f be real-valued Function; set X = dom f; AA: f|X = f; assume f is bounded_above; then consider a be Real such that A1: for x1 being object st x1 in X /\ dom f holds f.x1 <= a by AA,RFUNCT_1:70; a is UpperBound of rng f proof let y be ExtReal; assume y in rng f; then ex s being object st s in dom f & y = f.s by FUNCT_1:def 3; hence thesis by A1; end; hence thesis; end; theorem for f be real-valued Function st rng f is bounded_above holds f is bounded_above proof let f be real-valued Function; set X = dom f; assume rng f is bounded_above; then consider a be Real such that A1: a is UpperBound of rng f; AA: f|X = f; for x1 being object st x1 in X /\ dom f holds f.x1 <= a proof let x1 be object; assume x1 in X /\ dom f; then f.x1 in rng f by FUNCT_1:def 3; hence thesis by A1,XXREAL_2:def 1; end; hence thesis by AA,RFUNCT_1:70; end; theorem for f be real-valued Function holds f is bounded implies rng f is real-bounded by Th11,Th9; begin :: Characteristic function's properties theorem Th14: for A be non empty set holds chi(A,A)|A is constant proof let A be non empty set; reconsider jj=1 as Element of REAL by XREAL_0:def 1; for x being Element of A st x in A /\ dom chi(A,A) holds chi(A,A)/.x=jj proof let x be Element of A; assume x in A /\ dom chi(A,A); then A1: x in dom chi(A,A) by XBOOLE_0:def 4; chi(A,A).x=1 by FUNCT_3:def 3; hence thesis by A1,PARTFUN1:def 6; end; hence thesis by PARTFUN2:35; end; theorem Th15: for A be non empty Subset of X holds rng chi(A,A) = {1} proof let A be non empty Subset of X; A1: chi(A,A)|A is constant by Th14; dom chi(A,A) = A by FUNCT_3:def 3; then A2: A = A /\ dom chi(A,A); A3: dom chi(A,A) = A by FUNCT_3:def 3; ex x being Element of X st x in dom chi(A,A) & chi(A,A).x=1 proof consider x being Element of X such that A4: x in dom chi(A,A) by A3,SUBSET_1:4; take x; thus thesis by A4,FUNCT_3:def 3; end; then A5: 1 in rng chi(A,A) by FUNCT_1:def 3; A meets dom chi(A,A) by A2; then ex y being Element of REAL st rng (chi(A,A)|A)={y} by A1,PARTFUN2:37; hence thesis by A5,TARSKI:def 1; end; theorem Th16: for A be non empty Subset of X, B be set holds B meets dom chi(A ,A) implies rng (chi(A,A)|B) = {1} proof let A be non empty Subset of X; let B be set; A1: dom (chi(A,A)|B) = B /\ dom (chi(A,A)) by RELAT_1:61; rng (chi(A,A)|B) c= rng (chi(A,A)) by RELAT_1:70; then A2: rng (chi(A,A)|B) c= {1} by Th15; assume B /\ dom (chi(A,A)) <> {}; then rng (chi(A,A)|B) <> {} by A1,RELAT_1:42; hence thesis by A2,ZFMISC_1:33; end; theorem Th17: i in dom D implies vol(divset(D,i))=lower_volume(chi(A,A),D).i proof A1: dom (chi(A,A)) = A by FUNCT_3:def 3; assume A2: i in dom D; then A3: lower_volume(chi(A,A),D).i= (lower_bound (rng (chi(A,A)|divset(D,i))))* vol(divset(D,i)) by Def6; divset(D,i) c= A by A2,Th6; then divset(D,i) c= divset(D,i) /\ dom (chi(A,A)) by A1,XBOOLE_1:19; then divset(D,i) /\ dom (chi(A,A)) <> {}; then divset(D,i) meets dom (chi(A,A)); then A4: rng (chi(A,A)|divset(D,i)) = {1} by Th16; A5: rng chi(A,A) = {1} by Th15; then lower_bound rng (chi(A,A)) = 1 by SEQ_4:9; hence thesis by A3,A5,A4; end; theorem Th18: i in dom D implies vol(divset(D,i))=upper_volume(chi(A,A),D).i proof A1: dom (chi(A,A)) = A by FUNCT_3:def 3; assume A2: i in dom D; then A3: upper_volume(chi(A,A),D).i= (upper_bound (rng (chi(A,A)|divset(D,i))))* vol(divset(D,i)) by Def5; divset(D,i) c= A by A2,Th6; then divset(D,i) c= divset(D,i) /\ dom (chi(A,A)) by A1,XBOOLE_1:19; then divset(D,i) /\ dom (chi(A,A)) <> {}; then divset(D,i) meets dom (chi(A,A)); then A4: rng (chi(A,A)|divset(D,i)) = {1} by Th16; A5: rng chi(A,A) = {1} by Th15; then upper_bound rng (chi(A,A)) = 1 by SEQ_4:9; hence thesis by A3,A5,A4; end; theorem len F = len G & len F = len H & (for k st k in dom F holds H.k = F/.k + G/.k) implies Sum(H) = Sum(F) + Sum(G) proof assume that A1: len F = len G and A2: len F = len H and A3: for k st k in dom F holds H.k = F/.k + G/.k; A4: F is Element of (len F)-tuples_on REAL by FINSEQ_2:92; A5: G is Element of (len F)-tuples_on REAL by A1,FINSEQ_2:92; then F+G is Element of (len F)-tuples_on REAL by A4,FINSEQ_2:120; then A6: len H = len (F+G) by A2,CARD_1:def 7; then A7: dom H = Seg len(F+G) by FINSEQ_1:def 3; A8: for k st k in dom F holds H.k = F.k + G.k proof let k; assume A9: k in dom F; then k in Seg(len G) by A1,FINSEQ_1:def 3; then k in dom G by FINSEQ_1:def 3; then A10: G/.k = G.k by PARTFUN1:def 6; F/.k = F.k by A9,PARTFUN1:def 6; hence thesis by A3,A9,A10; end; for k being Nat st k in dom H holds H.k = (F+G).k proof let k be Nat; assume A11: k in dom H; then k in dom F by A2,A6,A7,FINSEQ_1:def 3; then A12: H.k=F.k+G.k by A8; k in dom(F+G) by A7,A11,FINSEQ_1:def 3; hence thesis by A12,VALUED_1:def 1; end; then Sum H=Sum(F+G) by A6,FINSEQ_2:9 .=Sum F+Sum G by A4,A5,RVSUM_1:89; hence thesis; end; theorem Th20: len F = len G & len F = len H & (for k st k in dom F holds H.k = F/.k - G/.k) implies Sum(H) = Sum(F) - Sum(G) proof assume that A1: len F = len G and A2: len F = len H and A3: for k st k in dom F holds H.k = F/.k - G/.k; A4: F is Element of (len F)-tuples_on REAL by FINSEQ_2:92; A5: G is Element of (len F)-tuples_on REAL by A1,FINSEQ_2:92; then A6: F-G is Element of (len F)-tuples_on REAL by A4,FINSEQ_2:120; then A7: len H = len (F-G) by A2,CARD_1:def 7; then A8: dom H = Seg len (F-G) by FINSEQ_1:def 3; A9: for k st k in dom F holds H.k = F.k - G.k proof let k; assume A10: k in dom F; then k in Seg(len G) by A1,FINSEQ_1:def 3; then k in dom G by FINSEQ_1:def 3; then A11: G/.k = G.k by PARTFUN1:def 6; F/.k = F.k by A10,PARTFUN1:def 6; hence thesis by A3,A10,A11; end; for k being Nat st k in dom H holds H.k = (F-G).k proof let k be Nat; assume A12: k in dom H; then k in Seg(len F) by A6,A8,CARD_1:def 7; then k in dom F by FINSEQ_1:def 3; then A13: H.k=F.k-G.k by A9; k in dom(F-G) by A8,A12,FINSEQ_1:def 3; hence thesis by A13,VALUED_1:13; end; then Sum H=Sum(F-G) by A7,FINSEQ_2:9 .=Sum F-Sum G by A4,A5,RVSUM_1:90; hence thesis; end; theorem Th21: Sum(lower_volume(chi(A,A),D))=vol(A) proof deffunc F(Nat)=In(vol(divset(D,$1)),REAL); consider p being FinSequence of REAL such that A1: len p = len D & for i be Nat st i in dom p holds p.i = F(i) from FINSEQ_2:sch 1; A2: dom p = Seg len D by A1,FINSEQ_1:def 3; A3: for i st i in Seg(len D) holds p.i = upper_bound divset(D,i) - lower_bound divset(D,i) proof let i; A4: In(vol(divset(D,i)),REAL) = vol(divset(D,i)); assume i in Seg(len D); hence thesis by A1,A2,A4; end; len D - 1 in NAT proof ex j being Nat st len D = 1 + j by NAT_1:10,14; hence thesis by ORDINAL1:def 12; end; then reconsider k = len D - 1 as Element of NAT; deffunc G(Nat)=In(lower_bound divset(D,$1+1),REAL); deffunc F(Nat)=In(upper_bound divset(D,$1),REAL); consider s1 being FinSequence of REAL such that A5: len s1 = k & for i be Nat st i in dom s1 holds s1.i = F(i) from FINSEQ_2:sch 1; consider s2 being FinSequence of REAL such that A6: len s2 = k & for i be Nat st i in dom s2 holds s2.i = G(i) from FINSEQ_2:sch 1; A7: dom s2 = Seg k by A6,FINSEQ_1:def 3; reconsider ub=upper_bound A, lb=lower_bound A as Element of REAL by XREAL_0:def 1; len (s1^<*upper_bound A*>) = len (<*lower_bound A*>^s2) & len (s1^<* upper_bound A*>) = len p & for i st i in dom (s1^<*upper_bound A*>) holds p.i=( s1^<*ub*>)/.i - (<*lb*>^s2)/.i proof dom(<*upper_bound A*>)=Seg 1 by FINSEQ_1:def 8; then len(<*upper_bound A*>)=1 by FINSEQ_1:def 3; then A8: len(s1^<*upper_bound A*>)=k+1 by A5,FINSEQ_1:22; dom(<*lower_bound A*>)=Seg 1 by FINSEQ_1:def 8; then len(<*lower_bound A*>)=1 by FINSEQ_1:def 3; hence A9: len (s1^<*upper_bound A*>) = len (<*lower_bound A*>^s2) by A6,A8, FINSEQ_1:22; thus len (s1^<*upper_bound A*>) = len p by A1,A8; let i; A10: In(upper_bound divset(D,i),REAL) = upper_bound divset(D,i); A11: In(lower_bound divset(D,i),REAL) = lower_bound divset(D,i); assume A12: i in dom (s1^<*upper_bound A*>); then A13: (s1^<*ub*>)/.i=(s1^<*ub*>).i by PARTFUN1:def 6; i in Seg(len (s1^<*upper_bound A*>)) by A12,FINSEQ_1:def 3; then i in dom (<*lower_bound A*>^s2) by A9,FINSEQ_1:def 3; then A14: (<*lb*>^s2)/.i=(<*lower_bound A*>^s2).i by PARTFUN1:def 6; A15: len D = 1 or len D is non trivial by NAT_2:def 1; now per cases by A15,NAT_2:29; suppose A16: len D = 1; then A17: i in Seg 1 by A8,A12,FINSEQ_1:def 3; then A18: i = 1 by FINSEQ_1:2,TARSKI:def 1; s1={} by A5,A16; then s1^<*upper_bound A*> = <*upper_bound A*> by FINSEQ_1:34; then A19: (s1^<*ub*>)/.i=upper_bound A by A13,A18,FINSEQ_1:def 8; A20: i in dom D by A16,A17,FINSEQ_1:def 3; s2={} by A6,A16; then <*lower_bound A*>^s2 = <*lower_bound A*> by FINSEQ_1:34; then A21: (<*lb*>^s2)/.i=lower_bound A by A14,A18,FINSEQ_1:def 8; D.i=upper_bound A by A16,A18,Def1; then A22: upper_bound divset(D,i)=upper_bound A by A18,A20,Def3; p.i=upper_bound divset(D,i)-lower_bound divset(D,i) by A3,A16,A17; hence thesis by A18,A20,A19,A21,A22,Def3; end; suppose A23: len D >= 2; 1 = 2 - 1; then A24: k>=1 by A23,XREAL_1:9; now per cases; suppose A25: i=1; then A26: i in Seg 1 by FINSEQ_1:2,TARSKI:def 1; then i in dom <*lower_bound A*> by FINSEQ_1:def 8; then (<*lower_bound A*>^s2).i=<*lower_bound A*>.i by FINSEQ_1:def 7 ; then A27: (<*lower_bound A*>^s2).i = lower_bound A by A25,FINSEQ_1:def 8; Seg 1 c= Seg k by A24,FINSEQ_1:5; then i in Seg k by A26; then A28: i in dom s1 by A5,FINSEQ_1:def 3; then (s1^<*upper_bound A*>).i=s1.i by FINSEQ_1:def 7; then A29: (s1^<*ub*>).i=upper_bound divset(D,i) by A5,A28,A10; A30: i in Seg 2 by A25,FINSEQ_1:2,TARSKI:def 2; A31: Seg 2 c= Seg len D by A23,FINSEQ_1:5; then i in Seg(len D) by A30; then A32: i in dom D by FINSEQ_1:def 3; p.i=upper_bound divset(D,i)-lower_bound divset(D,i) by A3,A31,A30; hence thesis by A13,A14,A25,A32,A29,A27,Def3; end; suppose A33: i=len D; then i-len s1 in Seg 1 by A5,FINSEQ_1:2,TARSKI:def 1; then A34: i-len s1 in dom <*upper_bound A*> by FINSEQ_1:def 8; i=i-len s1 + len s1; then (s1^<*upper_bound A*>).i=<*upper_bound A*>.(i-len s1) by A34, FINSEQ_1:def 7; then A35: (s1^<*ub*>)/.i=upper_bound A by A5,A13,A33, FINSEQ_1:def 8; A36: i<>1 by A23,A33; i in Seg(len D) by A33,FINSEQ_1:3; then A37: i in dom D by FINSEQ_1:def 3; p.i=upper_bound divset(D,i)-lower_bound divset(D,i) by A3,A33, FINSEQ_1:3; then p.i=upper_bound divset(D,i)-D.(i-1) by A37,A36,Def3; then A38: p.i=D.i-D.(i-1) by A37,A36,Def3; A39: i-len <*lower_bound A*> = i-1 by FINSEQ_1:40; i-1<>0 by A23,A33; then A40: i-1 in Seg k by A33,FINSEQ_1:3; then A41: i-len <*lower_bound A*> in dom s2 by A6,A39,FINSEQ_1:def 3; len <*lower_bound A*> + (i - len <* lower_bound A*>) = i; then A42: (<*lb*>^s2).i = s2.(i-1) by A41,A39,FINSEQ_1:def 7; reconsider i1=i-1 as Nat by A40; (<*lb*>^s2).i = G(i1) by A6,A39,A41,A42 .= lower_bound divset(D,i); then (<*lower_bound A*>^s2).i = D.(i-1) by A37,A36,Def3; hence thesis by A14,A33,A35,A38,Def1; end; suppose A43: i<>1 & i<>len D; len s1+len <*upper_bound A*> = k+1 by A5,FINSEQ_1:39; then A44: i in Seg(len D) by A12,FINSEQ_1:def 7; A45: i in dom s1 & i in Seg k & i-1 in Seg k & i-1+1=i & i-len<* lower_bound A*> in dom s2 proof i <> 0 by A44,FINSEQ_1:1; then i is non trivial by A43,NAT_2:def 1; then i >= 1+1 by NAT_2:29; then A46: i-1 >= 1 by XREAL_1:19; A47: 1 <= i by A44,FINSEQ_1:1; i <= len D by A44,FINSEQ_1:1; then A48: i < k + 1 by A43,XXREAL_0:1; then A49: i <= k by NAT_1:13; then i in Seg(len s1) by A5,A47,FINSEQ_1:1; hence i in dom s1 by FINSEQ_1:def 3; thus i in Seg k by A47,A49,FINSEQ_1:1; i <= k by A48,NAT_1:13; then i-1 <= k-1 by XREAL_1:9; then A50: i-1+0 <= k-1+1 by XREAL_1:7; ex j being Nat st i = 1 + j by A47,NAT_1:10; hence i-1 in Seg k by A46,A50,FINSEQ_1:1; then A51: i-len<*lower_bound A*> in Seg(len s2) by A6,FINSEQ_1:39; thus i-1+1=i; thus thesis by A51,FINSEQ_1:def 3; end; then A52: i-len<*lower_bound A*> in Seg(len s2) by FINSEQ_1:def 3; then i-len<*lower_bound A*> <= len s2 by FINSEQ_1:1; then A53: i <= len<*lower_bound A*>+len s2 by XREAL_1:20; 1 <= i-len<*lower_bound A*> by A52,FINSEQ_1:1; then len<*lower_bound A*>+1 <= i by XREAL_1:19; then (<*lower_bound A*>^s2).i = s2.(i-len<*lower_bound A*>) by A53, FINSEQ_1:23; then (<*lower_bound A*>^s2).i=s2.(i-1) by FINSEQ_1:39; then A54: (<*lower_bound A*>^s2).i= lower_bound divset(D,i) by A6,A7,A45,A11; (s1^<*upper_bound A*>).i = s1.i by A45,FINSEQ_1:def 7; then (s1^<*upper_bound A*>).i = upper_bound divset(D,i) by A5,A45,A10; hence thesis by A3,A13,A14,A44,A54; end; end; hence thesis; end; end; hence thesis; end; then Sum p = Sum(s1^<*ub*>)-Sum(<*lb*>^s2) by Th20; then Sum p=Sum s1 + upper_bound A -Sum(<*lb*>^s2) by RVSUM_1:74; then A55: Sum p=Sum s1 + upper_bound A - (lower_bound A + Sum s2) by RVSUM_1:76; A56: dom s1 = Seg k by A5,FINSEQ_1:def 3; A57: for i st i in Seg k holds upper_bound divset(D,i) =lower_bound divset(D ,i+1) proof let i; A58: 1+0 <= i+1 by XREAL_1:7; assume A59: i in Seg k; then i <= k by FINSEQ_1:1; then i+1 <= k+1 by XREAL_1:7; then i+1 in Seg(len D) by A58,FINSEQ_1:1; then A60: i+1 in dom D by FINSEQ_1:def 3; k + 1 = len D; then k <= len D by NAT_1:11; then Seg k c= Seg len D by FINSEQ_1:5; then i in Seg (len D) by A59; then A61: i in dom D by FINSEQ_1:def 3; A62: i+1-1=i; now per cases; suppose A63: i=1; then upper_bound divset(D,i) = D.i by A61,Def3; hence thesis by A60,A62,A63,Def3; end; suppose A64: i<>1; i >= 1 by A59,FINSEQ_1:1; then i+1>=1+1 by XREAL_1:6; then A65: i+1 <> 1; upper_bound divset(D,i) = D.i by A61,A64,Def3; hence thesis by A60,A62,A65,Def3; end; end; hence thesis; end; for i being Nat st i in dom s1 holds s1.i = s2.i proof let i be Nat; A66: In(upper_bound divset(D,i),REAL) = upper_bound divset(D,i); A67: In(lower_bound divset(D,i+1),REAL) = lower_bound divset(D,i+1); assume A68: i in dom s1; then s1.i = upper_bound divset(D,i) by A5,A66; then s1.i= lower_bound divset(D,i+1) by A57,A56,A68; hence thesis by A6,A7,A56,A68,A67; end; then A69: s1=s2 by A5,A6,FINSEQ_2:9; A70: len lower_volume(chi(A,A),D) = len D by Def6; then A71: dom lower_volume(chi(A,A),D) = Seg len D by FINSEQ_1:def 3; for i being Nat st i in dom lower_volume(chi(A,A),D) holds lower_volume(chi(A,A),D).i = p.i proof let i be Nat; A72: In(vol(divset(D,i)),REAL) = vol(divset(D,i)); assume A73: i in dom lower_volume(chi(A,A),D); then i in dom D by A70,FINSEQ_3:29; then lower_volume(chi(A,A),D).i=vol(divset(D,i)) by Th17; hence thesis by A1,A2,A71,A73,A72; end; hence thesis by A1,A69,A55,A70,FINSEQ_2:9; end; theorem Th22: Sum(upper_volume(chi(A,A),D))=vol(A) proof A1: for i be Nat st 1 <= i & i <= len(lower_volume(chi(A,A),D)) holds lower_volume(chi(A,A),D).i=upper_volume(chi(A,A),D).i proof let i be Nat; assume that A2: 1 <= i and A3: i <= len(lower_volume(chi(A,A),D)); i <= len D by A3,Def6; then A4: i in dom D by A2,FINSEQ_3:25; then lower_volume(chi(A,A),D).i=vol(divset(D,i)) by Th17 .=upper_volume(chi(A,A),D).i by A4,Th18; hence thesis; end; len (lower_volume(chi(A,A),D)) = len D by Def6 .= len (upper_volume(chi(A,A),D)) by Def5; then lower_volume(chi(A,A),D)=upper_volume(chi(A,A),D) by A1,FINSEQ_1:14; hence thesis by Th21; end; begin :: Some properties of Darboux sum registration let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; let D be Division of A; cluster upper_volume(f,D) -> non empty; coherence proof len upper_volume(f,D) = len D by Def5; hence thesis; end; cluster lower_volume(f,D) -> non empty; coherence proof len lower_volume(f,D) = len D by Def6; hence thesis; end; end; theorem Th23: f|A is bounded_below implies (lower_bound rng f)*vol(A) <= lower_sum(f,D) proof assume A1: f|A is bounded_below; A2: for i st i in dom D holds (lower_bound rng f)*vol(divset(D,i)) <= ( lower_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i; A3: rng(f|divset(D,i)) c= rng f by RELAT_1:70; A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48; A5: dom f = A by FUNCT_2:def 1; assume i in dom D; then dom (f|divset(D,i)) = divset(D,i) by A5,Th6,RELAT_1:62; then A6: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42; rng f is bounded_below by A1,Th9; hence thesis by A3,A6,A4,SEQ_4:47,XREAL_1:64; end; A7: for i st i in dom D holds (lower_bound rng f)*(lower_volume(chi(A,A),D) .i) <= (lower_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i; assume A8: i in dom D; then (lower_bound rng f)*vol(divset(D,i)) <= (lower_bound rng (f|divset(D, i)))*vol(divset(D,i)) by A2; hence thesis by A8,Th17; end; Sum((lower_bound rng f)*lower_volume(chi(A,A),D)) <=Sum(lower_volume(f, D)) proof len (lower_volume(chi(A,A),D)) = len ((lower_bound rng f)* lower_volume(chi(A,A),D)) by FINSEQ_2:33; then A9: len ((lower_bound rng f)*lower_volume(chi(A,A),D))=len D by Def6; deffunc G(Nat)= In((lower_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL); deffunc F(set)= In((lower_bound rng f)*(lower_volume(chi(A,A),D).$1),REAL); consider p being FinSequence of REAL such that A10: len p = len D & for i be Nat st i in dom p holds p.i=F(i) from FINSEQ_2:sch 1; A11: dom p = Seg len D by A10,FINSEQ_1:def 3; for i be Nat st 1 <= i & i <= len p holds p.i=((lower_bound rng f)* lower_volume(chi(A,A),D)).i proof let i be Nat; assume that A12: 1 <= i and A13: i <= len p; i in Seg(len D) by A10,A12,A13,FINSEQ_1:1; then p.i=F(i) by A10,A11; hence thesis by RVSUM_1:44; end; then A14: p=(lower_bound rng f)*lower_volume(chi(A,A),D) by A10,A9,FINSEQ_1:14; reconsider p as Element of (len D)-tuples_on REAL by A10,FINSEQ_2:92; consider q being FinSequence of REAL such that A15: len q = len D & for i be Nat st i in dom q holds q.i=G(i) from FINSEQ_2:sch 1; A16: for i be Nat st i in dom q holds q.i=(lower_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i be Nat; assume i in dom q; then q.i = G(i) by A15; hence thesis; end; A17: dom q = dom D by A15,FINSEQ_3:29; then A18: q=lower_volume(f,D) by A15,Def6,A16; reconsider q as Element of (len D)-tuples_on REAL by A15,FINSEQ_2:92; now let i be Nat; assume A19: i in Seg (len D); then A20: p.i=F(i) by A10,A11; A21: i in dom D by A19,FINSEQ_1:def 3; then q.i=G(i) by A15,A17; hence p.i <= q.i by A7,A20,A21; end; hence thesis by A18,A14,RVSUM_1:82; end; then (lower_bound rng f)*Sum(lower_volume(chi(A,A),D)) <=Sum(lower_volume(f, D)) by RVSUM_1:87; hence thesis by Th21; end; theorem f|A is bounded_above & i in dom D implies (upper_bound rng f)*vol( divset(D,i)) >= (upper_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof A1: dom f = A by FUNCT_2:def 1; assume f|A is bounded_above; then A2: rng f is bounded_above by Th11; assume i in dom D; then dom (f|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62; then A3: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42; A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48; rng(f|divset(D,i)) c= rng f by RELAT_1:70; hence thesis by A3,A2,A4,SEQ_4:48,XREAL_1:64; end; theorem Th25: f|A is bounded_above implies upper_sum(f,D) <= (upper_bound rng f)*vol(A) proof assume A1: f|A is bounded_above; A2: for i st i in Seg(len D) holds (upper_bound rng f)*vol(divset(D,i)) >= ( upper_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i; A3: rng(f|divset(D,i)) c= rng f by RELAT_1:70; A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48; assume i in Seg(len D); then A5: i in dom D by FINSEQ_1:def 3; dom f = A by FUNCT_2:def 1; then dom (f|divset(D,i)) = divset(D,i) by A5,Th6,RELAT_1:62; then A6: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42; rng f is bounded_above by A1,Th11; hence thesis by A3,A6,A4,SEQ_4:48,XREAL_1:64; end; A7: for i st i in Seg(len D) holds (upper_bound rng f)*(upper_volume(chi(A, A),D).i) >= (upper_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i; assume A8: i in Seg(len D); then A9: i in dom D by FINSEQ_1:def 3; (upper_bound rng f)*vol(divset(D,i)) >= (upper_bound rng (f|divset(D, i)))*vol(divset(D,i)) by A2,A8; hence thesis by A9,Th18; end; Sum((upper_bound rng f)*upper_volume(chi(A,A),D)) >=Sum(upper_volume(f, D)) proof len (upper_volume(chi(A,A),D)) = len ((upper_bound rng f)* upper_volume(chi(A,A),D)) by FINSEQ_2:33; then A10: len ((upper_bound rng f)*upper_volume(chi(A,A),D))=len D by Def5; deffunc G(Nat)= In((upper_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL); deffunc F(set)=In((upper_bound rng f)*(upper_volume(chi(A,A),D).$1),REAL); consider p being FinSequence of REAL such that A11: len p = len D & for i be Nat st i in dom p holds p.i=F(i) from FINSEQ_2:sch 1; A12: dom p = Seg len D by A11,FINSEQ_1:def 3; for i be Nat st 1 <= i & i <= len p holds p.i=((upper_bound rng f)* upper_volume(chi(A,A),D)).i proof let i be Nat; assume that A13: 1 <= i and A14: i <= len p; i in Seg(len D) by A11,A13,A14,FINSEQ_1:1; then p.i=F(i) by A11,A12; hence thesis by RVSUM_1:44; end; then A15: p=(upper_bound rng f)*upper_volume(chi(A,A),D) by A11,A10,FINSEQ_1:14; reconsider p as Element of (len D)-tuples_on REAL by A11,FINSEQ_2:92; consider q being FinSequence of REAL such that A16: len q = len D & for i be Nat st i in dom q holds q.i=G(i) from FINSEQ_2:sch 1; A17: for i be Nat st i in dom q holds q.i= (upper_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i be Nat; assume i in dom q; then q.i=G(i) by A16; hence thesis; end; A18: dom q = dom D by A16,FINSEQ_3:29; then A19: q=upper_volume(f,D) by A16,Def5,A17; reconsider q as Element of (len D)-tuples_on REAL by A16,FINSEQ_2:92; now let i be Nat; assume A20: i in Seg (len D); then i in dom D by FINSEQ_1:def 3; then A21: q.i=G(i) by A16,A18; p.i=F(i) by A11,A12,A20; hence q.i <= p.i by A7,A20,A21; end; hence thesis by A19,A15,RVSUM_1:82; end; then (upper_bound rng f)*Sum(upper_volume(chi(A,A),D))>= Sum(upper_volume(f, D)) by RVSUM_1:87; hence thesis by Th22; end; theorem Th26: f|A is bounded implies lower_sum(f,D) <= upper_sum(f,D) proof deffunc F(Nat)= In((lower_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL); consider p being FinSequence of REAL such that A1: len p = len D & for i be Nat st i in dom p holds p.i=F(i) from FINSEQ_2:sch 1; A2: for i be Nat st i in dom p holds p.i= (lower_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i be Nat; assume i in dom p; then p.i= F(i) by A1; hence thesis; end; assume A3: f|A is bounded; then A4: rng f is bounded_above by Th11; A5: dom p = dom D by A1,FINSEQ_3:29; reconsider p as Element of (len D)-tuples_on REAL by A1,FINSEQ_2:92; deffunc G(Nat)= In((upper_bound rng (f|divset(D,$1)))*vol(divset(D,$1)),REAL); consider q being FinSequence of REAL such that A6: len q = len D & for i be Nat st i in dom q holds q.i=G(i) from FINSEQ_2:sch 1; A7: for i be Nat st i in dom q holds q.i= (upper_bound rng (f|divset(D,i)))*vol(divset(D,i)) proof let i be Nat; assume i in dom q; then q.i=G(i) by A6; hence thesis; end; A8: dom q = dom D by A6,FINSEQ_3:29; then len q = len D by FINSEQ_3:29; then A9: q=upper_volume(f,D) by A7,Def5,A8; reconsider q as Element of (len D)-tuples_on REAL by A6,FINSEQ_2:92; A10: rng f is bounded_below by A3,Th9; for i be Nat st i in Seg(len D) holds p.i <= q.i proof let i be Nat; A11: dom f = A by FUNCT_2:def 1; assume A12: i in Seg(len D); then A13: i in dom D by FINSEQ_1:def 3; i in dom D by A12,FINSEQ_1:def 3; then dom (f|divset(D,i)) = divset(D,i) by A11,Th6,RELAT_1:62; then A14: rng(f|divset(D,i)) is non empty Subset of REAL by RELAT_1:42; A15: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48; A16: rng (f|divset(D,i)) is bounded_above by A4,RELAT_1:70,XXREAL_2:43; rng (f|divset(D,i)) is bounded_below by A10,RELAT_1:70,XXREAL_2:44; then lower_bound (rng(f|divset(D,i)))*vol(divset(D,i)) <= upper_bound (rng (f|divset(D,i)))*vol(divset(D,i)) by A16,A14,A15,SEQ_4:11,XREAL_1:64; then p.i <= upper_bound (rng(f|divset(D,i)))*vol(divset(D,i)) by A5,A13,A2; hence thesis by A8,A13,A7; end; then Sum p <= Sum q by RVSUM_1:82; hence thesis by A1,A5,A9,Def6,A2; end; definition let D1, D2 be FinSequence; pred D1 <= D2 means len D1 <= len D2 & rng D1 c= rng D2; reflexivity; end; notation let D1, D2 be FinSequence; synonym D2 >= D1 for D1 <= D2; end; theorem len D1 = 1 implies D1 <= D2 proof A1: D2.(len D2) = upper_bound A by Def1; assume A2: len D1 = 1; then D1.1 = upper_bound A by Def1; then D1=<*upper_bound A*> by A2,FINSEQ_1:40; then A3: rng D1 = {upper_bound A} by FINSEQ_1:38; A4: len D2 in Seg(len D2) by FINSEQ_1:3; hence len D1 <= len D2 by A2,FINSEQ_1:1; len D2 in dom D2 by A4,FINSEQ_1:def 3; then upper_bound A in rng D2 by A1,FUNCT_1:def 3; then rng D1 is Subset of rng D2 by A3,SUBSET_1:41; hence thesis; end; theorem Th28: f|A is bounded_above & len D1 = 1 implies upper_sum(f,D1) >= upper_sum(f,D2) proof assume that A1: f|A is bounded_above and A2: len D1=1; 1 in Seg(len D1) by A2,FINSEQ_1:3; then A3: 1 in dom D1 by FINSEQ_1:def 3; then A4: lower_bound divset(D1,1)=lower_bound A by Def3; A5: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1).] by Th2; upper_bound divset(D1,1)=D1.1 by A3,Def3 .=upper_bound A by A2,Def1; then A6: divset(D1,1)=A by A4,A5,Th2; A7: upper_volume(f,D1).1=(upper_bound (rng(f|divset(D1,1))))*vol(divset(D1, 1)) by A3,Def5; reconsider ubv = (upper_bound (rng (f|divset(D1,1))))*vol(divset(D1,1)) as Element of REAL by XREAL_0:def 1; len upper_volume(f,D1) = 1 by A2,Def5; then upper_sum(f,D1)=Sum <*ubv*> by A7,FINSEQ_1:40 .=(upper_bound (rng(f|A)))*vol(A) by A6,FINSOP_1:11 .=(upper_bound (rng f))*vol(A); hence thesis by A1,Th25; end; theorem Th29: f|A is bounded_below & len D1 = 1 implies lower_sum(f,D1) <= lower_sum(f,D2) proof assume that A1: f|A is bounded_below and A2: len D1=1; 1 in Seg(len D1) by A2,FINSEQ_1:3; then A3: 1 in dom D1 by FINSEQ_1:def 3; then A4: lower_bound divset(D1,1)=lower_bound A by Def3; upper_bound divset(D1,1)=D1.1 by A3,Def3 .=upper_bound A by A2,Def1; then divset(D1,1)=[.lower_bound A,upper_bound A.] by A4,Th2; then A5: divset(D1,1)=A by Th2; A6: lower_volume(f,D1).1=(lower_bound (rng(f|divset(D1,1))))*vol(divset(D1, 1)) by A3,Def6; reconsider lbv =(lower_bound (rng (f|divset(D1,1))))*vol(divset( D1,1)) as Element of REAL by XREAL_0:def 1; len lower_volume(f,D1) = 1 by A2,Def6; then lower_sum(f,D1)=Sum <*lbv*> by A6,FINSEQ_1:40 .=(lower_bound (rng(f|A)))*vol(A) by A5,FINSOP_1:11 .=(lower_bound (rng f))*vol(A); hence thesis by A1,Th23; end; theorem i in dom D implies ex A1,A2 be non empty closed_interval Subset of REAL st A1=[.lower_bound A,D.i .] & A2=[. D.i,upper_bound A.] & A=A1 \/ A2 proof assume i in dom D; then A1: D.i in rng D by FUNCT_1:def 3; rng D c= A by Def1; then D.i in A by A1; then D.i in [.lower_bound A,upper_bound A.] by Th2; then D.i in {a: lower_bound A <= a & a <= upper_bound A} by RCOMP_1:def 1; then A2: ex a st a=D.i & lower_bound A <= a & a <= upper_bound A; then reconsider A1 =[.lower_bound A,D.i .] as non empty closed_interval Subset of REAL by MEASURE5:14; reconsider A2 = [. D.i,upper_bound A.] as non empty closed_interval Subset of REAL by A2,MEASURE5:14; take A1, A2; A1 \/ A2 = [.lower_bound A,upper_bound A.] by A2,XXREAL_1:174 .= A by Th2; hence thesis; end; theorem Th31: i in dom D1 & D1 <= D2 implies ex j st j in dom D2 & D1.i=D2.j proof assume i in dom D1; then A1: D1.i in rng D1 by FUNCT_1:def 3; assume D1 <= D2; then rng D1 c= rng D2; then consider x1 being object such that A2: x1 in dom D2 and A3: D1.i=D2.x1 by A1,FUNCT_1:def 3; reconsider x1 as Element of NAT by A2; take x1; thus thesis by A2,A3; end; definition let A, D1, D2; let i be Nat; assume A1: D1 <= D2; func indx(D2,D1,i) -> Element of NAT means :Def18: it in dom D2 & D1.i=D2.it if i in dom D1 otherwise it = 0; existence by A1,Th31; uniqueness proof let m,n be Element of NAT; hereby assume that i in dom D1 and A2: m in dom D2 and A3: D1.i=D2.m and A4: n in dom D2 and A5: D1.i=D2.n; assume A6: m <> n; now per cases by A6,XXREAL_0:1; suppose m < n; hence contradiction by A2,A3,A4,A5,SEQM_3:def 1; end; suppose n < m; hence contradiction by A2,A3,A4,A5,SEQM_3:def 1; end; end; hence contradiction; end; assume that not i in dom D1 and A7: m=0 and A8: n=0; thus thesis by A7,A8; end; correctness; end; theorem Th32: for p be increasing FinSequence of REAL, n be Element of NAT holds n <= len p implies p/^n is increasing FinSequence of REAL proof let p be increasing FinSequence of REAL; let n be Element of NAT; assume A1: n <= len p; for i,j being Nat st i in dom (p/^n) & j in dom (p/^n) & i< j holds (p/^n).i < (p /^n).j proof let i,j be Nat; assume that A2: i in dom(p/^n) and A3: j in dom(p/^n) and A4: i= 0 + 1 by XREAL_1:6; then A8: 1 <= len M by A6,A7,FINSEQ_1:17; then len M in Seg(len M) by FINSEQ_1:1; then A9: len M in dom M by FINSEQ_1:def 3; 1 in Seg(len M) by A8,FINSEQ_1:1; then A10: 1 in dom M by FINSEQ_1:def 3; then M.1 <= M.(len M) by A8,A9,SEQ_4:137; then reconsider B=[. M.1,M.(len M) .] as non empty closed_interval Subset of REAL by MEASURE5:14; A11: B=[.lower_bound B,upper_bound B.] by Th2; then A12: lower_bound B = M.1 by Th3; A13: M.(len M)=upper_bound B by A11,Th3; for x being Element of REAL st x in rng M holds x in B proof let x be Element of REAL; assume x in rng M; then consider i such that A14: i in dom M and A15: x=M.i by PARTFUN1:3; A16: i in Seg(len M) by A14,FINSEQ_1:def 3; then i <= len M by FINSEQ_1:1; then A17: M.i <= M.(len M) by A9,A14,SEQ_4:137; 1 <= i by A16,FINSEQ_1:1; then M.1 <= M.i by A10,A14,SEQ_4:137; then M.i in {a: M.1 <= a & a <= M.(len M)} by A17; hence thesis by A15,RCOMP_1:def 1; end; then rng M c= B; then M is Division of B by A13,Def1; hence thesis by A12,A13; end; theorem Th35: i in dom D & j in dom D & i<=j & D.i>=lower_bound B & D.j= upper_bound B implies mid(D,i,j) is Division of B proof assume that A1: i in dom D and A2: j in dom D and A3: i<=j and A4: D.i>=lower_bound B and A5: D.j=upper_bound B; A6: j-i+1+i-1=j; i in Seg(len D) by A1,FINSEQ_1:def 3; then A7: 1 <= i by FINSEQ_1:1; 0<=j-i by A3,XREAL_1:48; then A8: 0+1<=j-i+1 by XREAL_1:6; j in Seg(len D) by A2,FINSEQ_1:def 3; then A9: j<=len D by FINSEQ_1:1; consider A1 be non empty closed_interval Subset of REAL such that A10: lower_bound A1=mid(D,i,j).1 and A11: upper_bound A1=mid(D,i,j).(len mid(D,i,j)) and A12: mid(D,i,j) is Division of A1 by A1,A2,A3,Th34; A13: len mid(D,i,j)=j-i+1 by A1,A2,A3,Lm1; A14: 1+i-1 = i; for x being Element of REAL st x in A1 holds x in B proof let x be Element of REAL; assume x in A1; then x in [.lower_bound A1,upper_bound A1.] by Th2; then x in {a: lower_bound A1 <= a & a <= upper_bound A1} by RCOMP_1:def 1; then A15: ex a st x=a & lower_bound A1 <= a & a <= upper_bound A1; then D.i <= x by A3,A10,A7,A9,A8,A14,FINSEQ_6:122; then A16: lower_bound B <= x by A4,XXREAL_0:2; x <= upper_bound B by A3,A5,A11,A13,A7,A9,A8,A6,A15,FINSEQ_6:122; then x in {a: lower_bound B <= a & a <= upper_bound B} by A16; then x in [.lower_bound B,upper_bound B.] by RCOMP_1:def 1; hence thesis by Th2; end; then A17: A1 c= B; rng mid(D,i,j) c= A1 by A12,Def1; then A18: rng mid(D,i,j) c= B by A17; mid(D,i,j).(len mid(D,i,j))=D.j by A3,A13,A7,A9,A8,A6,FINSEQ_6:122; hence thesis by A5,A12,A18,Def1; end; definition let p be FinSequence of REAL; func PartSums(p) -> FinSequence of REAL means :Def19: len it = len p & for i be Nat st i in dom p holds it.i=Sum(p|i); existence proof deffunc F(Nat)= In(Sum(p|$1),REAL); consider IT being FinSequence of REAL such that A1: len IT = len p & for i be Nat st i in dom IT holds IT.i=F(i) from FINSEQ_2:sch 1; take IT; thus len IT = len p by A1; let i be Nat; assume i in dom p; then i in dom IT by A1,FINSEQ_3:29; then IT.i=F(i) by A1; hence thesis; end; uniqueness proof let p1,p2 be FinSequence of REAL such that A2: len p1=len p and A3: for i be Nat st i in dom p holds p1.i=Sum(p|i) and A4: len p2=len p and A5: for i be Nat st i in dom p holds p2.i=Sum(p|i); for i be Nat st 1 <= i & i <= len p1 holds p1.i=p2.i proof let i be Nat; assume that A6: 1 <= i and A7: i <= len p1; A8: i in dom p by A2,A6,A7,FINSEQ_3:25; then p1.i=Sum(p|i) by A3; hence thesis by A5,A8; end; hence thesis by A2,A4,FINSEQ_1:14; end; end; theorem Th36: D1 <= D2 & f|A is bounded_above implies for i be non zero Element of NAT holds (i in dom D1 implies Sum(upper_volume(f,D1)|i) >= Sum( upper_volume(f,D2)|indx(D2,D1,i))) proof assume that A1: D1 <= D2 and A2: f|A is bounded_above; for i be non zero Nat holds i in dom D1 implies Sum(upper_volume(f,D1)| i) >= Sum(upper_volume(f,D2)|indx(D2,D1,i)) proof defpred P[Nat] means $1 in dom D1 implies Sum(upper_volume(f,D1)|$1) >= Sum(upper_volume(f,D2)|indx(D2,D1,$1)); A3: P[1] proof reconsider g=f|divset(D1,1) as PartFunc of divset(D1,1),REAL by PARTFUN1:10; set B=divset(D1,1); set DD1=mid(D1,1,1); A4: dom g = dom f /\ divset(D1,1) by RELAT_1:61; assume A5: 1 in dom D1; then A6: D1.1 = upper_bound B by Def3; then A7: D2.indx(D2,D1,1) = upper_bound B by A1,A5,Def18; D1.1 >= lower_bound B by A6,SEQ_4:11; then reconsider DD1 as Division of B by A5,A6,Th35; 1 in Seg(len D1) by A5,FINSEQ_1:def 3; then A8: 1 <= len D1 by FINSEQ_1:1; then A9: len mid(D1,1,1)=1-'1+1 by FINSEQ_6:118; A10: len upper_volume(g,DD1)=len DD1 by Def5 .= 1 by A9,XREAL_1:235; A11: len mid(D1,1,1)=1 by A9,XREAL_1:235; then A12: len mid(D1,1,1)=len (D1|1); for k be Nat st 1 <= k & k <= len mid(D1,1,1) holds mid(D1,1,1).k=(D1|1).k proof let k be Nat; assume that A13: 1 <= k and A14: k <= len mid(D1,1,1); k in Seg(len(D1|1)) by A12,A13,A14,FINSEQ_1:1; then k in dom (D1|1) by FINSEQ_1:def 3; then k in dom (D1|Seg 1) by FINSEQ_1:def 15; then A15: (D1|Seg 1).k = D1.k by FUNCT_1:47; A16: k = 1 by A11,A13,A14,XXREAL_0:1; then mid(D1,1,1).k = D1.(1+1-1) by A8,FINSEQ_6:118; hence thesis by A16,A15,FINSEQ_1:def 15; end; then A17: mid(D1,1,1)=D1|1 by A12,FINSEQ_1:14; A18: for i be Nat st 1 <= i & i <= len upper_volume(g,DD1) holds upper_volume(g,DD1).i=(upper_volume(f,D1)|1).i proof let i be Nat; assume that A19: 1 <= i and A20: i <= len upper_volume(g,DD1); A21: 1 in Seg 1 by FINSEQ_1:3; dom(D1|Seg 1) = dom D1 /\ Seg 1 by RELAT_1:61; then A22: 1 in dom(D1|Seg 1) by A5,A21,XBOOLE_0:def 4; dom(upper_volume(f,D1))=Seg(len upper_volume(f,D1)) by FINSEQ_1:def 3 .=Seg(len D1) by Def5; then A23: dom(upper_volume(f,D1)|Seg 1) =Seg(len D1) /\ Seg 1 by RELAT_1:61 .=Seg 1 by A8,FINSEQ_1:7; len DD1 = 1 by A9,XREAL_1:235; then A24: 1 in dom DD1 by A21,FINSEQ_1:def 3; A25: (upper_volume(f,D1)|1).i=(upper_volume(f,D1)|Seg 1).i by FINSEQ_1:def 15 .=(upper_volume(f,D1)|Seg 1).1 by A10,A19,A20,XXREAL_0:1 .=upper_volume(f,D1).1 by A23,FINSEQ_1:3,FUNCT_1:47 .=(upper_bound (rng(f|divset(D1,1))))*vol(divset(D1,1)) by A5,Def5; A26: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1) .] by Th2 .=[.lower_bound A,upper_bound divset(D1,1).] by A5,Def3 .=[.lower_bound A,D1.1 .] by A5,Def3; A27: upper_volume(g,DD1).i = upper_volume(g,DD1).1 by A10,A19,A20,XXREAL_0:1 .= (upper_bound (rng (g|divset(DD1,1))))*vol(divset(DD1,1)) by A24 ,Def5; divset(DD1,1)=[.lower_bound divset(DD1,1), upper_bound divset(DD1 ,1).] by Th2 .=[.lower_bound B,upper_bound divset(DD1,1).] by A24,Def3 .=[.lower_bound B,DD1.1 .] by A24,Def3 .=[.lower_bound A,(D1|1).1 .] by A5,A17,Def3 .=[.lower_bound A,(D1|Seg 1).1 .] by FINSEQ_1:def 15 .=[.lower_bound A,D1.1 .] by A22,FUNCT_1:47; hence thesis by A27,A26,A25; end; A28: g|divset(D1,1) is bounded_above proof consider a be Real such that A29: for x being object st x in A /\ dom f holds f.x <= a by A2,RFUNCT_1:70; for x being object st x in divset(D1,1) /\ dom g holds g.x <= a proof let x be object; A30: dom g c= dom f by RELAT_1:60; assume x in divset(D1,1) /\ dom g; then A31: x in dom g by XBOOLE_0:def 4; A32: A /\ dom f = dom f by XBOOLE_1:28; then x in A /\ dom f by A31,A30; then reconsider x as Element of A; f.x <= a by A29,A31,A32,A30; hence thesis by A31,FUNCT_1:47; end; hence thesis by RFUNCT_1:70; end; A33: rng D2 c= A by Def1; A34: indx(D2,D1,1) in dom D2 by A1,A5,Def18; then A35: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3; then A36: 1 <= indx(D2,D1,1) by FINSEQ_1:1; A37: indx(D2,D1,1) <= len D2 by A35,FINSEQ_1:1; then 1 <= len D2 by A36,XXREAL_0:2; then 1 in Seg(len D2) by FINSEQ_1:1; then A38: 1 in dom D2 by FINSEQ_1:def 3; then D2.1 in rng D2 by FUNCT_1:def 3; then D2.1 in A by A33; then D2.1 in [.lower_bound A,upper_bound A.] by Th2; then D2.1 in {a: lower_bound A <= a & a <= upper_bound A} by RCOMP_1:def 1; then ex a st D2.1=a & lower_bound A <= a & a <= upper_bound A; then D2.1 >= lower_bound B by A5,Def3; then reconsider DD2=mid(D2,1,indx(D2,D1,1)) as Division of B by A34,A36,A38,A7,Th35; indx(D2,D1,1) in dom D2 by A1,A5,Def18; then A39: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3; then A40: 1 <= indx(D2,D1,1) by FINSEQ_1:1; A41: indx(D2,D1,1) <= len D2 by A39,FINSEQ_1:1; then A42: 1 <= len D2 by A40,XXREAL_0:2; then len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-'1+1 by A40,A41, FINSEQ_6:118; then A43: len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-1+1 by A40,XREAL_1:233; then A44: len mid(D2,1,indx(D2,D1,1))=len (D2|indx(D2,D1,1)) by A41,FINSEQ_1:59; A45: for k be Nat st 1 <= k & k <= len mid(D2,1,indx(D2,D1,1)) holds mid (D2,1,indx(D2,D1,1)).k=(D2|indx(D2,D1,1)).k proof let k be Nat; assume that A46: 1 <= k and A47: k <= len mid(D2,1,indx(D2,D1,1)); k in Seg len (D2|indx(D2,D1,1)) by A44,A46,A47,FINSEQ_1:1; then k in dom (D2|indx(D2,D1,1)) by FINSEQ_1:def 3; then k in dom (D2|Seg indx(D2,D1,1)) by FINSEQ_1:def 15; then A48: (D2|Seg indx(D2,D1,1)).k=D2.k by FUNCT_1:47; mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-'1) by A40,A41,A42,A46,A47, FINSEQ_6:118; then mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-1) by NAT_1:11,XREAL_1:233; hence thesis by A48,FINSEQ_1:def 15; end; then A49: mid(D2,1,indx(D2,D1,1))=D2|indx(D2,D1,1) by A44,FINSEQ_1:14; A50: for i be Nat st 1 <= i & i <= len upper_volume(g,DD2) holds upper_volume(g,DD2).i = (upper_volume(f,D2)|indx(D2,D1,1)).i proof let i be Nat; assume that A51: 1 <= i and A52: i <= len upper_volume(g,DD2); A53: i <= len DD2 by A52,Def5; then A54: i in Seg(len DD2) by A51,FINSEQ_1:1; then A55: i in dom DD2 by FINSEQ_1:def 3; divset(DD2,i)=divset(D2,i) proof Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5; then i in Seg(len D2) by A43,A54; then A56: i in dom D2 by FINSEQ_1:def 3; now per cases; suppose A57: i=1; then A58: 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A55,FINSEQ_1:def 15; then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61; then A59: 1 in dom D2 by XBOOLE_0:def 4; A60: divset(D2,i)= [.lower_bound divset(D2,1),upper_bound divset(D2,1).] by A57,Th2 .=[.lower_bound A,upper_bound divset(D2,1).] by A59,Def3 .=[.lower_bound A,D2.1 .] by A59,Def3; divset (DD2,i)=[.lower_bound divset(DD2,1), upper_bound divset(DD2,1).] by A57,Th2 .=[.lower_bound B,upper_bound divset(DD2,1).] by A55,A57,Def3 .=[.lower_bound B,DD2.1 .] by A55,A57,Def3 .=[.lower_bound B,(D2|indx(D2,D1,1)).1 .] by A45,A53,A57 .=[.lower_bound B,(D2|Seg indx(D2,D1,1)).1 .] by FINSEQ_1:def 15 .=[.lower_bound B,D2.1 .] by A58,FUNCT_1:47 .=[.lower_bound A,D2.1 .] by A5,Def3; hence thesis by A60; end; suppose A61: i<>1; A62: i-1 in dom(D2|Seg indx(D2,D1,1)) proof i is non trivial by A51,A61,NAT_2:def 1; then A63: i>=1+1 by NAT_2:29; then A64: 1 <= i-1 by XREAL_1:19; A65: ex j being Nat st i = 1 + j by A51,NAT_1:10; A66: i-1<=indx(D2,D1,1)-0 by A43,A53,XREAL_1:13; then i-1 <= len D2 by A37,XXREAL_0:2; then i-1 in Seg(len D2) by A65,A64,FINSEQ_1:1; then A67: i-1 in dom D2 by FINSEQ_1:def 3; i-1 >= 1 by A63,XREAL_1:19; then i-1 in Seg indx(D2,D1,1) by A65,A66,FINSEQ_1:1; then i-1 in dom D2 /\ Seg indx(D2,D1,1) by A67,XBOOLE_0:def 4; hence thesis by RELAT_1:61; end; DD2.(i-1)=(D2|indx(D2,D1,1)).(i-1) by A44,A45,FINSEQ_1:14 .=(D2|Seg indx(D2,D1,1)).(i-1) by FINSEQ_1:def 15; then A68: DD2.(i-1)=D2.(i-1) by A62,FUNCT_1:47; i <= len D2 by A43,A37,A53,XXREAL_0:2; then i in Seg(len D2) by A51,FINSEQ_1:1; then i in dom D2 by FINSEQ_1:def 3; then i in dom D2 /\ Seg indx(D2,D1,1) by A43,A54,XBOOLE_0:def 4; then A69: i in dom(D2|Seg indx(D2,D1,1)) by RELAT_1:61; DD2.i=(D2|indx(D2,D1,1)).i by A44,A45,FINSEQ_1:14 .=(D2|Seg indx(D2,D1,1)).i by FINSEQ_1:def 15; then A70: DD2.i=D2.i by A69,FUNCT_1:47; A71: divset(D2,i)= [.lower_bound divset(D2,i),upper_bound divset(D2,i).] by Th2 .=[. D2.(i-1),upper_bound divset(D2,i).] by A56,A61,Def3 .=[. D2.(i-1),D2.i .] by A56,A61,Def3; divset(DD2,i)=[.lower_bound divset(DD2,i), upper_bound divset(DD2,i).] by Th2 .=[. DD2.(i-1),upper_bound divset(DD2,i).] by A55,A61,Def3 .=[. D2.(i-1),D2.i .] by A55,A61,A68,A70,Def3; hence thesis by A71; end; end; hence thesis; end; then A72: upper_volume(g,DD2).i =(upper_bound (rng (g|divset(D2,i))))*vol( divset(D2,i)) by A55,Def5; Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5; then i in Seg(len D2) by A43,A54; then A73: i in dom D2 by FINSEQ_1:def 3; A74: i in dom DD2 by A54,FINSEQ_1:def 3; A75: now per cases; suppose A76: i=1; then 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A74,FINSEQ_1:def 15; then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61; then A77: 1 in dom D2 by XBOOLE_0:def 4; then A78: D2.1 <= D2.indx(D2,D1,1) by A34,A36,SEQ_4:137; lower_bound divset(D2,i)=lower_bound A by A76,A77,Def3; then A79: lower_bound divset(D2,i)=lower_bound divset(D1,1) by A5,Def3; upper_bound divset(D2,i)=D2.1 by A76,A77,Def3; then upper_bound divset(D2,i) <= D1.1 by A1,A5,A78,Def18; then A80: upper_bound divset(D2,i) <= upper_bound divset(D1,1) by A5,Def3; lower_bound divset(D1,1) <= upper_bound divset(D1,1) by SEQ_4:11; hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by A79,XXREAL_1:1; lower_bound divset(D2,i) <= upper_bound divset(D2,i) by SEQ_4:11; then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r & r<= upper_bound divset(D1,1)} by A79,A80; hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by RCOMP_1:def 1; end; suppose A81: i<>1; then i is non trivial by A51,NAT_2:def 1; then i >= 1+1 by NAT_2:29; then A82: 1 <= i-1 by XREAL_1:19; A83: ex j being Nat st i = 1 + j by A51,NAT_1:10; A84: rng D2 c= A by Def1; A85: lower_bound divset(D2,i)=D2.(i-1) by A73,A81,Def3; A86: lower_bound divset(D1,1)=lower_bound A by A5,Def3; A87: i-1 <= indx(D2,D1,1)-0 by A43,A53,XREAL_1:13; then i-1 <= len D2 by A37,XXREAL_0:2; then i-1 in Seg(len D2) by A83,A82,FINSEQ_1:1; then A88: i-1 in dom D2 by FINSEQ_1:def 3; then D2.(i-1) in rng D2 by FUNCT_1:def 3; then A89: lower_bound divset(D2,i) >= lower_bound divset(D1,1) by A85,A86,A84 ,SEQ_4:def 2; A90: upper_bound divset(D1,1)=D1.1 by A5,Def3; D2.(i-1)<= D2.indx(D2,D1,1) by A34,A87,A88,SEQ_4:137; then lower_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5 ,A85,A90,Def18; then lower_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r & r<= upper_bound divset(D1,1)} by A89; hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by RCOMP_1:def 1; A91: upper_bound divset(D2,i)=D2.i by A73,A81,Def3; D2.i in rng D2 by A73,FUNCT_1:def 3; then A92: upper_bound divset(D2,i) >= lower_bound divset(D1,1) by A91,A86,A84 ,SEQ_4:def 2; D2.i <= D2.indx(D2,D1,1) by A43,A34,A53,A73,SEQ_4:137; then upper_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5 ,A91,A90,Def18; then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r & r<= upper_bound divset(D1,1)} by A92; hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by RCOMP_1:def 1; end; end; A93: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1) .] by Th2; A94: Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5; then i in Seg(len D2) by A43,A54; then A95: i in dom D2 by FINSEQ_1:def 3; divset(D2,i)=[.lower_bound divset(D2,i),upper_bound divset(D2,i) .] by Th2; then A96: divset(D2,i) c= divset(D1,1) by A93,A75,XXREAL_2:def 12; A97: dom (upper_volume(f,D2)|Seg indx(D2,D1,1)) =dom upper_volume(f, D2) /\ Seg indx(D2,D1,1) by RELAT_1:61 .=Seg(len upper_volume(f,D2)) /\ Seg indx(D2,D1,1) by FINSEQ_1:def 3 .=Seg(len D2) /\ Seg indx(D2,D1,1) by Def5 .=Seg indx(D2,D1,1) by A94,XBOOLE_1:28; (upper_volume(f,D2)|indx(D2,D1,1)).i =(upper_volume(f,D2)|Seg indx(D2,D1,1)).i by FINSEQ_1:def 15 .=upper_volume(f,D2).i by A43,A54,A97,FUNCT_1:47 .=(upper_bound (rng (f|divset(D2,i))))*vol(divset(D2,i)) by A95,Def5; hence thesis by A72,A96,FUNCT_1:51; end; len upper_volume(g,DD1) = len (upper_volume(f,D1)|1) by A10; then A98: upper_volume(g,DD1) = upper_volume(f,D1)|1 by A18,FINSEQ_1:14; A99: indx(D2,D1,1) <= len upper_volume(f,D2) by A41,Def5; len upper_volume(g,DD2)= indx(D2,D1,1) by A43,Def5; then A100: len upper_volume(g,DD2)=len(upper_volume(f,D2)|indx(D2,D1, 1)) by A99, FINSEQ_1:59; dom g = A /\ divset(D1,1) by A4,FUNCT_2:def 1; then dom g = divset(D1,1) by A5,Th6,XBOOLE_1:28; then g is total by PARTFUN1:def 2; then upper_sum(g,DD1) >= upper_sum(g,DD2) by A11,A28,Th28; hence thesis by A98,A100,A50,FINSEQ_1:14; end; A101: for k being non zero Nat st P[k] holds P[k+1] proof let k be non zero Nat; assume A102: k in dom D1 implies Sum(upper_volume(f,D1)|k) >= Sum( upper_volume(f,D2)|indx(D2,D1,k)); assume A103: k+1 in dom D1; then A104: k+1 in Seg(len D1) by FINSEQ_1:def 3; then A105: 1 <= k+1 by FINSEQ_1:1; A106: k+1 <= len D1 by A104,FINSEQ_1:1; now per cases; suppose 1=k+1; hence thesis by A3,A103; end; suppose A107: 1<>k+1; set IDK =indx(D2,D1,k); set IDK1=indx(D2,D1,k+1); set K1D2=upper_volume(f,D2)|indx(D2,D1,k+1); set KD1 =upper_volume(f,D1)|k; set K1D1=upper_volume(f,D1)|(k+1); set n=k+1; A108: k+1 <= len upper_volume(f,D1) by A106,Def5; then A109: len K1D1=k+1 by FINSEQ_1:59; then consider p1,q1 being FinSequence of REAL such that A110: len p1=k and A111: len q1=1 and A112: K1D1=p1^q1 by FINSEQ_2:23; A113: k <= k+1 by NAT_1:11; then A114: k <= len D1 by A106,XXREAL_0:2; then A115: k <= len upper_volume(f,D1) by Def5; then A116: len p1 = len KD1 by A110,FINSEQ_1:59; for i be Nat st 1 <= i & i <= len p1 holds p1.i=KD1.i proof let i be Nat; assume that A117: 1 <= i and A118: i <= len p1; A119: i in Seg(len p1) by A117,A118,FINSEQ_1:1; then A120: i in dom KD1 by A116,FINSEQ_1:def 3; then A121: i in dom (upper_volume(f,D1)|Seg k) by FINSEQ_1:def 15; k <= k+1 by NAT_1:11; then A122: Seg k c= Seg(k+1) by FINSEQ_1:5; A123: dom K1D1 =Seg(len K1D1) by FINSEQ_1:def 3 .= Seg(k+1) by A108,FINSEQ_1:59; dom KD1=Seg(len KD1) by FINSEQ_1:def 3 .= Seg k by A115,FINSEQ_1:59; then i in dom K1D1 by A120,A122,A123; then A124: i in dom (upper_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 15; A125: K1D1.i = (upper_volume(f,D1)|Seg (k+1)).i by FINSEQ_1:def 15 .= upper_volume(f,D1).i by A124,FUNCT_1:47; A126: KD1.i = (upper_volume(f,D1)|Seg k).i by FINSEQ_1:def 15 .= upper_volume(f,D1).i by A121,FUNCT_1:47; i in dom p1 by A119,FINSEQ_1:def 3; hence thesis by A112,A126,A125,FINSEQ_1:def 7; end; then A127: p1=KD1 by A116,FINSEQ_1:14; A128: indx(D2,D1,k+1) in dom D2 by A1,A103,Def18; then A129: indx(D2,D1,k+1) in Seg(len D2) by FINSEQ_1:def 3; then A130: 1 <= indx(D2,D1,k+1) by FINSEQ_1:1; n is non trivial by A107,NAT_2:def 1; then n >= 2 by NAT_2:29; then k >= (1+1)-1 by XREAL_1:20; then A131: k in Seg(len D1) by A114,FINSEQ_1:1; then A132: k in dom D1 by FINSEQ_1:def 3; then A133: indx(D2,D1,k) in dom D2 by A1,Def18; A134: indx(D2,D1,k) < indx(D2,D1,k+1) proof k < k+1 by NAT_1:13; then A135: D1.k < D1.(k+1) by A103,A132,SEQM_3:def 1; assume indx(D2,D1,k) >= indx(D2,D1,k+1); then A136: D2.indx(D2,D1,k) >= D2.indx(D2,D1,k+1) by A133,A128,SEQ_4:137; D1.k=D2.indx(D2,D1,k) by A1,A132,Def18; hence contradiction by A1,A103,A136,A135,Def18; end; A137: indx(D2,D1,k+1) >= indx(D2,D1,k) proof assume indx(D2,D1,k+1) < indx(D2,D1,k); then A138: D2.indx(D2,D1,k+1) < D2.indx(D2,D1,k) by A133,A128,SEQM_3:def 1; D1.(k+1) = D2.indx(D2,D1,k+1) by A1,A103,Def18; then D1.(k+1) < D1.k by A1,A132,A138,Def18; hence contradiction by A103,A132,NAT_1:11,SEQ_4:137; end; then consider ID being Nat such that A139: indx(D2,D1,k+1) = indx(D2,D1,k) + ID by NAT_1:10; reconsider ID as Element of NAT by ORDINAL1:def 12; A140: len upper_volume(f,D2) = len D2 by Def5; then A141: indx(D2,D1,k+1) <= len upper_volume(f,D2) by A129,FINSEQ_1:1; then len K1D2=IDK + (IDK1-IDK) by FINSEQ_1:59; then consider p2,q2 being FinSequence of REAL such that A142: len p2=IDK and A143: len q2=IDK1-IDK and A144: K1D2=p2^q2 by A139,FINSEQ_2:23; indx(D2,D1,k) in dom D2 by A1,A132,Def18; then A145: indx(D2,D1,k)in Seg(len upper_volume(f,D2)) by A140,FINSEQ_1:def 3; then A146: 1<=indx(D2,D1,k) by FINSEQ_1:1; set KD2 =upper_volume(f,D2)|indx(D2,D1,k); A147: Sum K1D2=Sum p2+Sum q2 by A144,RVSUM_1:75; A148: indx(D2,D1,k)<=len upper_volume(f, D2) by A145,FINSEQ_1:1; then A149: len p2 = len KD2 by A142,FINSEQ_1:59; for i be Nat st 1 <= i & i <= len p2 holds p2.i=KD2.i proof let i be Nat; assume that A150: 1 <= i and A151: i <= len p2; A152: i in Seg(len p2) by A150,A151,FINSEQ_1:1; then A153: i in dom KD2 by A149,FINSEQ_1:def 3; then A154: i in dom (upper_volume(f,D2)|Seg indx(D2,D1,k)) by FINSEQ_1:def 15; A155: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3 .= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59; A156: Seg indx(D2,D1,k) c= Seg indx(D2,D1,k+1) by A137,FINSEQ_1:5; dom KD2 =Seg(len KD2) by FINSEQ_1:def 3 .= Seg indx(D2,D1,k) by A148,FINSEQ_1:59; then i in dom K1D2 by A153,A156,A155; then A157: i in dom (upper_volume(f,D2)|Seg indx(D2,D1,k+ 1)) by FINSEQ_1:def 15; A158: K1D2.i=(upper_volume(f,D2)|Seg indx(D2,D1,k+1)).i by FINSEQ_1:def 15 .=upper_volume(f,D2).i by A157,FUNCT_1:47; A159: KD2.i=(upper_volume(f,D2)|Seg indx(D2,D1,k)).i by FINSEQ_1:def 15 .= upper_volume(f,D2).i by A154,FUNCT_1:47; i in dom p2 by A152,FINSEQ_1:def 3; hence thesis by A144,A159,A158,FINSEQ_1:def 7; end; then A160: p2=KD2 by A149,FINSEQ_1:14; A161: indx(D2,D1,k+1) <= len D2 by A129,FINSEQ_1:1; A162: ID = indx(D2,D1,k+1) - indx(D2,D1,k) by A139; A163: Sum q1 >= Sum q2 proof set MD2 = mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1)); set MD1 = mid(D1,k+1,k+1); set DD1 = divset(D1,k+1); set g = f|DD1; A164: 1 <= indx(D2,D1,k)+1 by NAT_1:11; reconsider g as PartFunc of DD1,REAL by PARTFUN1:10; (k+1)-1=k; then A165: lower_bound DD1=D1.k by A103,A107,Def3; D2.indx(D2,D1,k+1)=D1.(k+1) by A1,A103,Def18; then A166: D2.indx(D2,D1,k+1) = upper_bound DD1 by A103,A107,Def3; A167: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13; then A168: indx(D2,D1,k)+1 <= len D2 by A161,XXREAL_0:2; then indx(D2,D1,k)+1 in Seg(len D2) by A164,FINSEQ_1:1; then A169: indx(D2,D1,k)+1 in dom D2 by FINSEQ_1:def 3; then D2.(indx(D2,D1,k)+1)>=D2.indx(D2,D1,k) by A133,NAT_1:11 ,SEQ_4:137; then D2.(indx(D2,D1,k)+1) >= lower_bound DD1 by A1,A132,A165,Def18; then reconsider MD2 as Division of DD1 by A128,A167,A169,A166,Th35; A170: indx(D2,D1,k+1)-'(indx(D2,D1,k)+1)+1 =indx(D2,D1,k+1)-(indx( D2,D1,k)+1)+1 by A167,XREAL_1:233 .=indx(D2,D1,k+1)-indx(D2,D1,k); A171: for n be Nat st 1 <= n & n <= len q2 holds q2.n=upper_volume (g,MD2).n proof A172: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3 .= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59; then A173: dom K1D2 c= Seg(len D2) by A161,FINSEQ_1:5; then A174: dom K1D2 c= dom D2 by FINSEQ_1:def 3; A175: len mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1)) =ID by A130,A161,A139 ,A167,A168,A164,A170,FINSEQ_6:118; let n be Nat; assume that A176: 1 <= n and A177: n <= len q2; n in Seg(len q2) by A176,A177,FINSEQ_1:1; then A178: n in dom q2 by FINSEQ_1:def 3; then A179: indx(D2,D1,k)+n in dom K1D2 by A142,A144,FINSEQ_1:28; then A180: indx(D2,D1,k)+n in dom (upper_volume(f,D2) |Seg indx(D2,D1 ,k +1)) by FINSEQ_1:def 15; A181: q2.n=K1D2.(indx(D2,D1,k)+n) by A142,A144,A178,FINSEQ_1:def 7 .=(upper_volume(f,D2)|Seg indx(D2,D1,k+1)).(indx(D2,D1,k)+n) by FINSEQ_1:def 15 .=upper_volume(f,D2).(indx(D2,D1,k)+n) by A180,FUNCT_1:47 .=(upper_bound(rng(f|divset(D2,indx(D2,D1,k)+n))))* vol( divset(D2,indx(D2,D1,k)+n)) by A179,A174,Def5; indx(D2,D1,k)+n in Seg len D2 by A179,A173; then A182: indx(D2,D1,k)+n in dom D2 by FINSEQ_1:def 3; indx(D2,D1,k)+n <= indx(D2,D1,k+1) by A172,A179,FINSEQ_1:1; then A183: n <= ID by A162,XREAL_1:19; then n in Seg ID by A176,FINSEQ_1:1; then A184: n in dom MD2 by A175,FINSEQ_1:def 3; n in Seg(len mid(D2,indx(D2,D1,k)+1,indx( D2, D1,k+1))) by A176 ,A183,A175,FINSEQ_1:1; then A185: n in dom mid(D2,indx(D2,D1,k)+1,indx( D2, D1,k+1)) by FINSEQ_1:def 3; A186: 1 <=indx(D2,D1,k)+n by A172,A179,FINSEQ_1:1; A187: divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) & divset(D2,indx( D2,D1,k)+n) c= divset(D1,k+1) proof now per cases; suppose A188: n=1; then A189: indx(D2,D1,k)+1<=len D2 by A179,A173,FINSEQ_1:1; A190: 1<=indx(D2,D1,k)+1 by A172,A179,A188,FINSEQ_1:1; A191: upper_bound divset(MD2,1)= mid(D2,indx(D2,D1,k)+1, indx(D2,D1,k+1)).1 by A184,A188,Def3 .= D2.(1+indx(D2,D1,k)) by A130,A161,A190,A189, FINSEQ_6:118; A192: indx(D2,D1,k)+1 <> 1 by A146,NAT_1:13; A193: (k+1)-1=k; A194: lower_bound divset(MD2,1)=lower_bound divset(D1,k+1) by A184,A188,Def3 .= D1.k by A103,A107,A193,Def3; A195: divset(D2,indx(D2,D1,k)+n)= [.lower_bound divset(D2, indx(D2,D1,k)+1),upper_bound divset(D2, indx(D2,D1,k)+1).] by A188,Th2 .=[.D2.(indx(D2,D1,k)+1-1),upper_bound divset(D2,indx( D2,D1,k)+1).] by A169,A192,Def3 .=[.D2.indx(D2,D1,k),D2.(indx(D2,D1,k)+1).] by A169,A192 ,Def3 .=[.D1.k,D2.(indx(D2,D1,k)+1).] by A1,A132,Def18; hence divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A188,A194,A191 ,Th2; divset(MD2,n)=[.D1.k,D2.(indx( D2,D1,k)+1).] by A188,A194 ,A191,Th2; hence thesis by A184,A195,Th6; end; suppose A196: n<>1; A197: indx(D2,D1,k)+n <> 1 proof assume indx(D2,D1,k)+n = 1; then indx(D2,D1,k)=1-n; then n+1 <= 1 by A146,XREAL_1:19; then n <= 1-1 by XREAL_1:19; hence contradiction by A176,NAT_1:3; end; A198: divset(D2,indx(D2,D1,k)+n) =[.lower_bound divset(D2, indx(D2,D1,k)+n), upper_bound divset(D2,indx(D2,D1,k)+n).] by Th2 .=[.D2.(indx(D2,D1,k)+n-1),upper_bound divset(D2,indx( D2,D1,k)+n).] by A182,A197,Def3 .=[. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2,D1,k)+n) .] by A182,A197,Def3; n<=n+1 by NAT_1:12; then n-1 <= n by XREAL_1:20; then A199: n-1<=len MD2 by A183,A175,XXREAL_0:2; consider n1 being Nat such that A200: n=1+n1 by A176,NAT_1:10; n is non trivial by A176,A196,NAT_2:def 1; then n >= 1+1 by NAT_2:29; then A201: 1<=n-1 by XREAL_1:19; A202: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13; reconsider n1 as Element of NAT by ORDINAL1:def 12; A203: n1+(indx(D2,D1,k)+1)-'1=indx(D2,D1,k)+n-1 by A186,A200, XREAL_1:233; A204: n +(indx(D2,D1,k)+1)-'1=n+indx(D2,D1,k)+1-1 by NAT_1:11 ,XREAL_1:233 .=indx(D2,D1,k)+n; A205: lower_bound divset(MD2,n)=MD2.(n-1) by A184,A196,Def3 .=D2.(indx(D2,D1,k)+n-1) by A130,A161,A168,A164,A202,A200 ,A203,A201,A199,FINSEQ_6:118; A206: upper_bound divset(MD2,n)=MD2.n by A184,A196,Def3 .=D2.(indx(D2,D1,k)+n) by A130,A161,A168,A164,A176,A183, A175,A202,A204,FINSEQ_6:118; hence divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A205,A198 ,Th2; divset(MD2,n)= [. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2 ,D1,k)+n) .] by A205,A206,Th2; hence thesis by A184,A198,Th6; end; end; hence thesis; end; then g|divset(MD2,n) =f|divset(D2,indx(D2,D1,k)+n) by FUNCT_1:51; hence thesis by A185,A181,A187,Def5; end; (k+1)-1=k; then A207: lower_bound DD1=D1.k by A103,A107,Def3; D1.(k+1) = upper_bound DD1 by A103,A107,Def3; then reconsider MD1 as Division of DD1 by A103,A113,A132,A207,Th35, SEQ_4:137; A208: g|divset(D1,k+1) is bounded_above proof consider a be Real such that A209: for x being object st x in A /\ dom f holds f.x <= a by A2, RFUNCT_1:70; for x being object st x in divset(D1,k+1) /\ dom g holds g.x <= a proof let x be object; A210: dom g c= dom f by RELAT_1:60; assume x in divset(D1,k+1) /\ dom g; then A211: x in dom g by XBOOLE_0:def 4; A212: A /\ dom f = dom f by XBOOLE_1:28; then x in A /\ dom f by A211,A210; then reconsider x as Element of A; f.x <= a by A209,A211,A212,A210; hence thesis by A211,FUNCT_1:47; end; hence thesis by RFUNCT_1:70; end; len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118; then A213: len MD1 = ((k+1)-(k+1)) +1 by XREAL_1:233; then A214: dom q1 = dom MD1 by A111,FINSEQ_3:29; A215: for n be Nat st 1 <= n & n <= len q1 holds q1.n=upper_volume (g,MD1).n proof k+1 in Seg(len K1D1) by A109,FINSEQ_1:4; then k+1 in dom K1D1 by FINSEQ_1:def 3; then A216: k+1 in dom (upper_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 15; A217: MD1.1 =D1.(k+1) by A105,A106,FINSEQ_6:118; 1 in Seg(len MD1) by A213,FINSEQ_1:3; then A218: 1 in dom MD1 by FINSEQ_1:def 3; divset(MD1,1)=[.lower_bound divset(MD1,1), upper_bound divset(MD1,1).] by Th2; then A219: divset(MD1,1)=[.lower_bound DD1,upper_bound divset(MD1,1) .] by A218,Def3 .=[.lower_bound DD1,D1.(k+1).] by A218,A217,Def3; (k+1)-1=k; then A220: lower_bound DD1 = D1.k by A103,A107,Def3; let n be Nat; assume that A221: 1 <= n and A222: n <= len q1; A223: n = 1 by A111,A221,A222,XXREAL_0:1; n in Seg(len q1) by A221,A222,FINSEQ_1:1; then A224: n in dom q1 by FINSEQ_1:def 3; upper_bound DD1 = D1.(k+1) by A103,A107,Def3; then divset(D1,k+1)=[. D1.k,D1.(k+1).] by A220,Th2; then A225: upper_volume(g,MD1).n =(upper_bound(rng(g|divset(D1,k+1))) )*vol(divset(D1,k+1)) by A214,A223,A224,A219,A220,Def5; K1D1.(k+1)=(upper_volume(f,D1)|Seg(k+1)).(k+1) by FINSEQ_1:def 15 .=upper_volume(f,D1).(k+1) by A216,FUNCT_1:47; then q1.n = upper_volume(f,D1).(k+1) by A110,A112,A223,A224, FINSEQ_1:def 7 .=(upper_bound(rng(f|divset(D1,k+1))))*vol(divset(D1,k+1)) by A103,Def5; hence thesis by A225; end; len q1 = len(upper_volume(g,MD1)) by A111,A213,Def5; then A226: q1=upper_volume(g,MD1) by A215,FINSEQ_1:14; dom g = dom f /\ divset(D1,k+1) by RELAT_1:61; then dom g = A /\ divset(D1,k+1) by FUNCT_2:def 1; then dom g = divset(D1,k+1) by A103,Th6,XBOOLE_1:28; then A227: g is total by PARTFUN1:def 2; len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118; then len MD1 = (k+1) - (k+1) + 1 by XREAL_1:233; then A228: upper_sum(g,MD1) >= upper_sum(g,MD2) by A208,A227,Th28; len(upper_volume(g,MD2))= len mid(D2,indx(D2,D1,k)+1,indx(D2 ,D1,k+1)) by Def5 .=indx(D2,D1,k+1)-indx(D2,D1,k) by A130,A161,A167,A168,A164,A170, FINSEQ_6:118; hence thesis by A143,A226,A171,A228,FINSEQ_1:14; end; Sum K1D1=Sum p1+Sum q1 by A112,RVSUM_1:75; then Sum q1 = Sum K1D1 - Sum p1; then Sum K1D1 >= Sum q2 + Sum p1 by A163,XREAL_1:19; then Sum K1D1 - Sum q2 >= Sum p1 by XREAL_1:19; then Sum K1D1 - Sum q2 >= Sum p2 by A102,A131,A127,A160, FINSEQ_1:def 3,XXREAL_0:2; hence thesis by A147,XREAL_1:19; end; end; hence thesis; end; thus for k being non zero Nat holds P[k] from NAT_1:sch 10(A3, A101); end; hence thesis; end; theorem Th37: D1 <= D2 & f|A is bounded_below implies for i be non zero Element of NAT holds (i in dom D1 implies Sum(lower_volume(f,D1)|i) <= Sum(lower_volume(f,D2)|indx(D2,D1,i))) proof assume that A1: D1 <= D2 and A2: f|A is bounded_below; for i be non zero Nat holds i in dom D1 implies Sum(lower_volume(f,D1)| i) <= Sum(lower_volume(f,D2)|indx(D2,D1,i)) proof defpred P[Nat] means $1 in dom D1 implies Sum(lower_volume(f,D1)|$1) <= Sum(lower_volume(f,D2)|indx(D2,D1,$1)); A3: P[1] proof set g=f|divset(D1,1); set B=divset(D1,1); set DD2=mid(D2,1,indx(D2,D1,1)); set DD1=mid(D1,1,1); reconsider g as PartFunc of divset(D1,1),REAL by PARTFUN1:10; A4: dom g = dom f /\ divset(D1,1) by RELAT_1:61; assume A5: 1 in dom D1; then A6: D1.1 = upper_bound B by Def3; then A7: D2.indx(D2,D1,1) = upper_bound B by A1,A5,Def18; lower_bound B <= upper_bound B by SEQ_4:11; then reconsider DD1 as Division of B by A5,A6,Th35; 1 in Seg(len D1) by A5,FINSEQ_1:def 3; then A8: 1 <= len D1 by FINSEQ_1:1; then A9: len mid(D1,1,1)=1-'1+1 by FINSEQ_6:118; A10: len lower_volume(g,DD1)=len DD1 by Def6 .= 1 by A9,XREAL_1:235; A11: len mid(D1,1,1)=1 by A9,XREAL_1:235; then A12: len mid(D1,1,1)=len (D1|1); for k be Nat st 1 <= k & k <= len mid(D1,1,1) holds mid(D1,1,1).k=( D1|1).k proof let k be Nat; assume that A13: 1 <= k and A14: k <= len mid(D1,1,1); k in Seg(len(D1|1)) by A12,A13,A14,FINSEQ_1:1; then k in dom (D1|1) by FINSEQ_1:def 3; then k in dom (D1|Seg 1) by FINSEQ_1:def 15; then A15: (D1|Seg 1).k = D1.k by FUNCT_1:47; A16: k = 1 by A11,A13,A14,XXREAL_0:1; then mid(D1,1,1).k = D1.(1+1-1) by A8,FINSEQ_6:118; hence thesis by A16,A15,FINSEQ_1:def 15; end; then A17: mid(D1,1,1)=D1|1 by A12,FINSEQ_1:14; A18: for i be Nat st 1 <= i & i <= len lower_volume(g,DD1) holds lower_volume(g,DD1).i=(lower_volume(f,D1)|1).i proof let i be Nat; assume that A19: 1 <= i and A20: i <= len lower_volume(g,DD1); A21: 1 in Seg 1 by FINSEQ_1:3; dom(D1|Seg 1) = dom D1 /\ Seg 1 by RELAT_1:61; then A22: 1 in dom(D1|Seg 1) by A5,A21,XBOOLE_0:def 4; dom(lower_volume(f,D1))=Seg(len lower_volume(f,D1)) by FINSEQ_1:def 3 .=Seg(len D1) by Def6; then A23: dom(lower_volume(f,D1)|Seg 1) =Seg(len D1) /\ Seg 1 by RELAT_1:61 .=Seg 1 by A8,FINSEQ_1:7; len DD1 = 1 by A9,XREAL_1:235; then A24: 1 in dom DD1 by A21,FINSEQ_1:def 3; A25: (lower_volume(f,D1)|1).i=(lower_volume(f,D1)|Seg 1).i by FINSEQ_1:def 15 .=(lower_volume(f,D1)|Seg 1).1 by A10,A19,A20,XXREAL_0:1 .=lower_volume(f,D1).1 by A23,FINSEQ_1:3,FUNCT_1:47 .=(lower_bound (rng(f|divset(D1,1))))*vol(divset(D1,1)) by A5,Def6; A26: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1) .] by Th2 .=[.lower_bound A,upper_bound divset(D1,1).] by A5,Def3 .=[.lower_bound A,D1.1 .] by A5,Def3; A27: lower_volume(g,DD1).i = lower_volume(g,DD1).1 by A10,A19,A20,XXREAL_0:1 .= (lower_bound (rng (g|divset(DD1,1))))*vol(divset(DD1,1)) by A24 ,Def6; divset(DD1,1)=[.lower_bound divset(DD1,1),upper_bound divset(DD1, 1).] by Th2 .=[.lower_bound B,upper_bound divset(DD1,1).] by A24,Def3 .=[.lower_bound B,DD1.1 .] by A24,Def3 .=[.lower_bound A,(D1|1).1 .] by A5,A17,Def3 .=[.lower_bound A,(D1|Seg 1).1 .] by FINSEQ_1:def 15 .=[.lower_bound A,D1.1 .] by A22,FUNCT_1:47; hence thesis by A27,A26,A25; end; A28: g|divset(D1,1) is bounded_below proof consider a be Real such that A29: for x being object st x in A /\ dom f holds a <= f.x by A2,RFUNCT_1:71; for x being object st x in divset(D1,1) /\ dom g holds a <= g.x proof let x be object; A30: dom g c= dom f by RELAT_1:60; assume x in divset(D1,1) /\ dom g; then A31: x in dom g by XBOOLE_0:def 4; A32: A /\ dom f = dom f by XBOOLE_1:28; then reconsider x as Element of A by A31,A30,XBOOLE_0:def 4; a <= f.x by A29,A31,A32,A30; hence thesis by A31,FUNCT_1:47; end; hence thesis by RFUNCT_1:71; end; A33: rng D2 c= A by Def1; A34: indx(D2,D1,1) in dom D2 by A1,A5,Def18; then A35: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3; then A36: 1 <= indx(D2,D1,1) by FINSEQ_1:1; A37: indx(D2,D1,1) <= len D2 by A35,FINSEQ_1:1; then 1 <= len D2 by A36,XXREAL_0:2; then 1 in Seg(len D2) by FINSEQ_1:1; then A38: 1 in dom D2 by FINSEQ_1:def 3; then D2.1 in rng D2 by FUNCT_1:def 3; then D2.1 in A by A33; then D2.1 in [.lower_bound A,upper_bound A.] by Th2; then D2.1 in {a: lower_bound A <= a & a <= upper_bound A} by RCOMP_1:def 1; then ex a st D2.1=a & lower_bound A <= a & a <= upper_bound A; then D2.1 >= lower_bound B by A5,Def3; then reconsider DD2 as Division of B by A34,A36,A38,A7,Th35; indx(D2,D1,1) in dom D2 by A1,A5,Def18; then A39: indx(D2,D1,1) in Seg(len D2) by FINSEQ_1:def 3; then A40: 1 <= indx(D2,D1,1) by FINSEQ_1:1; A41: indx(D2,D1,1) <= len D2 by A39,FINSEQ_1:1; then A42: 1 <= len D2 by A40,XXREAL_0:2; then len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-'1+1 by A40,A41, FINSEQ_6:118; then A43: len mid(D2,1,indx(D2,D1,1))=indx(D2,D1,1)-1+1 by A40,XREAL_1:233; then A44: len mid(D2,1,indx(D2,D1,1))=len(D2|indx(D2,D1,1)) by A41,FINSEQ_1:59; A45: for k be Nat st 1 <= k & k <= len mid(D2,1,indx(D2,D1,1)) holds mid (D2,1,indx(D2,D1,1)).k=(D2|indx(D2,D1,1)).k proof let k be Nat; assume that A46: 1 <= k and A47: k <= len mid(D2,1,indx(D2,D1,1)); k in Seg len (D2|indx(D2,D1,1)) by A44,A46,A47,FINSEQ_1:1; then k in dom (D2|indx(D2,D1,1)) by FINSEQ_1:def 3; then k in dom (D2|Seg indx(D2,D1,1)) by FINSEQ_1:def 15; then A48: (D2|Seg indx(D2,D1,1)).k=D2.k by FUNCT_1:47; mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-'1) by A40,A41,A42,A46,A47, FINSEQ_6:118; then mid(D2,1,indx(D2,D1,1)).k=D2.(k+1-1) by NAT_1:11,XREAL_1:233; hence thesis by A48,FINSEQ_1:def 15; end; then A49: mid(D2,1,indx(D2,D1,1))=D2|indx(D2,D1,1) by A44,FINSEQ_1:14; A50: for i be Nat st 1 <= i & i <= len lower_volume(g,DD2) holds lower_volume(g,DD2).i = (lower_volume(f,D2)|indx(D2,D1,1)).i proof let i be Nat; assume that A51: 1 <= i and A52: i <= len lower_volume(g,DD2); A53: i <= len DD2 by A52,Def6; then A54: i in Seg(len DD2) by A51,FINSEQ_1:1; then A55: i in dom DD2 by FINSEQ_1:def 3; divset(DD2,i)=divset(D2,i) proof Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5; then i in Seg(len D2) by A43,A54; then A56: i in dom D2 by FINSEQ_1:def 3; now per cases; suppose A57: i=1; then A58: 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A55,FINSEQ_1:def 15; then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61; then A59: 1 in dom D2 by XBOOLE_0:def 4; A60: divset(D2,i)=[.lower_bound divset(D2,1), upper_bound divset(D2,1).] by A57,Th2 .=[.lower_bound A,upper_bound divset(D2,1).] by A59,Def3 .=[.lower_bound A,D2.1 .] by A59,Def3; divset (DD2,i)=[.lower_bound divset(DD2,1), upper_bound divset(DD2,1).] by A57,Th2 .=[.lower_bound B,upper_bound divset(DD2,1).] by A55,A57,Def3 .=[.lower_bound B,DD2.1 .] by A55,A57,Def3 .=[.lower_bound B,(D2|indx(D2,D1,1)).1 .] by A45,A53,A57 .=[.lower_bound B,(D2|Seg indx(D2,D1,1)).1 .] by FINSEQ_1:def 15 .=[.lower_bound B,D2.1 .] by A58,FUNCT_1:47 .=[.lower_bound A,D2.1 .] by A5,Def3; hence thesis by A60; end; suppose A61: i<>1; A62: i-1 in dom(D2|Seg indx(D2,D1,1)) proof i is non trivial by A51,A61,NAT_2:def 1; then A63: i >= 1+1 by NAT_2:29; then A64: 1 <= i-1 by XREAL_1:19; A65: ex j being Nat st i = 1 + j by A51,NAT_1:10; A66: i-1 <= indx(D2,D1,1)-0 by A43,A53,XREAL_1:13; then i-1 <= len D2 by A37,XXREAL_0:2; then i-1 in Seg(len D2) by A65,A64,FINSEQ_1:1; then A67: i-1 in dom D2 by FINSEQ_1:def 3; i-1 >= 1 by A63,XREAL_1:19; then i-1 in Seg indx(D2,D1,1) by A65,A66,FINSEQ_1:1; then i-1 in dom D2 /\ Seg indx(D2,D1,1) by A67,XBOOLE_0:def 4; hence thesis by RELAT_1:61; end; DD2.(i-1)=(D2|indx(D2,D1,1)).(i-1) by A44,A45,FINSEQ_1:14 .=(D2|Seg indx(D2,D1,1)).(i-1) by FINSEQ_1:def 15; then A68: DD2.(i-1)=D2.(i-1) by A62,FUNCT_1:47; i <= len D2 by A43,A37,A53,XXREAL_0:2; then i in Seg(len D2) by A51,FINSEQ_1:1; then i in dom D2 by FINSEQ_1:def 3; then i in dom D2 /\ Seg indx(D2,D1,1) by A43,A54,XBOOLE_0:def 4; then A69: i in dom(D2|Seg indx(D2,D1,1)) by RELAT_1:61; DD2.i=(D2|indx(D2,D1,1)).i by A44,A45,FINSEQ_1:14 .=(D2|Seg indx(D2,D1,1)).i by FINSEQ_1:def 15; then A70: DD2.i=D2.i by A69,FUNCT_1:47; A71: divset(D2,i)=[.lower_bound divset(D2,i), upper_bound divset(D2,i).] by Th2 .=[. D2.(i-1),upper_bound divset(D2,i).] by A56,A61,Def3 .=[. D2.(i-1),D2.i .] by A56,A61,Def3; divset(DD2,i)=[.lower_bound divset(DD2,i), upper_bound divset(DD2,i).] by Th2 .=[. DD2.(i-1),upper_bound divset(DD2,i).] by A55,A61,Def3 .=[. D2.(i-1),D2.i .] by A55,A61,A68,A70,Def3; hence thesis by A71; end; end; hence thesis; end; then A72: lower_volume(g,DD2).i =(lower_bound (rng (g|divset(D2,i))))*vol( divset(D2,i)) by A55,Def6; Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5; then i in Seg(len D2) by A43,A54; then A73: i in dom D2 by FINSEQ_1:def 3; A74: i in dom DD2 by A54,FINSEQ_1:def 3; A75: now per cases; suppose A76: i=1; then 1 in dom (D2|Seg indx(D2,D1,1)) by A49,A74,FINSEQ_1:def 15; then 1 in dom D2 /\ Seg indx(D2,D1,1) by RELAT_1:61; then A77: 1 in dom D2 by XBOOLE_0:def 4; then D2.1 <= D2.indx(D2,D1,1) by A34,A36,SEQ_4:137; then A78: D2.1 <= D1.1 by A1,A5,Def18; lower_bound divset(D2,i)=lower_bound A by A76,A77,Def3; then A79: lower_bound divset(D2,i)=lower_bound divset(D1,1) by A5,Def3; upper_bound divset(D2,i)=D2.1 by A76,A77,Def3; then A80: upper_bound divset(D2,i) <= upper_bound divset(D1,1) by A5,A78,Def3; lower_bound divset(D1,1) <= upper_bound divset(D1,1 ) by SEQ_4:11; hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by A79,XXREAL_1:1; lower_bound divset(D2,i) <= upper_bound divset(D2,i) by SEQ_4:11; then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r & r<= upper_bound divset(D1,1)} by A79,A80; hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by RCOMP_1:def 1; end; suppose A81: i<>1; then i is non trivial by A51,NAT_2:def 1; then i >= 1+1 by NAT_2:29; then A82: 1 <= i-1 by XREAL_1:19; A83: ex j being Nat st i = 1 + j by A51,NAT_1:10; A84: rng D2 c= A by Def1; A85: lower_bound divset(D2,i)=D2.(i-1) by A73,A81,Def3; A86: lower_bound divset(D1,1)=lower_bound A by A5,Def3; A87: i-1 <= indx(D2,D1,1)-0 by A43,A53,XREAL_1:13; then i-1 <= len D2 by A37,XXREAL_0:2; then i-1 in Seg(len D2) by A83,A82,FINSEQ_1:1; then A88: i-1 in dom D2 by FINSEQ_1:def 3; then D2.(i-1) in rng D2 by FUNCT_1:def 3; then A89: lower_bound divset(D2,i) >= lower_bound divset(D1,1) by A85,A86,A84 ,SEQ_4:def 2; A90: upper_bound divset(D1,1)=D1.1 by A5,Def3; D2.(i-1)<= D2.indx(D2,D1,1) by A34,A87,A88,SEQ_4:137; then lower_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5 ,A85,A90,Def18; then lower_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r & r<= upper_bound divset(D1,1)} by A89; hence lower_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by RCOMP_1:def 1; A91: upper_bound divset(D2,i)=D2.i by A73,A81,Def3; D2.i in rng D2 by A73,FUNCT_1:def 3; then A92: upper_bound divset(D2,i) >= lower_bound divset(D1,1) by A91,A86,A84 ,SEQ_4:def 2; D2.i <= D2.indx(D2,D1,1) by A43,A34,A53,A73,SEQ_4:137; then upper_bound divset(D2,i) <= upper_bound divset(D1,1) by A1,A5 ,A91,A90,Def18; then upper_bound divset(D2,i)in{r: lower_bound divset(D1,1)<=r & r<= upper_bound divset(D1,1)} by A92; hence upper_bound divset(D2,i)in [.lower_bound divset(D1,1), upper_bound divset(D1,1).] by RCOMP_1:def 1; end; end; A93: divset(D1,1)=[.lower_bound divset(D1,1),upper_bound divset(D1,1) .] by Th2; A94: Seg indx(D2,D1,1) c= Seg(len D2) by A41,FINSEQ_1:5; then i in Seg(len D2) by A43,A54; then A95: i in dom D2 by FINSEQ_1:def 3; divset(D2,i)=[.lower_bound divset(D2,i),upper_bound divset(D2,i) .] by Th2; then A96: divset(D2,i) c= divset(D1,1) by A93,A75,XXREAL_2:def 12; A97: dom (lower_volume(f,D2)|Seg indx(D2,D1,1)) =dom lower_volume(f, D2) /\ Seg indx(D2,D1,1) by RELAT_1:61 .=Seg(len lower_volume(f,D2)) /\ Seg indx(D2,D1,1) by FINSEQ_1:def 3 .=Seg(len D2) /\ Seg indx(D2,D1,1) by Def6 .=Seg indx(D2,D1,1) by A94,XBOOLE_1:28; (lower_volume(f,D2)|indx(D2,D1,1)).i =(lower_volume(f,D2)|Seg indx(D2,D1,1)).i by FINSEQ_1:def 15 .=lower_volume(f,D2).i by A43,A54,A97,FUNCT_1:47 .=(lower_bound (rng (f|divset(D2,i))))*vol(divset(D2,i)) by A95,Def6; hence thesis by A72,A96,FUNCT_1:51; end; len lower_volume(g,DD1) = len (lower_volume(f,D1)|1) by A10; then A98: lower_volume(g,DD1) = lower_volume(f,D1)|1 by A18,FINSEQ_1:14; A99: indx(D2,D1,1) <= len lower_volume(f,D2) by A41,Def6; len lower_volume(g,DD2)= indx(D2,D1,1) by A43,Def6; then A100: len lower_volume(g,DD2)=len(lower_volume(f,D2)|indx(D2,D1, 1)) by A99, FINSEQ_1:59; dom g = A /\ divset(D1,1) by A4,FUNCT_2:def 1; then dom g = divset(D1,1) by A5,Th6,XBOOLE_1:28; then g is total by PARTFUN1:def 2; then lower_sum(g,DD1) <= lower_sum(g,DD2) by A11,A28,Th29; hence thesis by A98,A100,A50,FINSEQ_1:14; end; A101: for k being non zero Nat st P[k] holds P[k+1] proof let k be non zero Nat; assume A102: k in dom D1 implies Sum(lower_volume(f,D1)|k) <= Sum( lower_volume(f,D2)|indx(D2,D1,k)); assume A103: k+1 in dom D1; then A104: k+1 in Seg(len D1) by FINSEQ_1:def 3; then A105: 1 <= k+1 by FINSEQ_1:1; A106: k+1 <= len D1 by A104,FINSEQ_1:1; now per cases; suppose 1=k+1; hence thesis by A3,A103; end; suppose A107: 1<>k+1; set IDK =indx(D2,D1,k); set IDK1=indx(D2,D1,k+1); set K1D2=lower_volume(f,D2)|indx(D2,D1,k+1); set KD1 =lower_volume(f,D1)|k; set K1D1=lower_volume(f,D1)|(k+1); set n=k+1; A108: k+1 <= len lower_volume(f,D1) by A106,Def6; then A109: len K1D1=k+1 by FINSEQ_1:59; then consider p1,q1 being FinSequence of REAL such that A110: len p1=k and A111: len q1=1 and A112: K1D1=p1^q1 by FINSEQ_2:23; A113: k <= k+1 by NAT_1:11; then A114: k <= len D1 by A106,XXREAL_0:2; then A115: k <= len lower_volume(f,D1) by Def6; then A116: len p1 = len KD1 by A110,FINSEQ_1:59; for i be Nat st 1 <= i & i <= len p1 holds p1.i=KD1.i proof let i be Nat; assume that A117: 1 <= i and A118: i <= len p1; A119: i in Seg(len p1) by A117,A118,FINSEQ_1:1; then A120: i in dom KD1 by A116,FINSEQ_1:def 3; then A121: i in dom (lower_volume(f,D1)|Seg k) by FINSEQ_1:def 15; k <= k+1 by NAT_1:11; then A122: Seg k c= Seg(k+1) by FINSEQ_1:5; A123: dom K1D1 =Seg(len K1D1) by FINSEQ_1:def 3 .= Seg(k+1) by A108,FINSEQ_1:59; dom KD1=Seg(len KD1) by FINSEQ_1:def 3 .= Seg k by A115,FINSEQ_1:59; then i in dom K1D1 by A120,A122,A123; then A124: i in dom (lower_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 15; A125: K1D1.i = (lower_volume(f,D1)|Seg (k+1)).i by FINSEQ_1:def 15 .= lower_volume(f,D1).i by A124,FUNCT_1:47; A126: KD1.i = (lower_volume(f,D1)|Seg k).i by FINSEQ_1:def 15 .= lower_volume(f,D1).i by A121,FUNCT_1:47; i in dom p1 by A119,FINSEQ_1:def 3; hence thesis by A112,A126,A125,FINSEQ_1:def 7; end; then A127: p1=KD1 by A116,FINSEQ_1:14; A128: indx(D2,D1,k+1) in dom D2 by A1,A103,Def18; then A129: indx(D2,D1,k+1) in Seg(len D2) by FINSEQ_1:def 3; then A130: 1 <= indx(D2,D1,k+1) by FINSEQ_1:1; n is non trivial by A107,NAT_2:def 1; then n >= 2 by NAT_2:29; then k >= (1+1)-1 by XREAL_1:20; then A131: k in Seg(len D1) by A114,FINSEQ_1:1; then A132: k in dom D1 by FINSEQ_1:def 3; then A133: indx(D2,D1,k) in dom D2 by A1,Def18; A134: indx(D2,D1,k) < indx(D2,D1,k+1) proof k < k+1 by NAT_1:13; then A135: D1.k < D1.(k+1) by A103,A132,SEQM_3:def 1; assume indx(D2,D1,k) >= indx(D2,D1,k+1); then A136: D2.indx(D2,D1,k) >= D2.indx(D2,D1,k+1) by A133,A128,SEQ_4:137; D1.k=D2.indx(D2,D1,k) by A1,A132,Def18; hence contradiction by A1,A103,A136,A135,Def18; end; A137: indx(D2,D1,k+1) >= indx(D2,D1,k) proof assume indx(D2,D1,k+1) < indx(D2,D1,k); then A138: D2.indx(D2,D1,k+1) < D2.indx(D2,D1,k) by A133,A128,SEQM_3:def 1; D1.(k+1) = D2.indx(D2,D1,k+1) by A1,A103,Def18; then D1.(k+1) < D1.k by A1,A132,A138,Def18; hence contradiction by A103,A132,NAT_1:11,SEQ_4:137; end; then consider ID being Nat such that A139: indx(D2,D1,k+1) = indx(D2,D1,k) + ID by NAT_1:10; reconsider ID as Element of NAT by ORDINAL1:def 12; A140: len lower_volume(f,D2) = len D2 by Def6; then A141: indx(D2,D1,k+1) <= len lower_volume(f,D2) by A129,FINSEQ_1:1; then len K1D2=IDK + (IDK1-IDK) by FINSEQ_1:59; then consider p2,q2 being FinSequence of REAL such that A142: len p2=IDK and A143: len q2=IDK1-IDK and A144: K1D2=p2^q2 by A139,FINSEQ_2:23; A145: indx(D2,D1,k+1) <= len D2 by A129,FINSEQ_1:1; indx(D2,D1,k) in dom D2 by A1,A132,Def18; then A146: indx(D2,D1,k) in Seg(len D2) by FINSEQ_1:def 3; then A147: 1<=indx(D2,D1,k) by FINSEQ_1:1; A148: Sum q1 <= Sum q2 proof set MD2 = mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1)); set MD1 = mid(D1,k+1,k+1); set DD1 = divset(D1,k+1); set g = f|DD1; A149: 1 <= indx(D2,D1,k)+1 by NAT_1:11; reconsider g as PartFunc of DD1,REAL by PARTFUN1:10; (k+1)-1=k; then A150: lower_bound DD1=D1.k by A103,A107,Def3; dom g = dom f /\ divset(D1,k+1) by RELAT_1:61; then dom g = A /\ divset(D1,k+1) by FUNCT_2:def 1; then dom g = divset(D1,k+1) by A103,Th6,XBOOLE_1:28; then A151: g is total by PARTFUN1:def 2; A152: upper_bound divset(D1,k+1)=D1.(k+1) by A103,A107,Def3; A153: D2.indx(D2,D1,k+1)=D1.(k+1) by A1,A103,Def18; A154: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13; then A155: indx(D2,D1,k)+1 <= len D2 by A145,XXREAL_0:2; then indx(D2,D1,k)+1 in Seg(len D2) by A149,FINSEQ_1:1; then A156: indx(D2,D1,k)+1 in dom D2 by FINSEQ_1:def 3; then D2.(indx(D2,D1,k)+1)>=D2.indx(D2,D1,k)by A133,NAT_1:11 ,SEQ_4:137; then D2.(indx(D2,D1,k)+1) >= lower_bound DD1 by A1,A132,A150,Def18; then reconsider MD2 as Division of DD1 by A128,A154,A156,A153,A152,Th35; A157: indx(D2,D1,k+1)-'(indx(D2,D1,k)+1)+1 =indx(D2,D1,k+1)-(indx( D2,D1,k)+1)+1 by A154,XREAL_1:233 .=indx(D2,D1,k+1)-indx(D2,D1,k); A158: for n be Nat st 1 <= n & n <= len q2 holds q2.n=lower_volume (g,MD2).n proof let n be Nat; assume that A159: 1 <= n and A160: n <= len q2; n in Seg(len q2) by A159,A160,FINSEQ_1:1; then A161: n in dom q2 by FINSEQ_1:def 3; then A162: indx(D2,D1,k)+n in dom K1D2 by A142,A144,FINSEQ_1:28; then A163: indx(D2,D1,k)+n in dom (lower_volume(f,D2) |Seg indx(D2,D1 ,k +1)) by FINSEQ_1:def 15; A164: len mid(D2,indx(D2,D1,k)+1,indx(D2,D1,k+1)) =ID by A130,A145,A139 ,A154,A155,A149,A157,FINSEQ_6:118; A165: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3 .= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59; then indx(D2,D1,k)+n <= indx(D2,D1,k+1) by A162,FINSEQ_1:1; then A166: n <= indx(D2,D1,k+1)-indx(D2,D1,k) by XREAL_1:19; then n in Seg(len mid(D2,indx(D2,D1,k)+1,indx( D2,D1,k+1))) by A139,A159,A164,FINSEQ_1:1; then A167: n in dom MD2 by FINSEQ_1:def 3; A168: Seg indx(D2,D1,k+1) c= Seg(len D2) by A145,FINSEQ_1:5; then indx(D2,D1,k)+n in Seg(len D2) by A165,A162; then A169: indx(D2,D1,k)+n in dom D2 by FINSEQ_1:def 3; A170: q2.n=K1D2.(indx(D2,D1,k)+n) by A142,A144,A161,FINSEQ_1:def 7 .=(lower_volume(f,D2)|Seg indx(D2,D1,k+1)).(indx(D2,D1,k)+n) by FINSEQ_1:def 15 .=lower_volume(f,D2).(indx(D2,D1,k)+n) by A163,FUNCT_1:47 .=(lower_bound(rng(f|divset(D2,indx(D2,D1,k)+n))))* vol( divset(D2,indx(D2,D1,k)+n)) by A169,Def6; A171: 1 <=indx(D2,D1,k)+n by A165,A162,FINSEQ_1:1; A172: divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) & divset(D2,indx( D2,D1,k)+n) c= divset(D1,k+1) proof now per cases; suppose A173: n=1; then A174: 1<=indx(D2,D1,k)+1 by A165,A162,FINSEQ_1:1; A175: indx(D2,D1,k)+1<=len D2 by A165,A162,A168,A173,FINSEQ_1:1; A176: upper_bound divset(MD2,1)= mid(D2,indx(D2,D1,k)+1, indx(D2,D1,k+1)).1 by A167,A173,Def3 .= D2.(1+indx(D2,D1,k)) by A130,A145,A174,A175, FINSEQ_6:118; A177: indx(D2,D1,k)+1 <> 1 by A147,NAT_1:13; A178: (k+1)-1=k; A179: lower_bound divset(MD2,1)=lower_bound divset(D1,k+1) by A167,A173,Def3 .= D1.k by A103,A107,A178,Def3; A180: divset(D2,indx(D2,D1,k)+n)= [.lower_bound divset(D2, indx(D2,D1,k)+1), upper_bound divset(D2,indx(D2,D1,k)+1).] by A173,Th2 .=[.D2.(indx(D2,D1,k)+1-1),upper_bound divset(D2,indx( D2,D1,k)+1).] by A156,A177,Def3 .=[.D2.indx(D2,D1,k),D2.(indx(D2,D1,k)+1).] by A156,A177 ,Def3 .=[.D1.k,D2.(indx(D2,D1,k)+1).] by A1,A132,Def18; hence divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A173,A179,A176 ,Th2; divset(MD2,n)=[.D1.k,D2.(indx( D2,D1,k)+1).] by A173,A179 ,A176,Th2; hence thesis by A167,A180,Th6; end; suppose A181: n<>1; A182: indx(D2,D1,k)+n <> 1 proof assume indx(D2,D1,k)+n = 1; then indx(D2,D1,k)=1-n; then n+1 <= 1 by A147,XREAL_1:19; then n <= 1-1 by XREAL_1:19; hence contradiction by A159,NAT_1:3; end; A183: divset(D2,indx(D2,D1,k)+n) =[.lower_bound divset(D2, indx(D2,D1,k)+n), upper_bound divset(D2,indx(D2,D1,k)+n).] by Th2 .=[.D2.(indx(D2,D1,k)+n-1),upper_bound divset(D2,indx( D2,D1,k)+n).] by A169,A182,Def3 .=[. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2,D1,k)+n) .] by A169,A182,Def3; n<=n+1 by NAT_1:12; then n-1 <= n by XREAL_1:20; then A184: n-1<=len MD2 by A139,A166,A164,XXREAL_0:2; A185: indx(D2,D1,k)+1 <= indx(D2,D1,k+1) by A134,NAT_1:13; n is non trivial by A159,A181,NAT_2:def 1; then n >= 1+1 by NAT_2:29; then A186: 1<=n-1 by XREAL_1:19; consider n1 being Nat such that A187: n=1+n1 by A159,NAT_1:10; reconsider n1 as Element of NAT by ORDINAL1:def 12; A188: n1+(indx(D2,D1,k)+1)-'1=indx(D2,D1,k)+n-1 by A171,A187, XREAL_1:233; A189: n+(indx(D2,D1,k)+1)-'1=n+indx(D2,D1,k)+1-1 by NAT_1:11 ,XREAL_1:233 .=indx(D2,D1,k)+n; A190: lower_bound divset(MD2,n)=MD2.(n-1) by A167,A181,Def3 .=D2.(indx(D2,D1,k)+n-1) by A130,A145,A155,A149,A185,A187 ,A188,A186,A184,FINSEQ_6:118; A191: upper_bound divset(MD2,n)=MD2.n by A167,A181,Def3 .=D2.(indx(D2,D1,k)+n) by A130,A145,A139,A155,A149,A159 ,A166,A164,A185,A189,FINSEQ_6:118; hence divset(MD2,n)=divset(D2,indx(D2,D1,k)+n) by A190,A183 ,Th2; divset(MD2,n)= [. D2.(indx(D2,D1,k)+n-1),D2.(indx(D2 ,D1,k)+n) .] by A190,A191,Th2; hence thesis by A167,A183,Th6; end; end; hence thesis; end; then g|divset(MD2,n) =f|divset(D2,indx(D2,D1,k)+n) by FUNCT_1:51; hence thesis by A167,A170,A172,Def6; end; (k+1)-1=k; then A192: lower_bound DD1=D1.k by A103,A107,Def3; D1.(k+1) = upper_bound DD1 by A103,A107,Def3; then reconsider MD1 as Division of DD1 by A103,A113,A132,A192,Th35, SEQ_4:137; A193: g|divset(D1,k+1) is bounded_below proof consider a be Real such that A194: for x being object st x in A /\ dom f holds a <= f.x by A2, RFUNCT_1:71; for x being object st x in divset(D1,k+1) /\ dom g holds a <= g.x proof let x be object; A195: dom g c= dom f by RELAT_1:60; assume x in divset(D1,k+1) /\ dom g; then A196: x in dom g by XBOOLE_0:def 4; A197: A /\ dom f = dom f by XBOOLE_1:28; then reconsider x as Element of A by A196,A195,XBOOLE_0:def 4; a <= f.x by A194,A196,A197,A195; hence thesis by A196,FUNCT_1:47; end; hence thesis by RFUNCT_1:71; end; len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118; then A198: len MD1 = (k+1) - (k+1) + 1 by XREAL_1:233; A199: for n be Nat st 1 <= n & n <= len q1 holds q1.n=lower_volume (g,MD1).n proof k+1 in Seg(len K1D1) by A109,FINSEQ_1:4; then k+1 in dom K1D1 by FINSEQ_1:def 3; then A200: k+1 in dom (lower_volume(f,D1)|Seg(k+1)) by FINSEQ_1:def 15; A201: K1D1.(k+1)=(lower_volume(f,D1)|Seg(k+1)).(k+1) by FINSEQ_1:def 15 .=lower_volume(f,D1).(k+1) by A200,FUNCT_1:47; A202: MD1.1 =D1.(k+1) by A105,A106,FINSEQ_6:118; 1 in Seg 1 by FINSEQ_1:3; then A203: 1 in dom MD1 by A198,FINSEQ_1:def 3; then A204: upper_bound divset( MD1,1) = MD1.1 by Def3; let n be Nat; assume that A205: 1 <= n and A206: n <= len q1; A207: n = 1 by A111,A205,A206,XXREAL_0:1; lower_bound divset(MD1,1) = lower_bound DD1 by A203,Def3; then A208: divset(MD1,1)=[.lower_bound DD1,D1.(k+1).] by A204,A202,Th2; (k+1)-1=k; then A209: lower_bound DD1 = D1.k by A103,A107,Def3; upper_bound DD1 = D1.(k+1) by A103,A107,Def3; then A210: divset(D1,k+1)=[. D1.k,D1.(k+1).] by A209,Th2; A211: n in Seg(len q1) by A205,A206,FINSEQ_1:1; then n in dom MD1 by A111,A198,FINSEQ_1:def 3; then A212: lower_volume(g,MD1).n =(lower_bound(rng(g|divset(D1,k+1))) )*vol(divset(D1,k+1)) by A207,A208,A209,A210,Def6; n in dom q1 by A211,FINSEQ_1:def 3; then q1.n = lower_volume(f,D1).(k+1) by A110,A112,A207,A201, FINSEQ_1:def 7 .=(lower_bound(rng(f|divset(D1,k+1))))*vol(divset(D1,k+1)) by A103,Def6; hence thesis by A212; end; len q1 = len(lower_volume(g,MD1)) by A111,A198,Def6; then A213: q1=lower_volume(g,MD1) by A199,FINSEQ_1:14; len MD1 = (k+1) -'(k+1) + 1 by A105,A106,FINSEQ_6:118; then len MD1 = (k+1) - (k+1) + 1 by XREAL_1:233; then A214: lower_sum(g,MD1) <= lower_sum(g,MD2) by A193,A151,Th29; len(lower_volume(g,MD2))= len mid(D2,indx(D2,D1,k)+1,indx(D2 ,D1,k+1)) by Def6 .=indx(D2,D1,k+1)-indx(D2,D1,k) by A130,A145,A154,A155,A149,A157, FINSEQ_6:118; hence thesis by A143,A213,A158,A214,FINSEQ_1:14; end; set KD2 =lower_volume(f,D2)|indx(D2,D1,k); A215: Sum K1D2=Sum p2+Sum q2 by A144,RVSUM_1:75; A216: indx(D2,D1,k)<=len lower_volume(f, D2) by A140,A146,FINSEQ_1:1; then A217: len p2 = len KD2 by A142,FINSEQ_1:59; for i be Nat st 1 <= i & i <= len p2 holds p2.i=KD2.i proof let i be Nat; assume that A218: 1 <= i and A219: i <= len p2; A220: i in Seg(len p2) by A218,A219,FINSEQ_1:1; then A221: i in dom KD2 by A217,FINSEQ_1:def 3; then A222: i in dom (lower_volume(f,D2)|Seg indx(D2,D1,k)) by FINSEQ_1:def 15; A223: dom K1D2 = Seg(len K1D2) by FINSEQ_1:def 3 .= Seg indx(D2,D1,k+1) by A141,FINSEQ_1:59; A224: Seg indx(D2,D1,k) c= Seg indx(D2,D1,k+1) by A137,FINSEQ_1:5; dom KD2 =Seg(len KD2) by FINSEQ_1:def 3 .= Seg indx(D2,D1,k) by A216,FINSEQ_1:59; then i in dom K1D2 by A221,A224,A223; then A225: i in dom (lower_volume(f,D2)|Seg indx(D2,D1,k+ 1)) by FINSEQ_1:def 15; A226: K1D2.i=(lower_volume(f,D2)|Seg indx(D2,D1,k+1)).i by FINSEQ_1:def 15 .=lower_volume(f,D2).i by A225,FUNCT_1:47; A227: KD2.i=(lower_volume(f,D2)|Seg indx(D2,D1,k)).i by FINSEQ_1:def 15 .= lower_volume(f,D2).i by A222,FUNCT_1:47; i in dom p2 by A220,FINSEQ_1:def 3; hence thesis by A144,A227,A226,FINSEQ_1:def 7; end; then A228: p2=KD2 by A217,FINSEQ_1:14; Sum K1D1=Sum p1+Sum q1 by A112,RVSUM_1:75; then Sum q1 = Sum K1D1 - Sum p1; then Sum K1D1 <= Sum q2 + Sum p1 by A148,XREAL_1:20; then Sum K1D1 - Sum q2 <= Sum p1 by XREAL_1:20; then Sum K1D1 - Sum q2 <= Sum p2 by A102,A131,A127,A228, FINSEQ_1:def 3,XXREAL_0:2; hence thesis by A215,XREAL_1:20; end; end; hence thesis; end; thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A3, A101); end; hence thesis; end; theorem Th38: D1 <= D2 & i in dom D1 & f|A is bounded_above implies (PartSums( upper_volume(f,D1))).i >= (PartSums(upper_volume(f,D2))).indx(D2,D1,i) proof assume that A1: D1 <= D2 and A2: i in dom D1 and A3: f|A is bounded_above; A4: len upper_volume(f,D2)=len D2 by Def5; i in Seg(len D1) by A2,FINSEQ_1:def 3; then i in Seg(len upper_volume(f,D1)) by Def5; then i in dom upper_volume(f,D1) by FINSEQ_1:def 3; then A5: (PartSums(upper_volume(f,D1))).i=Sum(upper_volume(f,D1)|i) by Def19; indx(D2,D1,i) in dom D2 by A1,A2,Def18; then indx(D2,D1,i) in Seg(len upper_volume(f,D2)) by A4,FINSEQ_1:def 3; then A6: indx(D2,D1,i) in dom upper_volume(f,D2) by FINSEQ_1:def 3; i in Seg(len D1) by A2,FINSEQ_1:def 3; then i is non zero Element of NAT by FINSEQ_1:1; then (PartSums(upper_volume(f,D1))).i >= Sum(upper_volume(f,D2)|indx(D2,D1,i )) by A1,A2,A3,A5,Th36; hence thesis by A6,Def19; end; theorem Th39: D1 <= D2 & i in dom D1 & f|A is bounded_below implies (PartSums( lower_volume(f,D1))).i <= (PartSums(lower_volume(f,D2))).indx(D2,D1,i) proof assume that A1: D1 <= D2 and A2: i in dom D1 and A3: f|A is bounded_below; A4: len lower_volume(f,D2)=len D2 by Def6; i in Seg(len D1) by A2,FINSEQ_1:def 3; then i in Seg(len lower_volume(f,D1)) by Def6; then i in dom lower_volume(f,D1) by FINSEQ_1:def 3; then A5: (PartSums(lower_volume(f,D1))).i=Sum(lower_volume(f,D1)|i) by Def19; indx(D2,D1,i) in dom D2 by A1,A2,Def18; then indx(D2,D1,i) in Seg(len lower_volume(f,D2)) by A4,FINSEQ_1:def 3; then A6: indx(D2,D1,i) in dom lower_volume(f,D2) by FINSEQ_1:def 3; i in Seg(len D1) by A2,FINSEQ_1:def 3; then i is non zero Element of NAT by FINSEQ_1:1; then (PartSums(lower_volume(f,D1))).i <= Sum(lower_volume(f,D2)|indx(D2,D1,i )) by A1,A2,A3,A5,Th37; hence thesis by A6,Def19; end; theorem Th40: (PartSums(upper_volume(f,D))).(len D) = upper_sum(f,D) proof len upper_volume(f,D) = len D by Def5; then len D in Seg(len upper_volume(f,D)) by FINSEQ_1:3; then len D in dom upper_volume(f,D) by FINSEQ_1:def 3; then A1: (PartSums(upper_volume(f,D))).(len D) = Sum(upper_volume(f,D)|(len D )) by Def19; dom upper_volume(f,D)=Seg len upper_volume(f,D) by FINSEQ_1:def 3; then dom upper_volume(f,D)=Seg len D by Def5; then upper_volume(f,D)|(Seg len D) = upper_volume(f,D); hence thesis by A1,FINSEQ_1:def 15; end; theorem Th41: (PartSums(lower_volume(f,D))).(len D) = lower_sum(f,D) proof len lower_volume(f,D) = len D by Def6; then len D in Seg(len lower_volume(f,D)) by FINSEQ_1:3; then len D in dom lower_volume(f,D) by FINSEQ_1:def 3; then A1: (PartSums(lower_volume(f,D))).(len D) = Sum(lower_volume(f,D)|(len D )) by Def19; dom lower_volume(f,D)=Seg len lower_volume(f,D) by FINSEQ_1:def 3; then dom lower_volume(f,D)=Seg len D by Def6; then lower_volume(f,D)|(Seg len D) = lower_volume(f,D); hence thesis by A1,FINSEQ_1:def 15; end; theorem Th42: D1 <= D2 implies indx(D2,D1,len D1) = len D2 proof len D1 in Seg(len D1) by FINSEQ_1:3; then A1: len D1 in dom D1 by FINSEQ_1:def 3; assume A2: D1 <= D2; then D1.(len D1)=D2.indx(D2,D1,len D1) by A1,Def18; then A3: D2.indx(D2,D1,len D1)=upper_bound A by Def1; len D2 in Seg(len D2) by FINSEQ_1:3; then A4: len D2 in dom D2 by FINSEQ_1:def 3; assume A5: indx(D2,D1,len D1) <> len D2; A6: indx(D2,D1,len D1) in dom D2 by A2,A1,Def18; then indx(D2,D1,len D1) in Seg(len D2) by FINSEQ_1:def 3; then indx(D2,D1,len D1) <= len D2 by FINSEQ_1:1; then indx(D2,D1,len D1) < len D2 by A5,XXREAL_0:1; then D2.indx(D2,D1,len D1) < D2.(len D2) by A4,A6,SEQM_3:def 1; hence contradiction by A3,Def1; end; theorem Th43: D1 <= D2 & f|A is bounded_above implies upper_sum(f,D2) <= upper_sum(f,D1) proof assume that A1: D1 <= D2 and A2: f|A is bounded_above; len D1 in Seg(len D1) by FINSEQ_1:3; then len D1 in dom D1 by FINSEQ_1:def 3; then (PartSums(upper_volume(f,D1))).(len D1) >= (PartSums(upper_volume(f,D2)) ).indx(D2,D1,len D1) by A1,A2,Th38; then upper_sum(f,D1) >= (PartSums(upper_volume(f,D2))).indx(D2,D1,len D1) by Th40; then upper_sum(f,D1) >= (PartSums(upper_volume(f,D2))).(len D2) by A1,Th42; hence thesis by Th40; end; theorem Th44: D1 <= D2 & f|A is bounded_below implies lower_sum(f,D2) >= lower_sum(f,D1) proof assume that A1: D1 <= D2 and A2: f|A is bounded_below; len D1 in Seg(len D1) by FINSEQ_1:3; then len D1 in dom D1 by FINSEQ_1:def 3; then (PartSums(lower_volume(f,D1))).(len D1) <= (PartSums(lower_volume(f,D2)) ).indx(D2,D1,len D1) by A1,A2,Th39; then lower_sum(f,D1) <= (PartSums(lower_volume(f,D2))).indx(D2,D1,len D1) by Th41; then lower_sum(f,D1) <= (PartSums(lower_volume(f,D2))).(len D2) by A1,Th42; hence thesis by Th41; end; theorem Th45: ex D be Division of A st D1 <= D & D2 <= D proof consider D3 being FinSequence of REAL such that A1: rng D3 = rng(D1^D2) and A2: len D3 = card rng(D1^D2) and A3: D3 is increasing by SEQ_4:140; reconsider D3 as non empty increasing FinSequence of REAL by A1,A3; A4: rng D2 c= A by Def1; rng D1 c= A by Def1; then rng D1 \/ rng D2 c= A by A4,XBOOLE_1:8; then A5: rng D3 c= A by A1,FINSEQ_1:31; D3.(len D3) = upper_bound A proof assume A6: D3.(len D3) <> upper_bound A; now per cases by A6,XXREAL_0:1; suppose A7: D3.(len D3) > upper_bound A; len D3 in Seg(len D3) by FINSEQ_1:3; then len D3 in dom D3 by FINSEQ_1:def 3; then D3.(len D3) in rng D3 by FUNCT_1:def 3; then D3.(len D3) in A by A5; then D3.(len D3) in [.lower_bound A,upper_bound A.] by Th2; then D3.(len D3) in {r:lower_bound A <= r & r <= upper_bound A} by RCOMP_1:def 1; then ex a st a=D3.(len D3) & lower_bound A <= a & a <= upper_bound A; hence contradiction by A7; end; suppose A8: D3.(len D3) < upper_bound A; A9: rng D1 c= rng (D1^D2) by FINSEQ_1:29; len D1 in Seg(len D1) by FINSEQ_1:3; then A10: len D1 in dom D1 by FINSEQ_1:def 3; len D3 in Seg(len D3) by FINSEQ_1:3; then A11: len D3 in dom D3 by FINSEQ_1:def 3; D1.(len D1) = upper_bound A by Def1; then upper_bound A in rng D1 by A10,FUNCT_1:def 3; then consider k being Nat such that A12: k in dom D3 and A13: D3.k = upper_bound A by A1,A9,FINSEQ_2:10; k in Seg(len D3) by A12,FINSEQ_1:def 3; then k <= len D3 by FINSEQ_1:1; hence contradiction by A8,A11,A12,A13,SEQ_4:137; end; end; hence thesis; end; then reconsider D3 as Division of A by A5,Def1; len D2 = card(rng D2) by FINSEQ_4:62; then A14: len D2 <= len D3 by A2,FINSEQ_1:30,NAT_1:43; take D3; A15: rng D1 c= rng (D1^D2) by FINSEQ_1:29; A16: rng D2 c= rng (D1^D2) by FINSEQ_1:30; len D1 = card(rng D1) by FINSEQ_4:62; then len D1 <= len D3 by A2,FINSEQ_1:29,NAT_1:43; hence thesis by A1,A15,A16,A14; end; theorem Th46: f|A is bounded implies lower_sum(f,D1) <= upper_sum(f,D2) proof consider D such that A1: D1 <= D and A2: D2 <= D by Th45; assume A3: f|A is bounded; then A4: lower_sum(f,D) <= upper_sum(f,D) by Th26; upper_sum(f,D) <= upper_sum(f,D2) by A3,A2,Th43; then A5: lower_sum(f,D) <= upper_sum(f,D2) by A4,XXREAL_0:2; lower_sum(f,D1) <= lower_sum(f,D) by A3,A1,Th44; hence thesis by A5,XXREAL_0:2; end; begin :: Additivity of integral theorem Th47: f|A is bounded implies upper_integral(f) >= lower_integral(f) proof assume A1: f|A is bounded; A2: for b be Real st b in rng upper_sum_set(f) holds lower_integral(f ) <= b proof let b be Real; assume b in rng upper_sum_set(f); then consider D1 being Element of divs A such that D1 in dom upper_sum_set(f) and A3: b=(upper_sum_set(f)).D1 by PARTFUN1:3; reconsider D1 as Division of A by Def2; A4: for a being Real st a in rng lower_sum_set(f) holds a <= upper_sum(f,D1) proof let a be Real; assume a in rng lower_sum_set(f); then consider D2 being Element of divs A such that D2 in dom lower_sum_set(f) and A5: a=(lower_sum_set(f)).D2 by PARTFUN1:3; reconsider D2 as Division of A by Def2; a=lower_sum(f,D2) by A5,Def10; hence thesis by A1,Th46; end; b=upper_sum(f,D1) by A3,Def9; hence thesis by A4,SEQ_4:45; end; thus thesis by A2,SEQ_4:43; end; theorem Th48: for X,Y be Subset of REAL holds (--X)++(--Y)=--(X++Y) proof let X,Y be Subset of REAL; for z be object st z in --(X++Y) holds z in (--X)++(--Y) proof let z be object; assume A1: z in --(X++Y); reconsider XY = X++Y as Subset of REAL by MEMBERED:3; z in -- XY by A1; then consider x be Real such that A2: x in XY and A3: z=-x by MEASURE6:72; consider a,b be Real such that A4: a in X and A5: b in Y and A6: x=a+b by A2,MEASURE6:21; A7: -a in --X by A4,MEMBER_1:11; A8: -b in --Y by A5,MEMBER_1:11; z = -a+-b by A3,A6; hence thesis by A7,A8,MEMBER_1:46; end; then A9: --(X++Y) c= (--X)++(--Y); for z be object st z in (--X)++(--Y) holds z in --(X++Y) proof let z be object; assume A10: z in --(X)++(--Y); consider x,y being Real such that A11: x in --X and A12: y in --Y and A13: z=x+y by A10,MEASURE6:21; consider b be Real such that A14: b in Y and A15: y=-b by A12,MEASURE6:72; reconsider X as Subset of REAL; consider a be Real such that A16: a in X and A17: x=-a by A11,MEASURE6:72; A18: a+b in X++Y by A16,A14,MEMBER_1:46; z=-(a+b) by A13,A17,A15; hence thesis by A18,MEMBER_1:11; end; then (--X)++(--Y) c= --(X++Y); hence thesis by A9; end; theorem Th49: for X,Y being Subset of REAL st X is bounded_above & Y is bounded_above holds X++Y is bounded_above proof let X,Y be Subset of REAL; assume that A1: X is bounded_above and A2: Y is bounded_above; A3: (--Y) is bounded_below by A2,MEASURE6:41; (--X) is bounded_below by A1,MEASURE6:41; then A4: (--X)++(--Y) is bounded_below by A3,SEQ_4:124; reconsider XY = X++Y as Subset of REAL by MEMBERED:3; --XY is bounded_below by Th48,A4; hence thesis by MEASURE6:41; end; theorem Th50: for X,Y be non empty Subset of REAL st X is bounded_above & Y is bounded_above holds upper_bound(X++Y) = upper_bound X + upper_bound Y proof let X,Y be non empty Subset of REAL; assume that A1: X is bounded_above and A2: Y is bounded_above; A3: (--Y) is bounded_below by A2,MEASURE6:41; A4: (--X) is bounded_below by A1,MEASURE6:41; then lower_bound(--X++--Y) = lower_bound(--X)+lower_bound(--Y) by A3,SEQ_4:125; then A5: lower_bound(--X++--Y) = -upper_bound(----X)+lower_bound(--Y) by A4,MEASURE6:43 .= -upper_bound X + -upper_bound(----Y) by A3,MEASURE6:43 .= -(upper_bound X + upper_bound Y); A6: (--X)++(--Y)=--(X++Y) by Th48; then A7: --(X++Y) is bounded_below by A4,A3,SEQ_4:124; reconsider XY = X++Y as Subset of REAL by MEMBERED:3; - upper_bound(-- --XY)= - (upper_bound X + upper_bound Y) by A6,A5,A7,MEASURE6:43; then upper_bound XY = upper_bound X + upper_bound Y; hence thesis; end; theorem Th51: i in dom D & f|A is bounded_above & g|A is bounded_above implies upper_volume(f+g,D).i <= upper_volume(f,D).i + upper_volume(g,D).i proof assume A1: i in dom D; dom(f+g) = A /\ A by FUNCT_2:def 1; then dom((f+g)|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62; then A2: rng((f+g)|divset(D,i)) is non empty by RELAT_1:42; (f+g)|divset(D,i)=f|divset(D,i) + g|divset(D,i) by RFUNCT_1:44; then A3: rng((f+g)|divset(D,i))c=rng(f|divset(D,i))++rng(g|divset(D,i)) by Th8; assume f|A is bounded_above; then rng f is bounded_above by Th11; then A4: rng(f|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43; dom g = A by FUNCT_2:def 1; then dom (g|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62; then A5: rng(g|divset(D,i)) is non empty by RELAT_1:42; A6: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48; assume g|A is bounded_above; then rng g is bounded_above by Th11; then A7: rng(g|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43; then A8: rng(f|divset(D,i))++rng(g|divset(D,i)) is bounded_above by A4,Th49; dom f = A by FUNCT_2:def 1; then dom (f|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62; then rng(f|divset(D,i)) is non empty by RELAT_1:42; then upper_bound(rng(f|divset(D,i))++rng(g|divset(D,i))) = upper_bound rng(f|divset(D,i)) + upper_bound rng(g|divset(D,i)) by A4,A7,A5,Th50; then upper_bound rng((f+g)|divset(D,i))*vol(divset(D,i)) <= (upper_bound rng (f|divset(D,i)) + upper_bound rng(g|divset(D,i)))*vol(divset(D,i)) by A8,A2 ,A6,A3,SEQ_4:48,XREAL_1:64; then upper_volume(f+g,D).i <= upper_bound rng(f|divset(D,i))*vol(divset(D,i) )+ upper_bound rng(g|divset(D,i))*vol(divset(D,i)) by A1,Def5; then upper_volume(f+g,D).i <= upper_volume(f,D).i+ upper_bound rng(g|divset( D,i))*vol(divset(D,i)) by A1,Def5; hence thesis by A1,Def5; end; theorem Th52: i in dom D & f|A is bounded_below & g|A is bounded_below implies lower_volume(f,D).i + lower_volume(g,D).i <= lower_volume(f+g,D).i proof assume that A1: i in dom D and A2: f|A is bounded_below and A3: g|A is bounded_below; A4: 0 <= vol(divset(D,i)) by SEQ_4:11,XREAL_1:48; dom(f+g) = A /\ A by FUNCT_2:def 1; then dom((f+g)|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62; then A5: rng((f+g)|divset(D,i)) is non empty by RELAT_1:42; rng g is bounded_below by A3,Th9; then A6: rng(g|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44; dom g = A by FUNCT_2:def 1; then dom (g|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62; then A7: rng(g|divset(D,i)) is non empty by RELAT_1:42; (f+g)|divset(D,i)=f|divset(D,i) + g|divset(D,i) by RFUNCT_1:44; then A8: rng((f+g)|divset(D,i))c=rng(f|divset(D,i))++rng(g|divset(D,i)) by Th8; rng f is bounded_below by A2,Th9; then A9: rng(f|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44; then A10: rng (f|divset(D,i))++rng(g|divset(D,i)) is bounded_below by A6,SEQ_4:124; dom f = A by FUNCT_2:def 1; then dom (f|divset(D,i)) = divset(D,i) by A1,Th6,RELAT_1:62; then rng(f|divset(D,i)) is non empty by RELAT_1:42; then lower_bound(rng(f|divset(D,i))++rng(g|divset(D,i))) = lower_bound rng(f|divset(D,i)) + lower_bound rng(g|divset(D,i)) by A9,A6,A7,SEQ_4:125; then lower_bound rng((f+g)|divset(D,i))*vol(divset(D,i)) >= (lower_bound rng (f|divset(D,i)) + lower_bound rng(g|divset(D,i)))*vol(divset(D,i)) by A10,A5 ,A4,A8,SEQ_4:47,XREAL_1:64; then lower_volume(f+g,D).i >= lower_bound rng(f|divset(D,i))*vol(divset(D,i) )+ lower_bound rng(g|divset(D,i))*vol(divset(D,i)) by A1,Def6; then lower_volume(f+g,D).i >= lower_volume(f,D).i+ lower_bound rng(g|divset( D,i))*vol(divset(D,i)) by A1,Def6; hence thesis by A1,Def6; end; theorem Th53: f|A is bounded_above & g|A is bounded_above implies upper_sum(f+ g,D) <= upper_sum(f,D) + upper_sum(g,D) proof assume that A1: f|A is bounded_above and A2: g|A is bounded_above; set H=upper_volume(f+g,D); set G=upper_volume(g,D); set F=upper_volume(f,D); len G = len D by Def5; then A3: G is Element of (len D)-tuples_on REAL by FINSEQ_2:92; len F = len D by Def5; then A4: F is Element of (len D)-tuples_on REAL by FINSEQ_2:92; A5: for j be Nat st j in Seg(len D) holds H.j <= (F+G).j proof let j be Nat; assume j in Seg(len D); then j in dom D by FINSEQ_1:def 3; then upper_volume(f+g,D).j <= upper_volume(f,D).j + upper_volume(g,D).j by A1,A2 ,Th51; hence thesis by A4,A3,RVSUM_1:11; end; len H = len D by Def5; then A6: H is Element of (len D)-tuples_on REAL by FINSEQ_2:92; F+G is Element of (len D)-tuples_on REAL by A4,A3,FINSEQ_2:120; then Sum H <= Sum(F+G) by A6,A5,RVSUM_1:82; hence thesis by A4,A3,RVSUM_1:89; end; theorem Th54: f|A is bounded_below & g|A is bounded_below implies lower_sum(f, D) + lower_sum(g,D) <= lower_sum(f+g,D) proof assume that A1: f|A is bounded_below and A2: g|A is bounded_below; set H=lower_volume(f+g,D); set G=lower_volume(g,D); set F=lower_volume(f,D); len G = len D by Def6; then A3: G is Element of (len D)-tuples_on REAL by FINSEQ_2:92; len F = len D by Def6; then A4: F is Element of (len D)-tuples_on REAL by FINSEQ_2:92; A5: for j be Nat st j in Seg(len D) holds (F+G).j <= H.j proof let j be Nat; assume j in Seg(len D); then j in dom D by FINSEQ_1:def 3; then lower_volume(f,D).j + lower_volume(g,D).j <= lower_volume(f+g,D).j by A1,A2 ,Th52; hence thesis by A4,A3,RVSUM_1:11; end; len H = len D by Def6; then A6: H is Element of (len D)-tuples_on REAL by FINSEQ_2:92; F+G is Element of (len D)-tuples_on REAL by A4,A3,FINSEQ_2:120; then Sum(F+G) <= Sum H by A6,A5,RVSUM_1:82; hence thesis by A4,A3,RVSUM_1:89; end; theorem f|A is bounded & g|A is bounded & f is integrable & g is integrable implies f+g is integrable & integral(f+g)=integral(f)+integral(g) proof assume that A1: f|A is bounded and A2: g|A is bounded and A3: f is integrable and A4: g is integrable; A5: lower_integral(f)+lower_integral(g) =upper_integral(f) + lower_integral(g) by A3 .=integral(f) + integral(g) by A4; A6: (f+g)|(A /\ A) is bounded by A1,A2,RFUNCT_1:83; for D be object st D in divs A /\ dom(lower_sum_set(f+g)) holds ( lower_sum_set(f+g)).D <= (upper_bound rng f)*vol(A) + (upper_bound rng g)*vol(A ) proof let D be object; assume D in divs A /\ dom(lower_sum_set(f+g)); then reconsider D as Division of A by Def2; (lower_sum_set(f+g)).D = lower_sum((f+g),D) by Def10; then A7: (lower_sum_set(f+g)).D <= upper_sum((f+g),D) by A6,Th26; upper_sum(f,D) <= (upper_bound rng f)*vol(A) by A1,Th25; then A8: upper_sum(f,D)+upper_sum(g,D) <= (upper_bound rng f)*vol(A)+upper_sum (g,D ) by XREAL_1:6; upper_sum(g,D) <= (upper_bound rng g)*vol(A) by A2,Th25; then A9: (upper_bound rng f)*vol(A)+upper_sum(g,D)<= (upper_bound rng f)*vol(A )+( upper_bound rng g)*vol(A) by XREAL_1:6; upper_sum((f+g),D) <= upper_sum(f,D)+upper_sum(g,D) by A1,A2,Th53; then (lower_sum_set(f+g)).D <= upper_sum(f,D)+upper_sum(g,D) by A7, XXREAL_0:2; then (lower_sum_set(f+g)).D <= (upper_bound rng f)*vol(A)+upper_sum(g,D ) by A8,XXREAL_0:2; hence thesis by A9,XXREAL_0:2; end; then (lower_sum_set(f+g))|divs A is bounded_above by RFUNCT_1:70; then A10: rng lower_sum_set(f+g) is bounded_above by Th11; then A11: f+g is lower_integrable; for D be object st D in divs A /\ dom(upper_sum_set(f+g)) holds ( lower_bound rng f)*vol(A) + (lower_bound rng g)*vol(A) <= (upper_sum_set(f+g)). D proof let D be object; assume D in divs A /\ dom(upper_sum_set(f+g)); then reconsider D as Division of A by Def2; (upper_sum_set(f+g)).D = upper_sum((f+g),D) by Def9; then A12: lower_sum((f+g),D) <= (upper_sum_set(f+g)).D by A6,Th26; (lower_bound rng f)*vol(A) <= lower_sum(f,D) by A1,Th23; then A13: (lower_bound rng f)*vol(A)+lower_sum(g,D) <= lower_sum(f,D)+lower_sum (g,D) by XREAL_1:6; (lower_bound rng g)*vol(A) <= lower_sum(g,D) by A2,Th23; then A14: (lower_bound rng f)*vol(A)+(lower_bound rng g)*vol(A)<= (lower_bound rng f )*vol(A)+lower_sum(g,D) by XREAL_1:6; lower_sum(f,D)+lower_sum(g,D) <= lower_sum((f+g),D) by A1,A2,Th54; then lower_sum(f,D)+lower_sum(g,D) <= (upper_sum_set(f+g)).D by A12, XXREAL_0:2; then (lower_bound rng f)*vol(A)+lower_sum(g,D) <= (upper_sum_set(f+g)).D by A13,XXREAL_0:2; hence thesis by A14,XXREAL_0:2; end; then (upper_sum_set(f+g))|divs A is bounded_below by RFUNCT_1:71; then A15: rng upper_sum_set(f+g) is bounded_below by Th9; A16: for D st D in divs A /\ dom upper_sum_set(f+g) holds (upper_sum_set f). D + (upper_sum_set g).D >= upper_integral(f+g) proof let D; upper_sum(f,D)+upper_sum(g,D) >= upper_sum((f+g),D) by A1,A2,Th53; then A17: (upper_sum_set f).D+upper_sum(g,D) >= upper_sum((f+g),D) by Def9; assume D in divs A /\ dom upper_sum_set(f+g); then D in dom(upper_sum_set(f+g)) by XBOOLE_0:def 4; then (upper_sum_set(f+g)).D in rng upper_sum_set(f+g) by FUNCT_1:def 3; then A18: (upper_sum_set(f+g)).D >= upper_integral(f+g) by A15,SEQ_4:def 2; (upper_sum_set f).D+(upper_sum_set g).D >= upper_sum((f+g),D) by A17,Def9; then (upper_sum_set f).D+(upper_sum_set g).D>=(upper_sum_set(f+g)).D by Def9; hence thesis by A18,XXREAL_0:2; end; A19: dom upper_sum_set(f+g) = divs A by FUNCT_2:def 1; A20: for a1 be Real st a1 in rng upper_sum_set(f) holds a1 >= upper_integral(f+g) - upper_integral(g) proof let a1 be Real; assume a1 in rng upper_sum_set(f); then consider D1 be Element of divs A such that D1 in dom upper_sum_set(f) and A21: a1=(upper_sum_set(f)).D1 by PARTFUN1:3; reconsider D1 as Division of A by Def2; A22: a1=upper_sum(f,D1) by A21,Def9; for a2 being Real st a2 in rng upper_sum_set(g) holds a2 >= upper_integral(f+g) - a1 proof let a2 be Real; assume a2 in rng upper_sum_set(g); then consider D2 be Element of divs A such that D2 in dom upper_sum_set(g) and A23: a2=(upper_sum_set(g)).D2 by PARTFUN1:3; reconsider D2 as Division of A by Def2; consider D such that A24: D1 <= D and A25: D2 <= D by Th45; A26: D in divs A by Def2; (upper_sum_set(g)).D = upper_sum(g,D) by Def9; then A27: (upper_sum_set(g)).D <= upper_sum(g,D2) by A2,A25,Th43; (upper_sum_set(f)).D = upper_sum(f,D) by Def9; then (upper_sum_set(f)).D <= upper_sum(f,D1) by A1,A24,Th43; then A28: (upper_sum_set f).D + (upper_sum_set g).D <= upper_sum(f,D1) + upper_sum(g,D2) by A27,XREAL_1:7; (upper_sum_set f).D + (upper_sum_set g).D >= upper_integral(f+g) by A19 ,A16,A26; then A29: upper_sum(f,D1)+upper_sum(g,D2) >= upper_integral(f+g) by A28,XXREAL_0:2; a2=upper_sum(g,D2) by A23,Def9; hence thesis by A22,A29,XREAL_1:20; end; then lower_bound rng upper_sum_set(g) >= upper_integral(f+g) - a1 by SEQ_4:43; then a1+lower_bound rng upper_sum_set(g) >= upper_integral(f+g) by XREAL_1:20; hence thesis by XREAL_1:20; end; upper_integral(f) >= upper_integral(f+g) - upper_integral(g) by A20,SEQ_4:43; then A30: integral(f)+upper_integral(g)>=upper_integral(f+g) by XREAL_1:20; A31: for D st D in divs A /\ dom lower_sum_set(f+g) holds (lower_sum_set f). D + (lower_sum_set g).D <= lower_integral(f+g) proof let D; lower_sum(f,D)+lower_sum(g,D) <= lower_sum((f+g),D) by A1,A2,Th54; then A32: (lower_sum_set f).D+lower_sum(g,D) <= lower_sum((f+g),D) by Def10; assume D in divs A /\ dom lower_sum_set(f+g); then D in dom(lower_sum_set(f+g)) by XBOOLE_0:def 4; then (lower_sum_set(f+g)).D in rng lower_sum_set(f+g) by FUNCT_1:def 3; then A33: (lower_sum_set(f+g)).D <= lower_integral(f+g) by A10,SEQ_4:def 1; (lower_sum_set f).D+(lower_sum_set g).D <= lower_sum((f+g),D) by A32,Def10; then (lower_sum_set f).D+(lower_sum_set g).D<=(lower_sum_set(f+g)).D by Def10; hence thesis by A33,XXREAL_0:2; end; A34: dom lower_sum_set(f+g) = divs A by FUNCT_2:def 1; A35: for a1 be Real st a1 in rng lower_sum_set(f) holds a1 <= lower_integral(f+g) - lower_integral(g) proof let a1 be Real; assume a1 in rng lower_sum_set(f); then consider D1 be Element of divs A such that D1 in dom lower_sum_set(f) and A36: a1=(lower_sum_set(f)).D1 by PARTFUN1:3; reconsider D1 as Division of A by Def2; A37: a1=lower_sum(f,D1) by A36,Def10; for a2 be Real st a2 in rng lower_sum_set(g) holds a2 <= lower_integral(f+g) - a1 proof let a2 be Real; assume a2 in rng lower_sum_set(g); then consider D2 be Element of divs A such that D2 in dom lower_sum_set(g) and A38: a2=(lower_sum_set(g)).D2 by PARTFUN1:3; reconsider D2 as Division of A by Def2; consider D such that A39: D1 <= D and A40: D2 <= D by Th45; A41: D in divs A by Def2; (lower_sum_set(g)).D = lower_sum(g,D) by Def10; then A42: (lower_sum_set(g)).D >= lower_sum(g,D2) by A2,A40,Th44; (lower_sum_set(f)).D = lower_sum(f,D) by Def10; then (lower_sum_set(f)).D >= lower_sum(f,D1) by A1,A39,Th44; then A43: (lower_sum_set f).D + (lower_sum_set g).D >= lower_sum(f,D1) + lower_sum(g,D2) by A42,XREAL_1:7; (lower_sum_set f).D + (lower_sum_set g).D <= lower_integral(f+g) by A34,A31,A41; then A44: lower_sum(f,D1)+lower_sum(g,D2) <= lower_integral(f+g) by A43,XXREAL_0:2; a2=lower_sum(g,D2) by A38,Def10; hence thesis by A37,A44,XREAL_1:19; end; then upper_bound rng lower_sum_set(g)<= lower_integral(f+g) - a1 by SEQ_4:45; then a1+upper_bound rng lower_sum_set(g) <= lower_integral(f+g) by XREAL_1:19; hence thesis by XREAL_1:19; end; upper_bound rng lower_sum_set(f)<= lower_integral(f+g)-lower_integral( g) by A35,SEQ_4:45; then A45: lower_integral(f) + lower_integral(g) <= lower_integral(f+g) by XREAL_1:19 ; A46: upper_integral(f+g)>=lower_integral(f+g) by A6,Th47; then integral(f)+integral(g) <= upper_integral(f+g) by A45,A5,XXREAL_0:2; then upper_integral(f+g)=integral(f) + integral(g) by A30,XXREAL_0:1; then A47: upper_integral(f+g) = lower_integral(f+g) by A45,A46,A5,XXREAL_0:1; f+g is upper_integrable by A15; hence thesis by A11,A45,A5,A30,A47,XXREAL_0:1; end; theorem for f being FinSequence holds i in dom f & j in dom f & i<=j implies len mid(f,i,j) = j-i+1 by Lm1;