:: The Basic Existence Theorem of Riemann-Stieltjes Integral :: by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama :: :: Received October 18, 2016 :: Copyright (c) 2016-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 NUMBERS, INTEGRA1, SUBSET_1, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4, CARD_1, REAL_1, ARYTM_3, ARYTM_1, CARD_3, FINSEQ_2, INTEGRA2, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1, XXREAL_1, FUNCT_3, PARTFUN1, TARSKI, FINSET_1, INTEGR15, MEASURE5, FUNCT_7, INTEGR22, VALUED_0, ZFMISC_1, FCONT_2, ORDINAL4, FUNCOP_1; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, SEQ_1, SEQ_2, RVSUM_1, SEQ_4, RCOMP_1, FCONT_1, FCONT_2, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGR22; constructors REAL_1, FINSEQOP, MONOID_0, SEQ_4, NAT_D, FCONT_1, FCONT_2, RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2, INTEGR22; registrations NUMBERS, XREAL_0, INTEGRA1, NAT_1, MEMBERED, ORDINAL1, FCONT_1, VALUED_0, RELSET_1, CARD_1, MEASURE5, FINSEQ_1, RVSUM_1, FINSET_1, SEQ_4, FINSEQ_2, RELAT_1, SEQM_3, INT_1, XXREAL_2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI; equalities XBOOLE_0, RCOMP_1, BINOP_1, FINSEQ_1, FINSEQ_2, INTEGR22; expansions FINSEQ_1, MEMBERED; theorems XBOOLE_0, XBOOLE_1, XREAL_0, INTEGRA1, INTEGRA4, XXREAL_2, XXREAL_0, RELAT_1, XCMPLX_1, ORDINAL1, XREAL_1, SEQ_4, SEQ_2, FINSEQ_1, FINSEQ_2, RVSUM_1, FUNCT_1, FUNCT_2, PARTFUN1, VALUED_1, ZFMISC_1, TARSKI, COMPLEX1, FINSEQ_3, XXREAL_1, SUBSET_1, VALUED_0, NAT_1, FCONT_2, INTEGR20, FINSEQ_4, FINSEQ_5, INTEGRA3, ABSVALUE, INT_1, FUNCOP_1, INTEGR22; schemes FUNCT_2, FINSEQ_1, NAT_1, INTEGR20, BINOP_1; begin :: 1. Preliminaries theorem Th1: for E be Real, q be FinSequence of REAL, S be FinSequence of REAL st len S = len q & for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E holds Sum S = (Sum q) * E proof let E be Real; defpred P[Nat] means for q be FinSequence of REAL, S be FinSequence of REAL st $1 = len S & len S = len q & for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E holds Sum S = (Sum q)*E; A1: P[0] proof let q be FinSequence of REAL, S be FinSequence of REAL; assume 0 = len S & len S = len q & for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E; then <*> REAL = S & <*> REAL = q; hence thesis by RVSUM_1:72; end; A3: now let i be Nat; assume A4: P[i]; now let q be FinSequence of REAL, S be FinSequence of REAL; set S0 = S|i, q0 = q|i; assume A5: i+1 = len S & len S = len q & for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E; A6: for k be Nat st k in dom S0 holds ex r be Real st r = q0.k & S0.k= r * E proof let k be Nat; assume k in dom S0; then A7: k in Seg i & k in dom S by RELAT_1:57; then consider r be Real such that A8: r = q.k & S.k= r * E by A5; take r; thus thesis by A7,A8,FUNCT_1:49; end; dom S = Seg(i+1) by A5,FINSEQ_1:def 3; then consider r be Real such that A9: r = q.(i+1) & S.(i+1)= r * E by A5,FINSEQ_1:4; A10: 1 <= i + 1 & i + 1 <= len q by A5,NAT_1:11; q = (q|i)^<*q/.(i+1)*> by A5,FINSEQ_5:21; then q = q0^<*q.(i+1)*> by A10,FINSEQ_4:15; then (Sum q)*E = (Sum q0 + q.(i+1))*E by RVSUM_1:74; then A11: (Sum q)*E = (Sum q0)*E + q.(i+1)*E; A12: i = len S0 & i = len q0 by A5,FINSEQ_1:59,NAT_1:11; reconsider v=S.(i+1) as Real; S = (S|i)^<* S/.len S *> by A5,FINSEQ_5:21; then S = S0^<* v *> by A5,A10,FINSEQ_4:15; then Sum S = Sum S0 + v by RVSUM_1:74; hence Sum S = (Sum q)*E by A4,A6,A9,A11,A12; end; hence P[i+1]; end; for i being Nat holds P[i] from NAT_1:sch 2(A1,A3); hence thesis; end; Lm1: for xseq,yseq be FinSequence of REAL st len xseq = len yseq + 1 & xseq | (len yseq) = yseq holds ex v be Real st v = xseq.(len xseq) & Sum xseq = Sum yseq + v proof let xseq,yseq be FinSequence of REAL; assume A1: len xseq = len yseq + 1 & xseq| (len yseq) = yseq; take v = xseq.(len xseq); len xseq in Seg len xseq by A1,FINSEQ_1:4; then len xseq in dom xseq by FINSEQ_1:def 3; then v = xseq/.(len xseq) by PARTFUN1:def 6; then xseq = (xseq| (len yseq))^<* v *> by A1,FINSEQ_5:21; hence thesis by A1,RVSUM_1:74; end; theorem Th2: for xseq, yseq be FinSequence of REAL st len xseq = len yseq & (for i be Element of NAT st i in dom xseq holds ex v be Real st v = xseq.i & yseq.i = |.v.|) holds |.Sum xseq.| <= Sum yseq proof defpred P[Nat] means for xseq, yseq be FinSequence of REAL st $1 = len xseq & len xseq = len yseq & (for i be Element of NAT st i in dom xseq holds ex v be Real st v = xseq.i & yseq.i = |.v.|) holds |.Sum xseq.| <= Sum yseq; A1: P[0] proof let xseq be FinSequence of REAL, yseq be FinSequence of REAL; assume A2: 0 = len xseq & len xseq = len yseq & (for i be Element of NAT st i in dom xseq holds ex v be Real st v = xseq.i & yseq.i = |.v.|); then <*>(REAL) = xseq; then Sum xseq = 0 & <*>(REAL) = yseq by A2,RVSUM_1:72; hence thesis by COMPLEX1:44,RVSUM_1:72; end; A3: now let i be Nat; assume A4: P[i]; now let xseq be FinSequence of REAL, yseq be FinSequence of REAL; set xseq0 = xseq|i, yseq0 = yseq|i; assume A5: i+1=len xseq & len xseq = len yseq & for i be Element of NAT st i in dom xseq holds ex v be Real st v=xseq.i & yseq.i=|.v.|; A6: for k be Element of NAT st k in dom xseq0 holds ex v be Real st v=xseq0.k & yseq0.k=|.v.| proof let k be Element of NAT; assume k in dom xseq0; then A8: k in Seg i & k in dom xseq by RELAT_1:57; then consider v be Real such that A9: v=xseq.k & yseq.k=|.v.| by A5; take v; thus thesis by A8,A9,FUNCT_1:49; end; dom xseq = Seg(i+1) by A5,FINSEQ_1:def 3; then consider w be Real such that A10: w=xseq.(i+1) & yseq.(i+1)=|.w.| by A5,FINSEQ_1:4; A11: 1 <= i + 1 & i + 1 <= len yseq by A5,NAT_1:11; yseq = (yseq|i)^<*yseq/.(i+1) *> by A5,FINSEQ_5:21; then yseq = yseq0 ^<*(yseq.(i+1))*> by A11,FINSEQ_4:15; then A12: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74; A13: i=len xseq0 by A5,FINSEQ_1:59,NAT_1:11; then A14: ex v be Real st v=xseq.(len xseq) & Sum xseq = Sum xseq0 + v by A5,Lm1; A15: |. Sum xseq0 + w.|<= |.Sum xseq0 .| + |. w .| by COMPLEX1:56; len xseq0 = len yseq0 by A5,A13,FINSEQ_1:59,NAT_1:11; then |. Sum xseq0 .| + |. w .| <= Sum yseq0 + yseq.(i+1) by A4,A6,A10,A13,XREAL_1:6; hence |. Sum xseq .| <= Sum yseq by A5,A10,A12,A14,A15,XXREAL_0:2; end; hence P[i+1]; end; for i be Nat holds P[i] from NAT_1:sch 2(A1,A3); hence thesis; end; theorem Th3: for p,q be FinSequence of REAL st len p = len q & (for j be Nat st j in dom p holds |. p.j .| <= q.j) holds |. Sum(p) .| <= Sum(q) proof let p, q be FinSequence of REAL; assume A1: len p = len q & (for j be Nat st j in dom p holds |. p.j .| <= q.j); defpred P1[Nat,set] means ex v be Real st v = p.$1 & $2 = |. v .|; A2: for i be Nat st i in Seg len p ex x be Element of REAL st P1[i,x] proof let i be Nat; assume i in Seg len p; reconsider w = |.p.i.| as Element of REAL by XREAL_0:def 1; take w; thus thesis; end; consider u be FinSequence of REAL such that A3: dom u = Seg len p & for i be Nat st i in Seg len p holds P1[i,u.i] from FINSEQ_1:sch 5(A2); A4: for i be Element of NAT st i in dom p holds ex v be Real st v = p.i & u.i = |. v .| proof let i be Element of NAT; assume i in dom p; then i in Seg len p by FINSEQ_1:def 3; hence ex v be Real st v = p.i & u.i = |. v .| by A3; end; A5: len u = len p by A3,FINSEQ_1:def 3; then A6: |.Sum p.| <= Sum u by A4,Th2; set i = len p; reconsider uu=u as Element of i-tuples_on REAL by A5,FINSEQ_2:92; reconsider qq=q as Element of i-tuples_on REAL by A1,FINSEQ_2:92; now let j be Nat; assume j in Seg i; then A7: j in dom p by FINSEQ_1:def 3; then ex v be Real st v = p.j & u.j = |. v .| by A4; hence uu.j <= qq.j by A1,A7; end; then Sum uu <= Sum qq by RVSUM_1:82; hence thesis by A6,XXREAL_0:2; end; theorem Th4: for n be Nat, a be object holds len (n |-> a) = n proof let n be Nat, a be object; set x = n |-> a; dom x = Seg len x by FINSEQ_1:def 3; hence thesis by FINSEQ_1:6,FUNCOP_1:13; end; theorem Th5: for p be FinSequence, a be object holds p = (len p) |-> a iff (for k be object st k in dom p holds p.k = a) proof let p be FinSequence, a be object; thus p = (len p) |-> a implies for k be object st k in dom p holds p.k = a proof assume A2: p = (len p) |-> a; let k be object; assume k in dom p; then k in Seg len p by FINSEQ_1:def 3; hence thesis by A2,FINSEQ_2:57; end; assume for k be object st k in dom p holds p.k = a; then p = dom p --> a by FUNCOP_1:11; hence thesis by FINSEQ_1:def 3; end; theorem Th8: for p be FinSequence of REAL, i be Nat, r be Real st i in dom p & p.i = r & for k be Nat st k in dom p & k <> i holds p.k = 0 holds Sum p = r proof defpred P[Nat] means for p be FinSequence of REAL, i be Nat, r be Real st len p = $1 & i in dom p & p.i = r & (for k be Nat st k in dom p & k <> i holds p.k = 0) holds Sum p = r; A1: P[0] proof let p be FinSequence of REAL, i be Nat, r be Real; assume that A2: len p = 0 and A3: i in dom p and p.i = r and for k be Nat st k in dom p & k <> i holds p.k = 0; p = <*>REAL by A2; hence thesis by A3; end; A4: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume A5: P[n]; P[n+1] proof let p be FinSequence of REAL, i be Nat, r be Real; assume that A6: len p = n+1 and A7: i in dom p and A8: p.i = r and A9: for k be Nat st k in dom p & k <> i holds p.k = 0; consider q be FinSequence of REAL, a be Element of REAL such that A10: p = q ^ <*a*> by A6,FINSEQ_2:19; A11: len p = len q + 1 by A10,FINSEQ_2:16; A12: 1 <= i <= n+1 by A6,A7,FINSEQ_3:25; per cases; suppose A13: i <> n+1; then 1 <= i < n+1 by A12,XXREAL_0:1; then A14: 1 <= i <= n by INT_1:7; A15: q.i = r proof q = p | dom q by A10,FINSEQ_1:21; hence thesis by A6,A8,A11,A14,FUNCT_1:47,FINSEQ_3:25; end; A17: for k be Nat st k in dom q & k <> i holds q.k = 0 proof let k be Nat; assume that A18: k in dom q and A19: k <> i; A20: dom q c= dom p by A10,FINSEQ_1:26; q.k = p.k by A10,A18,FINSEQ_1:def 7 .= 0 by A9,A18,A19,A20; hence thesis; end; A21: 1 <= n+1 <= n+1 by XREAL_1:31; a = p.(n+1) by A6,A10,A11,FINSEQ_1:42 .= 0 by A6,A9,A13,A21,FINSEQ_3:25; then Sum p = Sum q + 0 by A10,RVSUM_1:74 .= r by A5,A6,A11,A14,A15,A17,FINSEQ_3:25; hence thesis; end; suppose A22: i = n+1; for k be object st k in dom q holds q.k = 0 proof let k be object; assume A23: k in dom q; then reconsider k as Nat; A24: 1 <= k <= n by A6,A11,A23,FINSEQ_3:25; A25: dom q c= dom p by A10,FINSEQ_1:26; A26: k+0 < n+1 by A24,XREAL_1:8; q.k = p.k by A10,A23,FINSEQ_1:def 7 .= 0 by A9,A22,A23,A25,A26; hence thesis; end; then A27: q = n |-> (0 qua Real) by A6,A11,Th5; A28: a = r by A6,A8,A10,A11,A22,FINSEQ_1:42; Sum p = Sum q + a by A10,RVSUM_1:74 .= 0 + r by A27,A28,RVSUM_1:81; hence thesis; end; end; hence thesis; end; A29: for k be Nat holds P[k] from NAT_1:sch 2(A1,A4); let p be FinSequence of REAL, i be Nat, r be Real; assume A30: i in dom p & p.i = r & for k be Nat st k in dom p & k <> i holds p.k = 0; len p is Nat; hence thesis by A29,A30; end; theorem Th9: for p,q be FinSequence of REAL st len p <= len q & for i be Nat st i in dom q holds (i <= len p implies q.i = p.i) & (len p < i implies q.i = 0) holds Sum q = Sum p proof let p,q be FinSequence of REAL; assume that A1: len p <= len q and A2: for i be Nat st i in dom q holds (i <= len p implies q.i = p.i) & (len p < i implies q.i = 0); len q - len p is Nat by A1,NAT_1:21; then consider ix be Nat such that A3: ix = len q - len p; set x = ix |-> (0 qua Real); A5: Sum x = 0 by RVSUM_1:81; q = p ^ x proof A6: len x = ix by Th4; then A7: len q = len p + len x by A3; A8: dom q = Seg(len p + len x) by A3,A6,FINSEQ_1:def 3; A9: for i be Nat st i in dom p holds q.i = p.i proof let i be Nat; assume i in dom p; then A10: 1 <= i <= len p by FINSEQ_3:25; then 1 <= i <= len q by A1,XXREAL_0:2; then i in dom q by FINSEQ_3:25; hence thesis by A2,A10; end; for i be Nat st i in dom x holds q.(len p + i) = x.i proof let i be Nat; assume i in dom x; then A11: i in Seg ix by FUNCOP_1:13; then A12: x.i = 0 by FINSEQ_2:57; consider j be Nat such that A13: j = len p + i; A14: i >= 1 by A11,FINSEQ_1:1; then A15: len p < j by A13,NAT_1:19; A16: 0+1 <= j by A13,A14,INT_1:7; i <= len x by A6,A11,FINSEQ_1:1; then j <= len q by A7,A13,XREAL_1:6; then j in dom q by A16,FINSEQ_3:25; hence thesis by A2,A12,A13,A15; end; hence thesis by A8,A9,FINSEQ_1:def 7; end; then Sum q = Sum p + Sum x by RVSUM_1:75 .= Sum p by A5; hence thesis; end; theorem Th10: for a,b,c,d be Real st b <= c holds [.a,b.] /\ [.c,d.] c= [.b,b.] proof let a,b,c,d be Real; assume A1: b <= c; per cases; suppose A2: a <= b; per cases; suppose c <= d; then b <= d by A1,XXREAL_0:2; then [.a,b.] /\ [.b,d.] = [.b,b.] by A2,XXREAL_1:143; hence [.a,b.] /\ [.c,d.] c= [.b,b.] by A1,XBOOLE_1:26,XXREAL_1:34; end; suppose d < c; then [.c,d.] = {} by XXREAL_1:29; hence [.a,b.] /\ [.c,d.] c= [.b,b.]; end; end; suppose b < a; then [.a,b.] = {} by XXREAL_1:29; hence [.a,b.] /\ [.c,d.] c= [.b,b.]; end; end; theorem Th11: for a be Real, A be Subset of REAL, rho be real-valued Function st A c= [.a,a.] holds vol(A,rho) = 0 proof let a be Real, A be Subset of REAL, rho be real-valued Function; assume A c= [.a,a.]; then A c= {a} by XXREAL_1:17; then per cases by ZFMISC_1:33; suppose A = {}; hence vol(A,rho) = 0 by INTEGR22:def 1; end; suppose A = {a}; hence vol(A,rho) = rho.(upper_bound {a}) - rho.(lower_bound {a}) by INTEGR22:def 1 .= rho.(upper_bound {a}) - rho.(upper_bound {a}) by SEQ_4:10 .= 0; end; end; theorem Th12: for s be non empty increasing FinSequence of REAL, m be Nat st m in dom s holds s|m is non empty increasing FinSequence of REAL proof let s be non empty increasing FinSequence of REAL, m be Nat; assume a0: m in dom s; then 1 <= m <= len s by FINSEQ_3:25; then A2: len(s|m) = m by FINSEQ_1:59; set H = s|m; for e1,e2 be ExtReal st e1 in dom H & e2 in dom H & e1 < e2 holds H.e1 < H.e2 proof let e1,e2 be ExtReal; assume A3: e1 in dom H & e2 in dom H & e1 < e2; then A5: e1 in dom s & e2 in dom s by RELAT_1:57; s.e1 = H.e1 & s.e2 = H.e2 by A3,FUNCT_1:47; hence H.e1 < H.e2 by A3,A5,VALUED_0:def 13; end; hence thesis by A2,VALUED_0:def 13,a0,FINSEQ_3:25; end; theorem Th13: for s,t be non empty increasing FinSequence of REAL st s.(len s) < t.1 holds s^t is non empty increasing FinSequence of REAL proof let s,t be non empty increasing FinSequence of REAL; assume A1: s.(len s) < t.1; set H = s^t; A2: len H = len s + len t by FINSEQ_1:22; for e1,e2 be ExtReal st e1 in dom H & e2 in dom H & e1 < e2 holds H.e1 < H.e2 proof let e1,e2 be ExtReal; assume A3: e1 in dom H & e2 in dom H & e1 < e2; then reconsider ie1 = e1,ie2 = e2 as Nat; A5: 1 <= ie1 <= len s + len t & 1 <= ie2 <= len s + len t by A2,A3,FINSEQ_3:25; per cases; suppose A6: ie2 <= len s; then A7: ie1 <= len s by A3,XXREAL_0:2; A8: ie1 in dom s & ie2 in dom s by A5,A6,A7,FINSEQ_3:25; then H.e1 = s.e1 & H.e2 = s.e2 by FINSEQ_1:def 7; hence H.e1 < H.e2 by A3,A8,VALUED_0:def 13; end; suppose A9: len s < ie2; per cases; suppose A10: len s < ie1; then a10: len s < ie2 by A3,XXREAL_0:2; A11: not ie1 in dom s & not ie2 in dom s by A10,FINSEQ_3:25,a10; then consider n1 being Nat such that A12: n1 in dom t & ie1 = (len s) + n1 by A3,FINSEQ_1:25; consider n2 being Nat such that A13: n2 in dom t & ie2 = (len s) + n2 by A3,A11,FINSEQ_1:25; A14: H.e1 = t.n1 by A12,FINSEQ_1:def 7; A15: H.e2 = t.n2 by A13,FINSEQ_1:def 7; ie1 - (len s) < ie2 -(len s) by A3,XREAL_1:14; hence H.e1 < H.e2 by A12,A13,A14,A15,VALUED_0:def 13; end; suppose A16: ie1 <= len s; not ie2 in dom s by FINSEQ_3:25,A9; then consider n2 being Nat such that A17:n2 in dom t & ie2 = (len s) + n2 by A3,FINSEQ_1:25; A18: 1<=n2 <= len t by A17,FINSEQ_3:25; 1 <= len t by A18,XXREAL_0:2; then 1 in dom t by FINSEQ_3:25; then A19: t.1 <= t.n2 by A17,A18,VALUED_0:def 15; A20: H.e2 = t.n2 by A17,FINSEQ_1:def 7; A21: ie1 in dom s by A5,A16,FINSEQ_3:25; then A22: H.e1 = s.ie1 by FINSEQ_1:def 7; len s in Seg len s by FINSEQ_1:3; then len s in dom s by FINSEQ_1:def 3; then s.ie1 <= s.(len s) by A16,A21,VALUED_0:def 15; then s.ie1 < t.1 by A1,XXREAL_0:2; hence H.e1 < H.e2 by A19,A20,A22,XXREAL_0:2; end; end; end; hence thesis by VALUED_0:def 13; end; theorem Th14: for s be non empty increasing FinSequence of REAL, a be Real st s.(len s) < a holds s^<*a*> is non empty increasing FinSequence of REAL proof let s be non empty increasing FinSequence of REAL, a be Real; assume A1: s.(len s) < a; reconsider a0 = a as Element of REAL by XREAL_0:def 1; reconsider t = <*a0*> as non empty increasing FinSequence of REAL; s.(len s) < t.1 by A1,FINSEQ_1:40; hence thesis by Th13; end; theorem Th15: for T be FinSequence of REAL, n,m be Nat st n+1 < m <= len T holds ex TM1 be FinSequence of REAL st len TM1 = m-(n+1) & rng TM1 c= rng T & for i be Nat st i in dom TM1 holds TM1.i = T.(i+n) proof let T be FinSequence of REAL, n,m be Nat; assume A1: n+1 < m <= len T; deffunc F(Nat) = T.($1+n); m-(n+1) in NAT by A1,INT_1:5; then reconsider m1 = m-(n+1) as Nat; consider p being FinSequence such that A2: len p = m1 & for k being Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch 2; A3: rng p c= rng T proof let x be object; assume x in rng p; then consider i be object such that A4: i in dom p & x = p.i by FUNCT_1:def 3; reconsider i as Nat by A4; A6: p.i = T.(i+n) by A2,A4; A7: 1 <= i <= m1 by A2,FINSEQ_3:25,A4; A8: i + n <= m1 + n by A7,XREAL_1:6; m - 1 <= m - 0 by XREAL_1:10; then m - 1 <= len T by A1,XXREAL_0:2; then A9: i + n <= len T by A8,XXREAL_0:2; 1 + 0 <= i + n by A7,XREAL_1:7; then i+n in dom T by FINSEQ_3:25,A9; hence thesis by A4,A6,FUNCT_1:3; end; then reconsider p as FinSequence of REAL by FINSEQ_1:def 4,XBOOLE_1:1; take p; thus len p = m-(n+1) by A2; thus rng p c= rng T by A3; let i be Nat; assume i in dom p; hence thesis by A2; end; theorem Th16: for T be non empty increasing FinSequence of REAL, n,m be Nat st n+1 < m <= len T holds ex TM1 be non empty increasing FinSequence of REAL st len TM1 = m-(n+1) & rng TM1 c= rng T & for i be Nat st i in dom TM1 holds TM1.i = T.(i+n) proof let T be non empty increasing FinSequence of REAL, n,m be Nat; assume A1: n+1 < m <= len T; then consider p be FinSequence of REAL such that A2: len p = m-(n+1) & rng p c= rng T & for i be Nat st i in dom p holds p.i = T.(i+n) by Th15; m-(n+1) in NAT by A1,INT_1:5; then reconsider m1 = m-(n+1) as Nat; len p <> 0 by A1,A2; then reconsider p as non empty FinSequence of REAL; for e1,e2 be ExtReal st e1 in dom p & e2 in dom p & e1 < e2 holds p.e1 < p.e2 proof let e1,e2 be ExtReal; assume A3: e1 in dom p & e2 in dom p & e1 < e2; then reconsider ie1 = e1,ie2 = e2 as Nat; A5: p.e1 = T.(ie1+n) by A2,A3; A6: p.e2 = T.(ie2+n) by A2,A3; A7: 1 <= ie1 <= m1 by A2,A3,FINSEQ_3:25; A8: 1 <= ie2 <= m1 by A2,A3,FINSEQ_3:25; A9: ie1 + n <= m1 + n by A7,XREAL_1:6; m - 1 <= m - 0 by XREAL_1:10; then A10: m - 1 <= len T by A1,XXREAL_0:2; then A11: ie1+n <= len T by A9,XXREAL_0:2; 1 + 0 <= ie1 + n by A7,XREAL_1:7; then A12: ie1+n in dom T by A11,FINSEQ_3:25; A13: 1 + 0 <= ie2 + n by A8,XREAL_1:7; ie2 + n <= m1 + n by A8,XREAL_1:6; then ie2 + n <= len T by A10,XXREAL_0:2; then A14: ie2 + n in dom T by FINSEQ_3:25,A13; ie1 + n < ie2 + n by A3,XREAL_1:8; hence thesis by A5,A6,A12,A14,VALUED_0:def 13; end; then reconsider p as non empty increasing FinSequence of REAL by VALUED_0:def 13; take p; thus thesis by A2; end; theorem Th17: for p be FinSequence of REAL, n,m be Nat st n+1 < m <= len p holds ex pM1 be FinSequence of REAL st len pM1 = m-(n+1)-1 & rng pM1 c= rng p & for i be Nat st i in dom pM1 holds pM1.i = p.(i+n+1) proof let p be FinSequence of REAL, n,m be Nat; assume A1: n+1 < m <= len p; set n1 = n+1; A2: n1 + 1 <= m by A1,NAT_1:13; per cases; suppose A3: n1 + 1 = m; set pM1 = <*>REAL; take pM1; thus len pM1 = m-(n+1)-1 by A3; thus rng pM1 c= rng p; thus for i be Nat st i in dom pM1 holds pM1.i = p.(i+n+1); end; suppose n1 + 1 <> m; then n1 + 1 < m by A2,XXREAL_0:1; then consider TM1 be FinSequence of REAL such that A4: len TM1 = m-(n1+1) & rng TM1 c= rng p & for i be Nat st i in dom TM1 holds TM1.i = p.(i+n1) by A1,Th15; take TM1; thus len TM1 = m-(n+1)-1 by A4; thus rng TM1 c= rng p by A4; let i be Nat; assume i in dom TM1; hence TM1.i = p.(i+n1) by A4 .= p.(i+n+1); end; end; begin :: 2. Existence of Riemann-Stieltjes Integral for Continuous Functions theorem Th18: for A be non empty closed_interval Subset of REAL, T be Division of A, rho be real-valued Function, B be non empty closed_interval Subset of REAL, S0 be non empty increasing FinSequence of REAL, ST be FinSequence of REAL st B c= A & lower_bound B = lower_bound A & ex S be Division of B st S = S0 & len ST = len S & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .| holds ex H be Division of B, F be var_volume of rho,H st Sum ST = Sum(F) proof let A be non empty closed_interval Subset of REAL, T be Division of A, rho be real-valued Function; defpred P[Nat] means for B be non empty closed_interval Subset of REAL, S0 be non empty increasing FinSequence of REAL, ST be FinSequence of REAL st B c= A & lower_bound B=lower_bound A & len S0 = $1 & ex S be Division of B st S = S0 & len ST = len S & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .| holds ex H be Division of B, F be var_volume of rho,H st Sum ST = Sum(F); A1: P[0]; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; let B be non empty closed_interval Subset of REAL, S0 be non empty increasing FinSequence of REAL, ST be FinSequence of REAL; assume A4: B c= A & lower_bound B=lower_bound A & len S0 = k+1 & ex S be Division of B st S = S0 & len ST = len S & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .|; then consider S be Division of B such that A5: S = S0 & len ST = len S & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .|; Z: dom ST = dom S by A5,FINSEQ_3:29; per cases; suppose A6: k = 0; set IDX = {i where i is Nat : i in dom T & T.i < upper_bound B}; IDX c= dom T proof let x be object; assume x in IDX; then ex i being Nat st x=i & i in dom T & T.i < upper_bound B; hence thesis; end; then reconsider IDX as finite Subset of NAT by XBOOLE_1:1; a: 1 <= len T by NAT_1:14; then A7: 1 in dom T by FINSEQ_3:25; ST = <*ST.1*> by A4,A6,FINSEQ_1:40; then A8: Sum ST = ST.1 by RVSUM_1:73; A10: 1 in dom S by A4,A5,A6,FINSEQ_3:25; A11: S.1 = upper_bound B by A4,A5,A6,INTEGRA1:def 2; per cases; suppose A12: IDX = {}; set F = the var_volume of rho,S; take S,F; F = <*F.1*> by A4,A5,A6,FINSEQ_1:40,INTEGR22:def 2; then A13: Sum F = F.1 by RVSUM_1:73; not 1 in IDX by A12; then A14: upper_bound B <= T.1 by A7; A15: F.1 = |. vol(divset(S,1), rho) .| by A4,A5,A6,FINSEQ_3:25,INTEGR22:def 2; consider p be FinSequence of REAL such that A16: ST.1 = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol (divset(T,i) /\ divset(S,1),rho) .| by A4,A5,A6,FINSEQ_3:25; Z: dom p = dom T by A16,FINSEQ_3:29; A18: p.1 = |. vol(divset(T,1) /\ divset(S,1), rho) .| by FINSEQ_3:25,a,A16; A19: divset(S,1) c= B by A4,A5,A6,FINSEQ_3:25,INTEGRA1:8; A20: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4; A22: lower_bound divset(T,1) = lower_bound A & upper_bound divset(T,1) = T.1 by INTEGRA1:def 4,A7; [. lower_bound B, upper_bound B .] c= [. lower_bound divset(T,1), upper_bound divset(T,1) .] by A4,A14,A22,XXREAL_1:34; then [. lower_bound B, upper_bound B .] c= divset(T,1) by INTEGRA1:4; then divset(S,1) c= divset(T,1) by A19,A20; then A23: p.1 = |. vol(divset(S,1), rho) .| by A18,XBOOLE_1:28; for i be Nat st i in dom p & i <> 1 holds p.i = 0 proof let i be Nat; assume A24: i in dom p & i <> 1; then A26: 1 <= i <= len p by FINSEQ_3:25; then 1 < i by A24,XXREAL_0:1; then 1+1 <= i by NAT_1:13; then A27: 2-1 <= i-1 by XREAL_1:9; then reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12; i-1 <= len p - 0 by A26,XREAL_1:13; then i1 in dom T by A16,A27,FINSEQ_3:25; then A28: T.1 <= T.(i-1) by A7,A27,VALUED_0:def 15; A29: lower_bound divset(T,i) = T.(i-1) & upper_bound divset(T,i) = T.i by Z,A24,INTEGRA1:def 4; dom p = dom T by FINSEQ_3:29,A16; then A30: p.i = |. vol(divset(T,i) /\ divset(S,1), rho) .| by A16,A24; divset(T,i) /\ divset(S,1) c= divset(T,i) /\ B by A10,INTEGRA1:8,XBOOLE_1:26; then A31: divset(T,i) /\ divset(S,1) c= [. lower_bound B, upper_bound B .] /\ [. lower_bound divset(T,i), upper_bound divset(T,i) .] by A20,INTEGRA1:4; [. lower_bound B, upper_bound B .] /\ [. lower_bound divset(T,i), upper_bound divset(T,i) .] c= [.upper_bound B,upper_bound B.] by A14,A28,A29,Th10,XXREAL_0:2; then divset(T,i) /\ divset(S,1) c= [.upper_bound B,upper_bound B.] by A31; hence thesis by A30,COMPLEX1:44,Th11; end; hence Sum ST = Sum(F) by A8,A13,A15,A16,a,FINSEQ_3:25,A23,Th8; end; suppose A32: IDX <> {}; A33: sup IDX in IDX by A32,XXREAL_2:def 6; then reconsider n = sup IDX as Nat; A34: ex i be Nat st n=i & i in dom T & T.i < upper_bound B by A33; A35: 1 <= n <= len T by A34,FINSEQ_3:25; n <> len T proof assume n = len T; then upper_bound A < upper_bound B by A34,INTEGRA1:def 2; hence contradiction by A4,XXREAL_2:59; end; then n < len T by A35,XXREAL_0:1; then A37: 1 <= n+1 <= len T by NAT_1:11,NAT_1:13; then A38: n+1 in dom T by FINSEQ_3:25; A39: upper_bound B <= T.(n+1) proof assume T.(n+1) < upper_bound B; then n+1 in IDX by A38; hence contradiction by NAT_1:16,XXREAL_2:4; end; set H = (T|n)^ <* upper_bound B *>; upper_bound B is Element of REAL by XREAL_0:def 1; then A40: <* upper_bound B *> is FinSequence of REAL by FINSEQ_1:74; A41: len (T|n) = n by A35,FINSEQ_1:59; len <* upper_bound B *> = 1 by FINSEQ_1:39; then A42: len H = n+1 by A41,FINSEQ_1:22; reconsider H as non empty FinSequence of REAL by A40,FINSEQ_1:75; for e1,e2 be ExtReal st e1 in dom H & e2 in dom H & e1 < e2 holds H.e1 < H.e2 proof let e1,e2 be ExtReal; assume A43: e1 in dom H & e2 in dom H & e1 < e2; then reconsider i = e1, j = e2 as Nat; A45: 1<=i <= n+1 & 1<=j <= n+1 by A42,A43,FINSEQ_3:25; per cases; suppose A46: j = n+1; then A47: H.e2 = upper_bound B by A41,FINSEQ_1:42; A48: i <= n by A43,A46,NAT_1:13; then A49: i in dom (T|n) by A41,A45,FINSEQ_3:25; then A50: H.e1 = (T|n) .i by FINSEQ_1:def 7 .= T.i by A49,FUNCT_1:47; i <= len T by A37,A43,A46,XXREAL_0:2; then i in dom T by A45,FINSEQ_3:25; then T.i <= T.n by A34,A48,VALUED_0:def 15; hence H.e1 < H.e2 by A34,A47,A50,XXREAL_0:2; end; suppose j <> n+1; then j < n+1 by A45,XXREAL_0:1; then A52: j <= n by NAT_1:13; then A53: j in dom (T|n) by A41,A45,FINSEQ_3:25; then A54: H.e2 = (T|n) .j by FINSEQ_1:def 7 .= T.j by A53,FUNCT_1:47; A55: i <= n by A43,A52,XXREAL_0:2; then A56: i in dom (T|n) by A41,A45,FINSEQ_3:25; then A57: H.e1 = (T|n) .i by FINSEQ_1:def 7 .= T.i by A56,FUNCT_1:47; i <= len T by A35,A55,XXREAL_0:2; then A58: i in dom T by A45,FINSEQ_3:25; j <= len T by A35,A52,XXREAL_0:2; then j in dom T by A45,FINSEQ_3:25; hence H.e1 < H.e2 by A43,A54,A57,A58,VALUED_0:def 13; end; end; then reconsider H as non empty increasing FinSequence of REAL by VALUED_0:def 13; A59: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4; A60: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; A61: H.(len H) = upper_bound B by A41,A42,FINSEQ_1:42; A62: rng H = rng(T|n) \/ rng <* upper_bound B *> by FINSEQ_1:31; A63: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39; A64: rng(T|n) c= rng T by RELAT_1:70; rng T c= A by INTEGRA1:def 2; then A65: rng (T|n) c= A by A64; lower_bound B <= upper_bound B by SEQ_4:11; then upper_bound B in B by A59; then { upper_bound B } c= A by A4,ZFMISC_1:31; then A66: rng H c= A by A62,A63,A65,XBOOLE_1:8; for z be object st z in rng H holds z in B proof let z be object; assume A67: z in rng H; then reconsider x = z as Real; x in A by A66,A67; then A68: ex r be Real st x = r & lower_bound A <= r & r <= upper_bound A by A60; consider i be object such that A69: i in dom H & x = H.i by A67,FUNCT_1:def 3; reconsider i as Nat by A69; A70: 1 <= i <= len H by A69,FINSEQ_3:25; 1 <= len H <= len H by A70,XXREAL_0:2; then len H in dom H by FINSEQ_3:25; then x <= upper_bound B by A61,A69,A70,VALUED_0:def 15; hence z in B by A4,A59,A68; end; then A71: rng H c= B; reconsider H as Division of B by A61,A71,INTEGRA1:def 2; set F = the var_volume of rho,H; take H,F; A72: len F = len H by INTEGR22:def 2; ST = <*ST.1*> by A4,A6,FINSEQ_1:40; then A73: Sum ST = ST.1 by RVSUM_1:73; consider p be FinSequence of REAL such that A74: ST.1 = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol (divset(T,i) /\ divset(S,1),rho) .| by A4,A5,A6,FINSEQ_3:25; for i be Nat st i in dom p holds (i <= len F implies p.i = F.i) & (len F < i implies p.i = 0) proof let i be Nat; assume A75: i in dom p; dom p = dom T by A74,FINSEQ_3:29; then A76: p.i = |. vol(divset(T,i) /\ divset(S,1), rho) .| by A74,A75; A77: 1 <= i <= len T by A74,A75,FINSEQ_3:25; A78: lower_bound divset(S,1) = lower_bound B & upper_bound divset(S,1) = S.1 by A10,INTEGRA1:def 4; A79: divset(S,1) = [.lower_bound B,upper_bound B.] by A11,A78,INTEGRA1:4; thus i <= len F implies p.i = F.i proof assume i <= len F; then A80: 1 <= i <= len H by A75,FINSEQ_3:25,INTEGR22:def 2; then A81: i in dom H by FINSEQ_3:25; divset(T,i) /\ divset(S,1) = divset(H,i) proof per cases; suppose i <> n+1; then i < n+1 by A42,A80,XXREAL_0:1; then A82: i <= n by NAT_1:13; then A83: i in dom (T|n) by A41,A80,FINSEQ_3:25; then A84: H.i = (T|n) .i by FINSEQ_1:def 7 .= T.i by A83,FUNCT_1:47; A85: i in dom T by A83,RELAT_1:57; then T.i <= T.n by A34,A82,VALUED_0:def 15; then A86: T.i <= upper_bound B by A34,XXREAL_0:2; thus divset(T,i) /\ divset(S,1) = divset(H,i) proof per cases; suppose A87: i = 1; then A88: lower_bound divset(T,i) = lower_bound A & upper_bound divset(T,i) = T.i by A85,INTEGRA1:def 4; A89: lower_bound divset(H,i) = lower_bound B & upper_bound divset(H,i) = H.i by A81,A87,INTEGRA1:def 4; A90: divset(T,i) =[.lower_bound B,T.i.] by A4,A88,INTEGRA1:4; divset(H,i) = [.lower_bound B, T.i .] by A84,A89,INTEGRA1:4 .= divset(T,i) by A4,A88,INTEGRA1:4; hence divset(T,i) /\ divset(S,1) = divset(H,i) by A79,A86,A90,XBOOLE_1:28,XXREAL_1:34; end; suppose A91: i <> 1; then A92: lower_bound divset(T,i) = T.(i-1) & upper_bound divset(T,i) = T.i by A85,INTEGRA1:def 4; A93: lower_bound divset(H,i) = H.(i-1) & upper_bound divset(H,i) = H.i by A81,A91,INTEGRA1:def 4; 1 < i by A77,A91,XXREAL_0:1; then A94: 1-1 < i-1 by XREAL_1:14; then reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12; A95: 1 <= i1 by A94,NAT_1:14; i1 <= n +1 -1 by A42,A80,XREAL_1:13; then A96: i-1 in dom (T|n) by A41,A95,FINSEQ_3:25; then H.(i-1) = (T|n) .(i-1) by FINSEQ_1:def 7 .= T.(i-1) by A96,FUNCT_1:47; then A98: divset(H,i) = [.T.(i-1),T.i .] by A84,A93,INTEGRA1:4; A99: divset(T,i) = [.T.(i-1),T.i .] by A92,INTEGRA1:4; i-1 in dom T by A96,RELAT_1:57; then T.(i-1) in A by INTEGRA1:6; then ex r be Real st r= T.(i-1) & lower_bound A <=r & r <= upper_bound A by A60; hence divset(T,i) /\ divset(S,1) = divset(H,i) by A4,A79,A86,A98,A99,XBOOLE_1:28,XXREAL_1:34; end; end; end; suppose A100: i = n+1; A101: 1 < i by A35,A100,NAT_1:16; A102: lower_bound divset(T,i) = T.(i-1) & upper_bound divset(T,i) = T.i by A38,A100,A101,INTEGRA1:def 4; A103: lower_bound divset(H,i) = H.(i-1) & upper_bound divset(H,i) = H.i by A81,A101,INTEGRA1:def 4; reconsider i1 = i-1 as Nat by A100; A104: i-1 in dom (T|n) by A35,A41,A100,FINSEQ_3:25; then A105: H.(i-1) = (T|n).(i-1) by FINSEQ_1:def 7 .= T.(i-1) by A104,FUNCT_1:47; T.(i-1) in A by A34,A100,INTEGRA1:6; then A106: ex r be Real st r= T.(i-1) & lower_bound A <=r & r <= upper_bound A by A60; thus divset(T,i) /\ divset(S,1) = [.T.(i-1),T.i .] /\ [.lower_bound B,upper_bound B.] by A79,A102,INTEGRA1:4 .= [.T.(i-1),upper_bound B .] by A4,A39,A100,A106,XXREAL_1:143 .= [.H.(i-1),H.i.] by A41,A100,A105,FINSEQ_1:42 .= divset(H,i) by A103,INTEGRA1:4; end; end; hence thesis by A76,A81,INTEGR22:def 2; end; thus len F < i implies p.i = 0 proof assume A107: len F < i; then A108: len H < i by INTEGR22:def 2; A109: 1 <= n+1 by NAT_1:11; i in dom T by A75,A74,FINSEQ_3:29; then lower_bound divset(T,i) = T.(i-1) & upper_bound divset(T,i) = T.i by A42,A72,A107,A109,INTEGRA1:def 4; then A110: divset(T,i) = [.T.(i-1),T.i .] by INTEGRA1:4; n+1 + 1 <= i by A42,A108,NAT_1:13; then A111: n+1 +1 -1 <= i -1 by XREAL_1:9; 1 <= n+1 by NAT_1:11; then A112: 1 <= i-1 by A111,XXREAL_0:2; reconsider i1 = i-1 as Nat by A111,INT_1:3,ORDINAL1:def 12; i-1 <= i-0 by XREAL_1:13; then i-1 <= len T by A77,XXREAL_0:2; then i1 in dom T by A112,FINSEQ_3:25; then T.(n+1) <= T.i1 by A38,A111,VALUED_0:def 15; then divset(T,i) /\ divset(S,1) c= [.upper_bound B,upper_bound B.] by A39,A79,A110,Th10,XXREAL_0:2; hence p.i = 0 by A76,COMPLEX1:44,Th11; end; end; hence Sum ST = Sum(F) by A37,A42,A72,A73,A74,Th9; end; end; suppose A114: k <> 0; set S01 = S0 | k; A115: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4; A116: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; A117: k = len S01 by A4,FINSEQ_1:59,NAT_1:11; dom S0 = Seg(k+1) by A4,FINSEQ_1:def 3; then A118: Seg k c= dom S0 by FINSEQ_1:5,NAT_1:11; for e1,e2 be ExtReal st e1 in dom S01 & e2 in dom S01 & e1 < e2 holds S01.e1 < S01.e2 proof let e1,e2 be ExtReal; assume A119: e1 in dom S01 & e2 in dom S01 & e1 < e2; then A120: e1 in Seg k & e2 in Seg k by A117,FINSEQ_1:def 3; then S01.e1 = S0.e1 & S01.e2 = S0.e2 by FUNCT_1:49; hence thesis by A118,A119,A120,VALUED_0:def 13; end; then reconsider S01 as non empty increasing FinSequence of REAL by A114,A117,VALUED_0:def 13; A121: k in dom S0 by A114,A118,FINSEQ_1:3; then consider B1,B2 be non empty closed_interval Subset of REAL such that A122: B1 = [.lower_bound B, S0.k .] & B2 = [. S0.k, upper_bound B.] & B = B1 \/ B2 by A5,INTEGRA1:32; A123: B1 c= B by A122,XBOOLE_1:7; then A124: B1 c= A by A4; A125: B1 = [. lower_bound B1, upper_bound B1 .] by INTEGRA1:4; then A126: upper_bound B1 = S.k by A5,A122,INTEGRA1:5; A127: lower_bound B1 = lower_bound A by A4,A122,A125,INTEGRA1:5; A128: rng S0 c= B by A5,INTEGRA1:def 2; A129: rng S01 c= rng S0 by RELAT_1:70; for y be object st y in rng S01 holds y in B1 proof let y be object; assume A130: y in rng S01; then y in B by A128,A129; then y in [. lower_bound B, upper_bound B .] by INTEGRA1:4; then consider y1 be Real such that A131: y = y1 & lower_bound B <= y1 & y1 <= upper_bound B; consider x be object such that A132: x in dom S01 & y1 = S01.x by A130,A131,FUNCT_1:def 3; reconsider x as Nat by A132; A133: x in Seg k by A117,A132,FINSEQ_1:def 3; then A134: x <= k by FINSEQ_1:1; now assume x <> k; then x < k by A134,XXREAL_0:1; hence S0.x <= S0.k by A118,A121,A133,VALUED_0:def 13; end; then y1 <= S0.k by A132,A133,FUNCT_1:49; hence y in B1 by A122,A131; end; then A135: rng S01 c= B1; A136: S01.k = S0.k by A114,FINSEQ_1:3,FUNCT_1:49; A137: B1 = [. lower_bound B1, upper_bound B1 .] by INTEGRA1:4; then S01.(len S01) = upper_bound B1 by A117,A122,A136,INTEGRA1:5; then reconsider S1 = S01 as Division of B1 by A135,INTEGRA1:def 2; reconsider ST1 = ST | k as FinSequence of REAL; A138: len S1 = k by A4,FINSEQ_1:59,NAT_1:11; A139: len ST1 = len S1 by A4,A138,FINSEQ_1:59,NAT_1:11; for j be Nat st j in dom S1 holds ex p be FinSequence of REAL st ST1.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S1,j), rho) .| proof let j be Nat; assume A140: j in dom S1; then A141: j in Seg k & j in dom S0 by RELAT_1:57; then consider p be FinSequence of REAL such that A142: ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j), rho) .| by A5; A143: for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S1,j), rho) .| proof let i be Nat; assume A144: i in dom T; A145: divset(S,j) = [. lower_bound divset(S,j), upper_bound divset(S,j) .] & divset(S1,j) = [. lower_bound divset(S1,j), upper_bound divset(S1,j) .] by INTEGRA1:4; divset(S,j) = divset(S1,j) proof per cases; suppose j = 1; then A146: lower_bound(divset(S,j)) = lower_bound B & upper_bound(divset(S,j)) = S.j & lower_bound(divset(S1,j)) = lower_bound B1 & upper_bound(divset(S1,j)) = S1.j by A5,A140,A141,INTEGRA1:def 4; lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5; hence divset(S,j) = divset(S1,j) by A5,A140,A145,A146,FUNCT_1:47; end; suppose A147: j<>1; then A148: lower_bound(divset(S,j)) = S.(j-1) & upper_bound(divset(S,j)) = S.j & lower_bound(divset(S1,j)) = S1.(j-1) & upper_bound(divset(S1,j)) = S1.j by A5,A140,A141,INTEGRA1:def 4; A149: 1 <= j by A141,FINSEQ_1:1; then j-1 in NAT by INT_1:5; then reconsider j1 = j-1 as Nat; 1 < j by A147,A149,XXREAL_0:1; then S.j1 = S1.j1 by A5,A141,FINSEQ_3:12,FUNCT_1:49; hence divset(S,j) = divset(S1,j) by A5,A140,A145,A148,FUNCT_1:47; end; end; hence p.i = |. vol (divset(T,i) /\ divset(S1,j),rho) .| by A142,A144; end; take p; thus thesis by A141,A142,A143,FUNCT_1:49; end; then consider H1 be Division of B1, F1 be var_volume of rho,H1 such that A150: Sum ST1 = Sum(F1) by A3,A124,A127,A138,A139; A151: 1 <= k + 1 <= len ST by A4,NAT_1:11; ST = (ST|k)^<*ST/.(k+1)*> by A4,FINSEQ_5:21; then A152: ST = ST1^<*ST.(k+1)*> by A151,FINSEQ_4:15; dom ST = Seg (k+1) by A4,FINSEQ_1:def 3; then consider p be FinSequence of REAL such that A153: ST.(k+1) = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,(k+1)),rho) .| by Z,A5,FINSEQ_1:4; set JDX = {i where i is Nat : i in dom T & upper_bound B <= T.i }; JDX c= dom T proof let x be object; assume x in JDX; then ex i being Nat st x = i & i in dom T & upper_bound B <= T.i; hence thesis; end; then reconsider JDX as finite Subset of NAT by XBOOLE_1:1; H: dom p = dom T by FINSEQ_3:29,A153; A154: upper_bound B <= upper_bound A by A4,XXREAL_2:59; A155: T.(len T) = upper_bound A by INTEGRA1:def 2; A156: 1 <= len T by NAT_1:14; then A157: 1 in dom T by FINSEQ_3:25; reconsider m = min* JDX as Nat; A159: S.(len S) = upper_bound B by INTEGRA1:def 2; len T in dom T by A156,FINSEQ_3:25; then len T in JDX by A154,A155; then m in JDX by NAT_1:def 1; then consider i being Nat such that A160: m = i & i in dom T & upper_bound B <= T.i; A161: 1 <= k by A114,NAT_1:14; k <= k+1 by NAT_1:11; then k in Seg (k+1) by A161; then A162: k in dom S by A4,A5,FINSEQ_1:def 3; then S.k in B by INTEGRA1:6; then A163: ex r be Real st r = S.k & lower_bound B <= r & r <= upper_bound B by A115; A164: for i be Nat st m <= i & i in dom T holds upper_bound B <= T.i proof let i be Nat; assume m <= i & i in dom T; then T.m <= T.i by A160,VALUED_0:def 15; hence thesis by A160,XXREAL_0:2; end; k+1 in Seg (k+1) by FINSEQ_1:4; then A167: k+1 in dom S by A4,A5,FINSEQ_1:def 3; S.k < S.(k+1) by A162,A167,NAT_1:16,VALUED_0:def 13; then A168: S.k < upper_bound B by A4,A5,INTEGRA1:def 2; A169: divset(S,(k+1)) = [. lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)) .] by INTEGRA1:4; k+1 <> 1 by A114; then A170: lower_bound(divset(S,k+1)) = S.(k+1-1) & upper_bound(divset(S,k+1)) = S.(k+1) by A167,INTEGRA1:def 4; A171: S.(k+1) = upper_bound B by A4,A5,INTEGRA1:def 2; per cases; suppose A172: m = 1; set H = H1 ^ <* upper_bound B *>; A173: upper_bound B <= T.1 by A156,A164,A172,FINSEQ_3:25; upper_bound B is Element of REAL by XREAL_0:def 1; then A174: <* upper_bound B *> is FinSequence of REAL by FINSEQ_1:74; A175: len <* upper_bound B *> = 1 by FINSEQ_1:39; then A176: len H = (len H1) + 1 by FINSEQ_1:22; reconsider H as non empty FinSequence of REAL by A174,FINSEQ_1:75; for e1,e2 be ExtReal st e1 in dom H & e2 in dom H & e1 < e2 holds H.e1 < H.e2 proof let e1,e2 be ExtReal; assume A177: e1 in dom H & e2 in dom H & e1 < e2; then A178: e1 in Seg len H & e2 in Seg len H by FINSEQ_1:def 3; reconsider i = e1, j = e2 as Nat by A177; A179: 1<=i & i <= (len H1) + 1 & 1<=j & j <= (len H1) + 1 by A176,A178,FINSEQ_1:1; per cases; suppose A180: j = (len H1) + 1; then A181: H.e2 = upper_bound B by FINSEQ_1:42; i <= len H1 by A177,A180,NAT_1:13; then A182: i in dom H1 by A179,FINSEQ_3:25; then A183: H.e1 = H1.i by FINSEQ_1:def 7; H1.i in [.lower_bound B, S0.k .] by A122,A182,INTEGRA1:6; then ex r be Real st r = H1.i & lower_bound B <= r & r <= S0.k; hence H.e1 < H.e2 by A5,A168,A181,A183,XXREAL_0:2; end; suppose j <> (len H1) + 1; then j < (len H1) + 1 by A179,XXREAL_0:1; then A184: j <= len H1 by NAT_1:13; then A185: j in dom H1 by A179,FINSEQ_3:25; then A186: H.e2 = H1 .j by FINSEQ_1:def 7; i <= len H1 by A177,A184,XXREAL_0:2; then A187: i in dom H1 by A179,FINSEQ_3:25; then H.e1 = H1 .i by FINSEQ_1:def 7; hence H.e1 < H.e2 by A177,A185,A186,A187,VALUED_0:def 13; end; end; then reconsider H as non empty increasing FinSequence of REAL by VALUED_0:def 13; A188: H.(len H) = upper_bound B by A176,FINSEQ_1:42; rng H1 c= B1 by INTEGRA1:def 2; then A189: rng H1 c= B by A123; A190: rng H = rng H1 \/ rng <* upper_bound B *> by FINSEQ_1:31; A191: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39; lower_bound B <= upper_bound B by SEQ_4:11; then upper_bound B in B by A115; then rng <* upper_bound B *> c= B by A191,ZFMISC_1:31; then reconsider H as Division of B by A188,A189,A190,INTEGRA1:def 2,XBOOLE_1:8; set F = F1 ^<* |. vol([.S.k,upper_bound B.], rho) .| *>; |. vol([.S.k,upper_bound B.], rho) .| is Element of REAL by XREAL_0:def 1; then A192: <* |. vol([.S.k,upper_bound B.], rho) .| *> is FinSequence of REAL by FINSEQ_1:74; reconsider F as FinSequence of REAL by A192,FINSEQ_1:75; A193: len F = len F1 + len <* |. vol([.S.k,upper_bound B.],rho) .| *> by FINSEQ_1:22 .= len H1 + len <* |. vol([.S.k,upper_bound B.],rho) .| *> by INTEGR22:def 2 .= len H1 + 1 by FINSEQ_1:40 .= len H by A175,FINSEQ_1:22; 1 <= len H1 by NAT_1:14; then A194: 1 in dom H1 by FINSEQ_3:25; A195: len F1 = len H1 by INTEGR22:def 2; then A196: dom F1 = dom H1 by FINSEQ_3:29; for j be Nat st j in dom H holds F.j = |. vol(divset(H,j),rho) .| proof let j be Nat; A197: divset(H,j) = [. lower_bound divset(H,j), upper_bound divset(H,j) .] & divset(H1,j) = [. lower_bound divset(H1,j), upper_bound divset(H1,j) .] by INTEGRA1:4; assume A198: j in dom H; then A199: 1 <= j <= len H by FINSEQ_3:25; per cases; suppose A200: j = 1; then A201: lower_bound divset(H,j) = lower_bound B & upper_bound divset(H,j) = H.j by A198,INTEGRA1:def 4; A203: lower_bound divset(H1,j) = lower_bound B1 & upper_bound divset(H1,j) = H1.j by A194,A200,INTEGRA1:def 4; A204: lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5; thus F.j = F1.j by A196,A194,A200,FINSEQ_1:def 7 .= |. vol(divset(H1,j),rho) .| by A200,A194,INTEGR22:def 2 .= |. vol(divset(H,j),rho) .| by A197,A201,A200,A194,A203,A204,FINSEQ_1:def 7; end; suppose A205: j <> 1; per cases; suppose A206: j = len H; then A207: j = len H1 + 1 by A175,FINSEQ_1:22; A208: F.j = |. vol([.S.k,upper_bound B.],rho) .| by A176,A195,A206,FINSEQ_1:42; A209: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A198,A205,INTEGRA1:def 4; j-1 in NAT by A198,INT_1:5,FINSEQ_3:25; then reconsider j1 = j-1 as Nat; 1 < j by A199,A205,XXREAL_0:1; then 1-1 < j1 by XREAL_1:14; then A210: 1 <= j1 by NAT_1:14; j-1 in dom H1 by A207,A210,FINSEQ_3:25; then H.(j-1) = H1.(len H1) by A207,FINSEQ_1:def 7 .= S.k by A126,INTEGRA1:def 2; hence F.j = |. vol(divset(H,j),rho) .| by A197,A206,A208,A209,INTEGRA1:def 2; end; suppose j <> len H; then j < len H1 + 1 by A176,A199,XXREAL_0:1; then L: j <= len H1 by NAT_1:13; then A211: j in Seg len H1 by A199; A212: j in dom H1 by A199,L,FINSEQ_3:25; then A213: H.j = H1.j by FINSEQ_1:def 7; j-1 in NAT by A198,FINSEQ_3:25,INT_1:5; then reconsider j1 = j-1 as Nat; 1 < j by A199,A205,XXREAL_0:1; then j-1 in Seg len H1 by A211,FINSEQ_3:12; then j-1 in dom H1 by FINSEQ_1:def 3; then A214: H.j1 = H1.j1 by FINSEQ_1:def 7; A215: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A198,A205,INTEGRA1:def 4; thus F.j = F1.j by A196,A212,FINSEQ_1:def 7 .= |. vol(divset(H1,j),rho) .| by A212,INTEGR22:def 2 .= |. vol(divset(H,j),rho) .| by A205,A212,A213,A214,A215,INTEGRA1:def 4; end; end; end; then reconsider F as var_volume of rho,H by A193,INTEGR22:def 2; take H,F; A217: p.1 = |. vol(divset(T,1) /\ divset(S,k+1),rho) .| by A156,FINSEQ_3:25,A153; A218: divset(S,k+1) c= B by A167,INTEGRA1:8; A219: B = [. lower_bound B, upper_bound B .] by INTEGRA1:4; A221: lower_bound divset(T,1) = lower_bound A & upper_bound divset(T,1) = T.1 by INTEGRA1:def 4,A157; [. lower_bound B, upper_bound B .] c= [. lower_bound divset(T,1), upper_bound divset(T,1) .] by A4,A173,A221,XXREAL_1:34; then [. lower_bound B, upper_bound B .] c= divset(T,1) by INTEGRA1:4; then divset(S,k+1) c= divset(T,1) by A218,A219; then A222: p.1 = |. vol(divset(S,k+1),rho) .| by A217,XBOOLE_1:28; for i be Nat st i in dom p & i <> 1 holds p.i = 0 proof let i be Nat; assume A223: i in dom p & i <> 1; then A225: 1 <= i <= len p by FINSEQ_3:25; then 1 < i by A223,XXREAL_0:1; then 1+1 <= i by NAT_1:13; then A226: 2-1 <= i-1 by XREAL_1:9; then reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12; i-1 <= len p - 0 by A225,XREAL_1:13; then i1 in dom T by A226,FINSEQ_3:25,A153; then A227: T.1 <= T.(i-1) by A157,A226,VALUED_0:def 15; A228: lower_bound divset(T,i) = T.(i-1) & upper_bound divset(T,i) = T.i by INTEGRA1:def 4,A223,H; A229: p.i = |. vol(divset(T,i) /\ divset(S,k+1),rho) .| by A153,A223,H; divset(T,i) /\ divset(S,k+1) c= divset(T,i) /\ B by A167,INTEGRA1:8,XBOOLE_1:26; then A230: divset(T,i) /\ divset(S,k+1) c= [. lower_bound B, upper_bound B .] /\ [. lower_bound divset(T,i), upper_bound divset(T,i) .] by A219,INTEGRA1:4; [. lower_bound B, upper_bound B .] /\ [. lower_bound divset(T,i), upper_bound divset(T,i) .] c= [.upper_bound B,upper_bound B.] by A173,A227,A228,Th10,XXREAL_0:2; then divset(T,i) /\ divset(S,k+1) c= [.upper_bound B,upper_bound B.] by A230; hence thesis by A229,COMPLEX1:44,Th11; end; then A231: Sum p = |. vol(divset(S,k+1),rho) .| by A153,A156,A222,Th8,FINSEQ_3:25 .= |. vol([.S.k,upper_bound B.],rho) .| by A4,A5,A159,A170,INTEGRA1:4; thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74 .= Sum(F) by A231,RVSUM_1:74; end; suppose A232: m <> 1; S: m in Seg len T by A160,FINSEQ_1:def 3; A233: 1 <= m <= len T by A160,FINSEQ_3:25; then 1 < m by A232,XXREAL_0:1; then a234: m - 1 in Seg len T by FINSEQ_3:12,S; then A234: m-1 in dom T by FINSEQ_1:def 3; then A235: 1 <= m-1 <= len T by FINSEQ_3:25; reconsider m1 = m-1 as Nat by a234; LL: m1 in dom T by a234,FINSEQ_1:def 3; set IDX = {i where i is Nat : i in dom T & T.i <= S.k}; IDX c= dom T proof let x be object; assume x in IDX; then ex i being Nat st x = i & i in dom T & T.i <= S.k; hence thesis; end; then reconsider IDX as finite Subset of NAT by XBOOLE_1:1; per cases; suppose A237: IDX = {}; A238: for i be Nat st i in dom T holds S.k < T.i proof assume not for i be Nat st i in dom T holds S.k < T.i; then consider i be Nat such that A239: i in dom T & not S.k < T.i; i in IDX by A239; hence contradiction by A237; end; reconsider TM1 = T | m1 as non empty increasing FinSequence of REAL by Th12,LL; A240: len TM1= m1 by A235,FINSEQ_1:59; then a240: dom TM1 = Seg m1 by FINSEQ_1:def 3; then A242: TM1.(len TM1) = T.m1 by FUNCT_1:49,A240,FINSEQ_3:25,A235; A243: T.m1 < upper_bound B proof assume not T.m1 < upper_bound B; then A245: m1 in JDX by A234; m-1 < m-0 by XREAL_1:15; hence contradiction by A245,NAT_1:def 1; end; then reconsider TM1B = TM1 ^ <* upper_bound B *> as non empty increasing FinSequence of REAL by A242,Th14; A246: H1.(len H1) = S.k by A126,INTEGRA1:def 2; 1 in Seg len TM1 by A235,A240; then A248: TM1.1 = T.1 by A240,FUNCT_1:49; 1 in dom TM1 by A235,A240,FINSEQ_3:25; then A249: TM1B.1 = T.1 by A248,FINSEQ_1:def 7; reconsider H = H1 ^TM1B as non empty increasing FinSequence of REAL by A157,A238,A246,A249,Th13; A250: rng TM1B = rng TM1 \/ rng <* upper_bound B *> by FINSEQ_1:31; A251: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39; A256: rng TM1 c= B proof let z be object; assume A252: z in rng TM1; then reconsider x = z as Real; x in rng T by A252,RELAT_1:70,TARSKI:def 3; then x in A by INTEGRA1:def 2,TARSKI:def 3; then A253: ex r be Real st x = r & lower_bound A <= r & r <= upper_bound A by A116; consider i be object such that A254: i in dom TM1 & x =TM1.i by A252,FUNCT_1:def 3; reconsider i as Nat by A254; A255: 1 <= i <= len TM1 by FINSEQ_3:25,A254; 1 <= len TM1 by A255,XXREAL_0:2; then len TM1 in dom TM1 by FINSEQ_3:25; then TM1.i <= TM1.(len TM1) by A254,A255,VALUED_0:def 15; then x <= upper_bound B by A242,A243,A254,XXREAL_0:2; hence z in B by A4,A115,A253; end; lower_bound B <= upper_bound B by SEQ_4:11; then upper_bound B in B by A115; then { upper_bound B } c= B by ZFMISC_1:31; then A257: rng TM1B c= B by A250,A251,A256,XBOOLE_1:8; rng H1 c= B1 by INTEGRA1:def 2; then rng H1 c= B by A123; then rng H1 \/ rng TM1B c= B by A257,XBOOLE_1:8; then A258: rng H c= B by FINSEQ_1:31; A259: len TM1B = len TM1 + len <* upper_bound B *> by FINSEQ_1:22 .= len TM1 + 1 by FINSEQ_1:40; len TM1 + 1 in Seg(len TM1 + 1) by FINSEQ_1:4; then A260: len TM1 + 1 in dom TM1B by A259,FINSEQ_1:def 3; A261: len H = len H1 + (len TM1 + 1) by A259,FINSEQ_1:22; X: 1 in Seg 1; then A262: 1 in dom <* upper_bound B *> by FINSEQ_1:38; H.(len H) = TM1B.(len TM1 + 1) by A260,A261,FINSEQ_1:def 7 .= (<* upper_bound B *>).1 by A262,FINSEQ_1:def 7 .= upper_bound B by FINSEQ_1:40; then reconsider H as Division of B by A258,INTEGRA1:def 2; set q = (p|m1) ^ <* |. vol([. T.m1,upper_bound B .], rho) .| *>; rng q c= REAL; then reconsider q as FinSequence of REAL by FINSEQ_1:def 4; A263: len(p|m1) = m1 by A153,A235,FINSEQ_1:59; A264: len q = len(p|m1) + len <* |. vol([. T.m1,upper_bound B .], rho) .| *> by FINSEQ_1:22 .= m1+ 1 by A263,FINSEQ_1:40 .= m; A265: 1 in dom <* |. vol([. T.m1,upper_bound B .], rho) .| *> by FINSEQ_1:38,X; A266: q.m = q.(m1+1) .= (<* |. vol([. T.m1,upper_bound B .], rho) .| *>).1 by A263,A265,FINSEQ_1:def 7 .= |. vol([. T.m1,upper_bound B .], rho) .| by FINSEQ_1:40; A267: for i be Nat st 1 <= i & i <= m1 holds q.i = |. vol(divset(T,i) /\ divset(S,(k+1)), rho) .| proof let i be Nat; assume A268: 1 <= i <= m1; then A269: i in Seg m1; then A270: i in dom (p|m1) by A263,FINSEQ_1:def 3; C: i <= len T by A235,A268,XXREAL_0:2; thus q.i = (p|m1).i by A270,FINSEQ_1:def 7 .= p.i by A269,FUNCT_1:49 .= |. vol(divset(T,i) /\ divset(S,(k+1)),rho) .| by A153,C,FINSEQ_3:25,A268; end; reconsider F = F1^q as FinSequence of REAL; A272: Sum F = Sum F1 + Sum q by RVSUM_1:75; A273: len F = len F1 + len q by FINSEQ_1:22; A274: len H = len H1 + m1 + 1 by A240,A261; A275: 1 <= len H1 by NAT_1:14; then A276: 1 in dom H1 by FINSEQ_3:25; A277: len F1 = len H1 by INTEGR22:def 2; then A278: dom F1 = dom H1 by FINSEQ_3:29; m-1 <= m-0 by XREAL_1:15; then 1 <= m by A235,XXREAL_0:2; then A279: m in dom q by A264,FINSEQ_3:25; for j be Nat st j in dom H holds F.j = |. vol (divset(H,j),rho) .| proof let j be Nat; A280: divset(H,j) = [. lower_bound divset(H,j), upper_bound divset(H,j) .] & divset(H1,j) = [. lower_bound divset(H1,j), upper_bound divset(H1,j) .] by INTEGRA1:4; assume A281: j in dom H; then A282: 1<=j <= len H by FINSEQ_3:25; per cases; suppose A283: j = 1; then A284: lower_bound divset(H,j) = lower_bound B & upper_bound divset(H,j) = H.j by A281,INTEGRA1:def 4; A285: j in dom H1 by A275,A283,FINSEQ_3:25; then A286: lower_bound divset(H1,j) = lower_bound B1 & upper_bound divset(H1,j) = H1.j by A283,INTEGRA1:def 4; A287: lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5; thus F.j = F1.j by A278,A276,A283,FINSEQ_1:def 7 .= |. vol (divset(H1,j),rho) .| by A285,INTEGR22:def 2 .= |. vol (divset(H,j),rho) .| by A280,A284,A285,A286,A287,FINSEQ_1:def 7; end; suppose A288: j <> 1; per cases; suppose A289: j = len H; A290: F.j = |. vol([. T.m1,upper_bound B .],rho) .| by A240,A261,A266,A277,A279,A289,FINSEQ_1:def 7; A291: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A281,A288,INTEGRA1:def 4; j-1 in NAT by A281,INT_1:5,FINSEQ_3:25; then reconsider j1 = j-1 as Nat; m-1 < m-0 by XREAL_1:15; then m1 in Seg m by A235; then A292: m1 in dom TM1B by A240,A259,FINSEQ_1:def 3; A293: m1 in dom TM1 by A240,A235,FINSEQ_3:25; H.j1 = TM1B.m1 by A274,A289,A292,FINSEQ_1:def 7 .= TM1.m1 by A293,FINSEQ_1:def 7 .= T.m1 by a240,A240,FUNCT_1:49,A235,FINSEQ_3:25; hence F.j = |. vol(divset(H,j),rho) .| by A280,A289,A290,A291,INTEGRA1:def 2; end; suppose j <> len H; then A294: j < len H1 + m by A240,A261,A282,XXREAL_0:1; per cases; suppose j > len H1; then A295: j - len H1 > 0 by XREAL_1:50; then j - len H1 in NAT by INT_1:3; then reconsider j1 = j- len H1 as Nat; A296: j1 < len H1 + m - len H1 by A294,XREAL_1:14; then j1 + 1 <= m by NAT_1:13; then A297: j1 + 1 - 1 <= m - 1 by XREAL_1:13; A298: 1 <= j1 by A295,NAT_1:14; then A299: j1 in Seg m by A296; A300: j1 in dom q by A296,A264,FINSEQ_3:25,A298; A301: j1 in Seg m1 by A297,A298; then A302: j1 in dom TM1 by A240,FINSEQ_1:def 3; A303: F.j = F.(len H1 + j1) .= q.j1 by A277,A300,FINSEQ_1:def 7 .= |. vol(divset(T,j1) /\ divset(S,(k+1)),rho) .| by A267,A297,A298; A304: j1 in dom TM1B by A240,A259,A299,FINSEQ_1:def 3; len TM1 in Seg len TM1 by FINSEQ_1:3; then A305: m1 in dom TM1 by A240,FINSEQ_1:def 3; A306: H.j = H.(len H1 + j1) .= TM1B.j1 by A304,FINSEQ_1:def 7 .= TM1.j1 by A302,FINSEQ_1:def 7 .= T.j1 by A301,FUNCT_1:49; A307: j1 in dom T by A302,RELAT_1:57; m1 in dom T by A305,RELAT_1:57; then T.j1 <= T.m1 by A297,A307,VALUED_0:def 15; then A308: T.j1 <= upper_bound B by A243,XXREAL_0:2; per cases; suppose A309: j1 <> 1; then A310: lower_bound(divset(T,j1)) = T.(j1-1) & upper_bound(divset(T,j1)) = T.j1 by A307,INTEGRA1:def 4; 1 < j1 by A298,A309,XXREAL_0:1; then 1+1 <= j1 by NAT_1:13; then A311: 1+1-1 <= j1-1 by XREAL_1:9; then j1-1 in NAT by INT_1:3; then reconsider j11 = j1-1 as Nat; A312: j11 <= m1-0 by A297,XREAL_1:13; j11 <= len T by A235,A312,XXREAL_0:2; then A313: lower_bound(divset(S,k+1)) <= lower_bound(divset(T,j1)) by A170,A238,A310,A311,FINSEQ_3:25; A314: upper_bound(divset(T,j1)) <= upper_bound divset(S,(k+1)) by A4,A5,A159,A170,A307,A308,A309,INTEGRA1:def 4; A315: divset(T,j1) = [. lower_bound divset(T,j1), upper_bound divset(T,j1) .] by INTEGRA1:4; A316: divset(T,j1) /\ divset(S,(k+1)) = divset(T,j1) by A169,A313,A314,A315,XBOOLE_1:28,XXREAL_1:34; m-1 < m-0 by XREAL_1:15; then 1 <= j11 <= m by A311,A312,XXREAL_0:2; then A317: j11 in dom TM1B by A240,A259,FINSEQ_3:25; A318: j11 in Seg m1 by A311,A312; then A319: j11 in dom TM1 by A240,FINSEQ_1:def 3; A320: H.(j-1) = H.(len H1 + j11) .= TM1B.j11 by A317,FINSEQ_1:def 7 .= TM1.j11 by A319,FINSEQ_1:def 7 .= T.j11 by A318,FUNCT_1:49; A321: upper_bound divset(H,j) = T.j1 by A281,A288,A306,INTEGRA1:def 4 .= upper_bound divset(T,j1) by A307,A309,INTEGRA1:def 4; lower_bound divset(H,j) = T.(j1-1) by A281,A288,A320,INTEGRA1:def 4 .= lower_bound divset(T,j1) by A307,A309,INTEGRA1:def 4; hence F.j = |. vol(divset(H,j), rho) .| by A303,A315,A316,A321,INTEGRA1:4; end; suppose A322: j1 = 1; then A323: lower_bound(divset(T,j1)) = lower_bound A & upper_bound(divset(T,j1)) = T.j1 by A307,INTEGRA1:def 4; A324: divset(T,j1) = [. lower_bound divset(T,j1), upper_bound divset(T,j1) .] by INTEGRA1:4; A325: upper_bound divset(H,j) = T.j1 by A281,A288,A306,INTEGRA1:def 4 .= upper_bound(divset(T,j1)) by A307,A322,INTEGRA1:def 4; A326: len H1 in dom H1 by A275,FINSEQ_3:25; A327: lower_bound(divset(H,j)) = H.(len H1 + j1-1) by A281,A288,INTEGRA1:def 4 .= S.k by A246,A322,A326,FINSEQ_1:def 7; divset(T,j1) /\ divset(S,k+1) = [. S.k, upper_bound divset(T,j1) .] by A4,A163,A169,A170,A171,A308,A323,A324,XXREAL_1:143 .= divset(H,j) by A325,A327,INTEGRA1:4; hence F.j = |. vol(divset(H,j), rho) .| by A303; end; end; suppose B: j <= len H1; then A328: j in Seg len H1 by A282; A329: j in dom H1 by A282,B,FINSEQ_3:25; then A330: H.j = H1.j by FINSEQ_1:def 7; j-1 in NAT by A281,INT_1:5,FINSEQ_3:25; then reconsider j1 = j-1 as Nat; 1 < j by A282,A288,XXREAL_0:1; then j-1 in Seg len H1 by A328,FINSEQ_3:12; then j-1 in dom H1 by FINSEQ_1:def 3; then A331: H.j1 = H1.j1 by FINSEQ_1:def 7; A332: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A281,A288,INTEGRA1:def 4; thus F.j = F1.j by A278,A329,FINSEQ_1:def 7 .= |. vol(divset(H1,j), rho) .| by A329,INTEGR22:def 2 .= |. vol(divset(H,j), rho) .| by A288,A329,A330,A331,A332,INTEGRA1:def 4; end; end; end; end; then reconsider F as var_volume of rho,H by A240,A261,A264,A273,A277,INTEGR22:def 2; take H, F; Z: dom p = dom T by FINSEQ_3:29,A153; A333: for i be Nat st i in dom p holds (i <= len q implies p.i = q.i) & (len q < i implies p.i = 0) proof let i be Nat; assume A334: i in dom p; then A335: 1 <= i <= len p by FINSEQ_3:25; dom p = dom T by A153,FINSEQ_3:29; then A336: p.i = |. vol(divset(T,i) /\ divset(S,(k+1)), rho) .| by A153,A334; thus i <= len q implies p.i = q.i proof assume A337: i <= len q; A338: divset(T,i) = [. lower_bound divset(T,i), upper_bound divset(T,i) .] by INTEGRA1:4; per cases; suppose i <> m; then i < m by A264,A337,XXREAL_0:1; then i+1 <= m by NAT_1:13; then i+1-1 <= m-1 by XREAL_1:13; hence thesis by A267,A335,A336; end; suppose A339: i = m; m-1 < m-0 by XREAL_1:15; then A341: lower_bound(divset(T,m)) = T.(m-1) & upper_bound(divset(T,m)) = T.m by A235,A160,INTEGRA1:def 4; A342: lower_bound(divset(S,k+1)) < lower_bound(divset(T,m)) by A170,A234,A238,A341; divset(T,i) /\ divset(S,(k+1)) = [. lower_bound divset(T,i), upper_bound divset(T,i) .] /\ [. lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)) .] by A338,INTEGRA1:4 .= [. T.m1, upper_bound B .] by A4,A5,A159,A160,A170,A339,A341,A342,XXREAL_1:143; hence thesis by A153,A266,A334,A339,Z; end; end; A343: divset(T,i) = [. lower_bound divset(T,i), upper_bound divset(T,i) .] by INTEGRA1:4; thus len q < i implies p.i = 0 proof assume A344: len q < i; m-1 < m-0 by XREAL_1:15; then A345: 1 < m by A235,XXREAL_0:2; then A346: lower_bound(divset(T,i)) = T.(i-1) & upper_bound(divset(T,i)) = T.i by A264,A344,INTEGRA1:def 4,A334,Z; m+1 <= i by A264,A344,NAT_1:13; then A347: m+1-1 <= i-1 by XREAL_1:13; then A348: 1 < i-1 by A345,XXREAL_0:2; i-1 in NAT by A347,INT_1:3; then reconsider i1 = i-1 as Nat; len T - 1 < len T - 0 by XREAL_1:15; then i1 <= len T by A153,A335,XREAL_1:15; then A350: i1 in dom T by A348,FINSEQ_3:25; divset(T,i) /\ divset(S,(k+1)) c= [.upper_bound(divset(S,k+1)), upper_bound(divset(S,k+1)) .] by A4,A5,A159,A164,A169,A170,A343,A346,A347,A350,Th10; hence thesis by A336,COMPLEX1:44,Th11; end; end; thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74 .= Sum(F) by A272,A264,A153,A160,FINSEQ_3:25,A333,Th9; end; suppose IDX <> {}; then A351: sup IDX in IDX by XXREAL_2:def 6; then reconsider n = sup IDX as Nat; consider i be Nat such that A352: n = i & i in dom T & T.i <= S.k by A351; A353: 1 <= n <= len T by FINSEQ_3:25,A352; n <> len T proof assume n = len T; then A354: upper_bound A <= S.k by A352,INTEGRA1:def 2; upper_bound A < upper_bound B by A168,A354,XXREAL_0:2; hence contradiction by A4,XXREAL_2:59; end; then n < len T by A353,XXREAL_0:1; then Z: 1 <= n+1 <= len T by NAT_1:11,13; then A355: n+1 in dom T by FINSEQ_3:25; A356: S.k < T.(n+1) proof assume T.(n+1) <= S.k; then n+1 in IDX by A355; hence contradiction by NAT_1:16,XXREAL_2:4; end; A357: for i be Nat st i in dom T & n < i holds S.k < T.i proof let i be Nat; assume A358: i in dom T & n < i; then A359: n+1 <= i by NAT_1:13; n+1 in dom T by Z,FINSEQ_3:25; then T.(n+1) <= T.i by A358,A359,VALUED_0:def 15; hence S.k < T.i by A356,XXREAL_0:2; end; A361: n < m proof assume m <= n; then T.m <= T.n by A160,A352,VALUED_0:def 15; then upper_bound B <= T.n by A160,XXREAL_0:2; hence contradiction by A168,A352,XXREAL_0:2; end; A364: for i be Nat st i<=n & i in dom T holds T.i <= S.k proof let i be Nat; assume A365: i <= n & i in dom T; assume A366: not T.i <= S.k; T.i <= T.n by A352,A365,VALUED_0:def 15; hence contradiction by A352,A366,XXREAL_0:2; end; A368: for i be Nat st n; H1.(len H1) = S.k by A126,INTEGRA1:def 2; then reconsider H as non empty increasing FinSequence of REAL by A168,Th14; A372: len <* upper_bound B *> = 1 by FINSEQ_1:39; then A373: len H = (len H1) + 1 by FINSEQ_1:22; A374: H.(len H) = upper_bound B by A373,FINSEQ_1:42; rng H1 c= B1 by INTEGRA1:def 2; then A375: rng H1 c= B by A123; A376: rng H = rng H1 \/ rng <* upper_bound B *> by FINSEQ_1:31; A377: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39; lower_bound B <= upper_bound B by SEQ_4:11; then upper_bound B in B by A115; then rng <* upper_bound B *> c= B by A377,ZFMISC_1:31; then reconsider H as Division of B by A374,A375,A376,INTEGRA1:def 2,XBOOLE_1:8; set F = F1 ^ <* |. vol([. S.k, upper_bound B .], rho) .| *>; |. vol([.S.k,upper_bound B.], rho) .| is Element of REAL by XREAL_0:def 1; then A378: <* |. vol([. S.k, upper_bound B .], rho) .| *> is FinSequence of REAL by FINSEQ_1:74; reconsider F as FinSequence of REAL by A378,FINSEQ_1:75; A379: len F = len F1 + len <* |. vol([.S.k,upper_bound B.], rho) .| *> by FINSEQ_1:22 .= len H1 + len <* |. vol([.S.k,upper_bound B.], rho) .| *> by INTEGR22:def 2 .= len H1 + 1 by FINSEQ_1:40 .= len H by A372,FINSEQ_1:22; D: 1 <= len H1 by NAT_1:14; then A380: 1 in dom H1 by FINSEQ_3:25; A381: len F1 = len H1 by INTEGR22:def 2; then A382: dom F1 = dom H1 by FINSEQ_3:29; for j be Nat st j in dom H holds F.j = |. vol(divset(H,j), rho) .| proof let j be Nat; A383: divset(H,j) = [. lower_bound divset(H,j), upper_bound divset(H,j) .] & divset(H1,j) = [. lower_bound divset(H1,j), upper_bound divset(H1,j) .] by INTEGRA1:4; assume A384: j in dom H; then A385: 1 <= j <= len H by FINSEQ_3:25; per cases; suppose A386: j = 1; then A387: lower_bound divset(H,j) = lower_bound B & upper_bound divset(H,j) = H.j by A384,INTEGRA1:def 4; A388: j in dom H1 by D,A386,FINSEQ_3:25; A389: lower_bound divset(H1,j) = lower_bound B1 & upper_bound divset(H1,j) = H1.j by INTEGRA1:def 4,A380,A386; A390: lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5; thus F.j = F1.j by A382,A388,FINSEQ_1:def 7 .= |. vol (divset(H1,j),rho) .| by A388,INTEGR22:def 2 .= |. vol (divset(H,j),rho) .| by A383,A387,A388,A389,A390,FINSEQ_1:def 7; end; suppose A391: j <> 1; per cases; suppose A392: j = len H; A393: F.j = |. vol([.S.k,upper_bound B.], rho) .| by A373,A381,A392,FINSEQ_1:42; A394: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A384,A391,INTEGRA1:def 4; j-1 in NAT by A384,INT_1:5,FINSEQ_3:25; then reconsider j1 = j-1 as Nat; 1 < j by A385,A391,XXREAL_0:1; then 1-1 < j1 by XREAL_1:14; then 1 <= j1 by NAT_1:14; then j1 in dom H1 by FINSEQ_3:25,A373,A392; then H.(j-1) = H1.(len H1) by A373,A392,FINSEQ_1:def 7 .= S.k by A126,INTEGRA1:def 2; hence F.j = |. vol (divset(H,j), rho) .| by A383,A392,A393,A394,INTEGRA1:def 2; end; suppose j <> len H; then j < len H1 + 1 by A373,A385,XXREAL_0:1; then K: j <= len H1 by NAT_1:13; then A396: j in Seg len H1 by A385; A397: j in dom H1 by FINSEQ_3:25,K,A385; then A398: H.j = H1.j by FINSEQ_1:def 7; j-1 in NAT by A384,FINSEQ_3:25,INT_1:5; then reconsider j1 = j-1 as Nat; 1 < j by A385,A391,XXREAL_0:1; then j-1 in Seg len H1 by A396,FINSEQ_3:12; then j-1 in dom H1 by FINSEQ_1:def 3; then A399: H.j1 = H1.j1 by FINSEQ_1:def 7; A400: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A384,A391,INTEGRA1:def 4; thus F.j = F1.j by A382,A397,FINSEQ_1:def 7 .= |. vol(divset(H1,j), rho) .| by A397,INTEGR22:def 2 .= |. vol(divset(H,j), rho) .| by A391,A397,A398,A399,A400,INTEGRA1:def 4; end; end; end; then reconsider F as var_volume of rho,H by A379,INTEGR22:def 2; take H, F; A401: 1 < 1+n by A353,NAT_1:16; A403: p.m = |. vol(divset(T,m) /\ divset(S,k+1), rho) .| by A153,A160; A405: lower_bound divset(T,m) = T.m1 & upper_bound divset(T,m) = T.m by A160,A371,A401,INTEGRA1:def 4; [. lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)) .] c= [. lower_bound divset(T,m), upper_bound divset(T,m) .] by A160,A170,A171,A352,A371,A405,XXREAL_1:34; then divset(S,k+1) c= divset(T,m) by A169,INTEGRA1:4; then A406: p.m = |. vol (divset(S,k+1), rho) .| by A403,XBOOLE_1:28; for i be Nat st i in dom p & i <> m holds p.i = 0 proof let i be Nat; assume A407: i in dom p & i <> m; then A408: i in Seg len p by FINSEQ_1:def 3; A409: 1 <= i <= len p by A407,FINSEQ_3:25; per cases by A407,XXREAL_0:1; suppose A410: i < m; A412: i in dom T by A153,A408,FINSEQ_1:def 3; A413: upper_bound divset(T,i) = T.i proof per cases; suppose i = 1; hence upper_bound divset(T,i) = T.i by A412,INTEGRA1:def 4; end; suppose i <> 1; hence upper_bound divset(T,i) = T.i by A412,INTEGRA1:def 4; end; end; A414: i+1-1 <= n+1-1 by A371,A410,NAT_1:13; A415: divset(T,i) /\ divset(S,k+1) = [. lower_bound(divset(T,i)), upper_bound(divset(T,i)) .] /\ [. lower_bound(divset(S,k+1)), upper_bound(divset(S,k+1)) .] by A169,INTEGRA1:4; divset(T,i) /\ divset(S,k+1) c= [. upper_bound(divset(T,i)), upper_bound(divset(T,i)) .] by H,A170,A364,A407,A413,A414,A415,Th10; then vol(divset(T,i) /\ divset(S,k+1),rho) = 0 by Th11; hence thesis by A153,COMPLEX1:44,A412; end; suppose A416: m < i; then A417: 1 < i by A353,A371,NAT_1:16,XXREAL_0:2; a418: i in dom T by A153,A408,FINSEQ_1:def 3; then A419: lower_bound divset(T,i) = T.(i-1) & upper_bound divset(T,i) = T.i by A371,A401,A416,INTEGRA1:def 4; m+1 <= i by A416,NAT_1:13; then A420: m+1-1 <= i-1 by XREAL_1:9; 1+1 <= i by A417,NAT_1:13; then A421: 2-1 <= i-1 by XREAL_1:9; then reconsider i1 = i-1 as Nat by INT_1:3,ORDINAL1:def 12; i-1 <= len p - 0 by A409,XREAL_1:13; then i1 in dom T by A153,FINSEQ_3:25,A421; then A422: T.m <= T.i1 by A160,A420,VALUED_0:def 15; divset(T,i) /\ divset(S,k+1) = [. lower_bound(divset(T,i)), upper_bound(divset(T,i)) .] /\ [. lower_bound(divset(S,k+1)), upper_bound(divset(S,k+1)) .] by A169,INTEGRA1:4; then divset(T,i) /\ divset(S,k+1) c= [. upper_bound(divset(S,k+1)), upper_bound(divset(S,k+1)) .] by A160,A170,A171,A419,A422,Th10,XXREAL_0:2; then vol(divset(T,i) /\ divset(S,k+1), rho) = 0 by Th11; hence thesis by A153,a418,COMPLEX1:44; end; end; then A423: Sum p = |. vol(divset(S,k+1), rho) .| by A160,H,A406,Th8 .= |. vol([.S.k,upper_bound B.], rho) .| by A4,A5,A159,A170,INTEGRA1:4; thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74 .= Sum(F) by A423,RVSUM_1:74; end; suppose A424: n+1 <> m; then A425: n+1 < m by A370,XXREAL_0:1; m-(n+1) in NAT by A370,INT_1:5; then reconsider mn1 = m-(n+1) as Nat; m-n in NAT by A361,INT_1:5; then reconsider mn = m-n as Nat; A426: 0+1 <= mn1 by A425,NAT_1:13,XREAL_1:50; m-n-1 <= mn-0 by XREAL_1:13; then A427: 1 <= mn by A426,XXREAL_0:2; consider TM1 be non empty increasing FinSequence of REAL such that A428: len TM1 = mn1 & rng TM1 c= rng T & for i be Nat st i in dom TM1 holds TM1.i = T.(i+n) by A233,A425,Th16; consider pM1 be FinSequence of REAL such that A429: len pM1 = mn1-1 & rng pM1 c= rng p & for i be Nat st i in dom pM1 holds pM1.i = p.(i+n+1) by A153,A233,A425,Th17; reconsider m1 = m-1 as Nat by a234; A430: TM1.(len TM1) = T.(mn1+n) by FINSEQ_3:25,A426,A428; A431: T.(mn1+n) < upper_bound B proof assume A432: not T.(mn1+n) < upper_bound B; A433: (mn1+n) in JDX by A234,A432; m-1 < m-0 by XREAL_1:15; hence contradiction by A433,NAT_1:def 1; end; then reconsider TM1B = TM1 ^ <* upper_bound B *> as non empty increasing FinSequence of REAL by A430,Th14; A434: H1.(len H1) = S.k by A126,INTEGRA1:def 2; KK: 1 in dom TM1 by A426,A428,FINSEQ_3:25; A436: TM1.1 = T.(1+n) by A428,A426,FINSEQ_3:25; A437: TM1B.1 = T.(1+n) by A436,FINSEQ_1:def 7,KK; reconsider H = H1 ^TM1B as non empty increasing FinSequence of REAL by A356,A434,A437,Th13; A438: rng TM1B = rng TM1 \/ rng <* upper_bound B *> by FINSEQ_1:31; A439: rng <* upper_bound B *> = { upper_bound B } by FINSEQ_1:39; A444: rng TM1 c= B proof let z be object; assume A440: z in rng TM1; then reconsider x = z as Real; x in A by A428,A440,INTEGRA1:def 2,TARSKI:def 3; then A441: ex r be Real st x = r & lower_bound A <= r & r <= upper_bound A by A116; consider i be object such that A442: i in dom TM1 & x = TM1.i by A440,FUNCT_1:def 3; reconsider i as Nat by A442; A443: 1 <= i <= len TM1 by A442,FINSEQ_3:25; 1 <= len TM1 <= len TM1 by A443,XXREAL_0:2; then len TM1 in dom TM1 by FINSEQ_3:25; then TM1.i <= TM1.(len TM1) by A442,A443,VALUED_0:def 15; then x <= upper_bound B by A430,A431,A442,XXREAL_0:2; hence z in B by A4,A115,A441; end; lower_bound B <= upper_bound B by SEQ_4:11; then upper_bound B in B by A115; then { upper_bound B } c= B by ZFMISC_1:31; then A445: rng TM1B c= B by A438,A439,A444,XBOOLE_1:8; rng H1 c= B1 by INTEGRA1:def 2; then rng H1 c= B by A123; then rng H1 \/ rng TM1B c= B by A445,XBOOLE_1:8; then A446: rng H c= B by FINSEQ_1:31; A447: len TM1B = len TM1 + len <* upper_bound B *> by FINSEQ_1:22 .= len TM1 + 1 by FINSEQ_1:40; len TM1 + 1 in Seg(len TM1 + 1) by FINSEQ_1:4; then A448: len TM1 + 1 in dom TM1B by A447,FINSEQ_1:def 3; A449: len H = len H1 + (len TM1 + 1) by A447,FINSEQ_1:22; G: 1 in Seg 1; then A450: 1 in dom <* upper_bound B *> by FINSEQ_1:38; H.(len H) = TM1B.(len TM1 + 1) by A448,A449,FINSEQ_1:def 7 .= (<* upper_bound B *>).1 by A450,FINSEQ_1:def 7 .= upper_bound B by FINSEQ_1:40; then reconsider H as Division of B by A446,INTEGRA1:def 2; set q1 = <* |. vol([. S.k, T.(n+1) .], rho) .| *> ^ pM1; set q = q1 ^ <* |. vol([. T.m1,upper_bound B .], rho) .| *>; rng q1 c= REAL; then reconsider q1 as FinSequence of REAL by FINSEQ_1:def 4; rng q c= REAL; then reconsider q as FinSequence of REAL by FINSEQ_1:def 4; A451: len q1 = len(<* |. vol([. S.k, T.(n+1) .], rho) .| *>) + len pM1 by FINSEQ_1:22 .= 1 + (mn1-1) by A429,FINSEQ_1:40 .= mn1; A452: len q = len q1 + len <* |. vol([. T.m1, upper_bound B .], rho) .| *> by FINSEQ_1:22 .= mn1+ 1 by A451,FINSEQ_1:40 .= mn; A453: 1 in dom <* |. vol([. T.m1,upper_bound B .], rho) .| *> by G,FINSEQ_1:38; A454: q.(len q) = q.(mn1+1) by A452 .= ( <* |. vol([. T.m1,upper_bound B .], rho) .| *>).1 by A451,A453,FINSEQ_1:def 7 .= |. vol([. T.m1,upper_bound B .], rho) .| by FINSEQ_1:40; A455: 1 in dom <* |. vol([. S.k,T.(n+1) .], rho) .| *> by FINSEQ_1:38,G; 1 in Seg mn1 by A426; then 1 in dom q1 by A451,FINSEQ_1:def 3; then A456: q.1 = q1.1 by FINSEQ_1:def 7 .= (<* |. vol([. S.k,T.(n+1) .], rho) .| *>).1 by A455,FINSEQ_1:def 7 .= |. vol([. S.k,T.(n+1) .], rho) .| by FINSEQ_1:40; A457: for i be Nat st 2 <= i & i <= len q1 holds q.i = |. vol(divset(T,n+i) /\ divset(S,(k+1)), rho) .| proof let i be Nat; assume A458: 2 <= i & i <= len q1; then A459: 1 <= i by XXREAL_0:2; then i in dom q1 by A458,FINSEQ_3:25; then A460: q.i = q1.i by FINSEQ_1:def 7; A461: 2-1 <= i-1 by A458,XREAL_1:9; then A462: 1 <= i-1 & i-1 <= mn1-1 by A451,A458,XREAL_1:9; i-1 in NAT by A461,INT_1:3; then reconsider i1 = i-1 as Nat; A463: len(<* |. vol([. S.k, T.(n+1) .], rho) .| *>) = 1 by FINSEQ_1:40; A465: i1 in dom pM1 by FINSEQ_3:25,A429,A462; A466: q1.i = q1.(1+i1) .= pM1.i1 by A463,A465,FINSEQ_1:def 7 .= p.(i1+n+1) by FINSEQ_3:25,A429,A462 .= p.(i+n); i <= i+n by NAT_1:11; then A467: 1 <= i+n by A459,XXREAL_0:2; i+n <= m-n-1+n by A451,A458,XREAL_1:6; then i+n <= len T by A235,XXREAL_0:2; hence thesis by A153,A460,A466,FINSEQ_3:25,A467; end; reconsider F = F1^q as FinSequence of REAL; A468: len F = len F1 + len q by FINSEQ_1:22; E: 1 <= len H1 by NAT_1:14; then A469: 1 in dom H1 by FINSEQ_3:25; A470: len F1 = len H1 by INTEGR22:def 2; then A471: dom F1 = dom H1 by FINSEQ_3:29; mn in Seg (mn) by A427; then A472: mn in dom q by A452,FINSEQ_1:def 3; 1<= len q by NAT_1:14; then A473: 1 in dom q by FINSEQ_3:25; 1 <= len TM1B by NAT_1:14; then A474: 1 in dom TM1B by FINSEQ_3:25; 1 <= len TM1 by NAT_1:14; then A475: 1 in dom TM1 by FINSEQ_3:25; A476: H.(len H1 +1) = TM1B.1 by A474,FINSEQ_1:def 7 .= TM1.1 by A475,FINSEQ_1:def 7 .= T.(n+1) by A428,A426,FINSEQ_3:25; for j be Nat st j in dom H holds F.j = |. vol (divset(H,j),rho) .| proof let j be Nat; A477: divset(H,j) = [. lower_bound divset(H,j), upper_bound divset(H,j) .] & divset(H1,j) = [. lower_bound divset(H1,j), upper_bound divset(H1,j) .] by INTEGRA1:4; assume A478: j in dom H; then A479: 1 <= j <= len H by FINSEQ_3:25; per cases; suppose A480: j = 1; then A481: lower_bound divset(H,j) = lower_bound B & upper_bound divset(H,j) = H.j by A478,INTEGRA1:def 4; A482: j in dom H1 by E,A480,FINSEQ_3:25; A483: lower_bound divset(H1,j) = lower_bound B1 & upper_bound divset(H1,j) = H1.j by A469,A480,INTEGRA1:def 4; A484: lower_bound B = lower_bound B1 by A122,A137,INTEGRA1:5; thus F.j = F1.j by A471,A482,FINSEQ_1:def 7 .= |. vol(divset(H1,j), rho) .| by A482,INTEGR22:def 2 .= |. vol(divset(H,j), rho) .| by A477,A481,A482,A483,A484,FINSEQ_1:def 7; end; suppose A485: j <> 1; per cases; suppose A486: j = len H; then A487: j = len H1 + mn1 + 1 by A428,A449; A488: F.j = |. vol( [. T.m1,upper_bound B .], rho) .| by A428,A449,A452,A454,A470,A472,A486,FINSEQ_1:def 7; A489: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A478,A485,INTEGRA1:def 4; j-1 in NAT by A478,INT_1:5,FINSEQ_3:25; then reconsider j1 = j-1 as Nat; mn-1 < mn-0 by XREAL_1:15; then mn1 in Seg mn by A426; then A490: mn1 in dom TM1B by A428,A447,FINSEQ_1:def 3; len TM1 in Seg len TM1 by FINSEQ_1:3; then A491: mn1 in dom TM1 by A428,FINSEQ_1:def 3; H.j1 = TM1B.mn1 by A487,A490,FINSEQ_1:def 7 .= T.m1 by A428,A430,A491,FINSEQ_1:def 7; hence F.j = |. vol(divset(H,j), rho) .| by A477,A486,A488,A489,INTEGRA1:def 2; end; suppose j <> len H; then A492: j < len H1 + mn1 + 1 by A428,A449,A479,XXREAL_0:1; per cases; suppose j > len H1; then A493: j - len H1 > 0 by XREAL_1:50; then j- len H1 in NAT by INT_1:3; then reconsider j1 = j - len H1 as Nat; A494: j1 < len H1 + mn - len H1 by A492,XREAL_1:14; then j1 + 1 <= mn by NAT_1:13; then A495: j1 + 1 - 1 <= mn - 1 by XREAL_1:13; A496: 1 <= j1 by A493,NAT_1:14; then A497: j1 in Seg mn by A494; then A498: j1 in dom q by A452,FINSEQ_1:def 3; 1 <= j1 <= mn1 by A493,A495,NAT_1:14; then j1 in Seg mn1; then A500: j1 in dom TM1 by A428,FINSEQ_1:def 3; A501: j1 in dom TM1B by A428,A447,A497,FINSEQ_1:def 3; A502: H.j = H.(len H1 + j1) .= TM1B.j1 by A501,FINSEQ_1:def 7 .= TM1.j1 by A500,FINSEQ_1:def 7 .= T.(j1+n) by A428,A500; A503: j1 +n <= mn1+n by A495,XREAL_1:6; A504: 1 <= j1+n by A493,NAT_1:14; j1+n <= len T by A235,A503,XXREAL_0:2; then A505: j1+n in dom T by A504,FINSEQ_3:25; then T.(j1+n) <= T.(mn1+n) by A234,A503,VALUED_0:def 15; then A506: T.(j1+n) <= upper_bound divset(S,(k+1)) by A4,A5,A159,A170,A431,XXREAL_0:2; per cases; suppose A507: j1 = 1; 0 < len H1; then 1 + 0 < 1 + len H1 by XREAL_1:8; then A508: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A478,A507,INTEGRA1:def 4; len H1 in Seg len H1 by FINSEQ_1:3; then A509: len H1 in dom H1 by FINSEQ_1:def 3; A510: F.j = F.(len H1 + 1) by A507 .= |. vol( [. S.k,T.(n+1) .], rho) .| by A456,A470,A473,FINSEQ_1:def 7; H.(len H1) = S.k by A434,A509,FINSEQ_1:def 7; hence F.j = |. vol(divset(H,j), rho) .| by A476,A507,A508,A510,INTEGRA1:4; end; suppose j1 <> 1; then A511: 1 < j1 by A496,XXREAL_0:1; then A512: 1+1 <= j1 by NAT_1:13; A513: F.j = F.(len H1 + j1) .= q.j1 by A470,A498,FINSEQ_1:def 7 .= |. vol(divset(T,j1+n) /\ divset(S,(k+1)),rho) .| by A451,A457,A495,A512; A514: j1 + n <> 1 by A511,NAT_1:11; then 1 < j1+n by A504,XXREAL_0:1; then 1+1 <= j1+n by NAT_1:13; then A515: 1+1 -1 <= j1+n -1 by XREAL_1:9; then j1+n-1 in NAT by INT_1:3; then reconsider j11=j1+n-1 as Nat; 2+(n-1) <= j1+(n-1) by A512,XREAL_1:6; then n+1 <= j11; then A516: n < j11 by NAT_1:16,XXREAL_0:2; A517: j1 + (n-1) <= m-n-1 + (n-1) by A495,XREAL_1:6; m1-1 <= m1-0 by XREAL_1:13; then A518: j11 <= m1 by A517,XXREAL_0:2; j11 <= len T by A235,A518,XXREAL_0:2; then j11 in dom T by FINSEQ_3:25,A515; then A519: S.k < T.j11 by A357,A516; A520: lower_bound(divset(S,k+1)) <= lower_bound(divset(T,j1+n)) by A170,A505,A514,A519,INTEGRA1:def 4; A521: upper_bound(divset(T,j1+n)) <= upper_bound divset(S,(k+1)) by A505,A506,A514,INTEGRA1:def 4; A522: divset(T,j1+n) = [. lower_bound divset(T,j1+n), upper_bound divset(T,j1+n) .] by INTEGRA1:4; A523: divset(T,j1+n) /\ divset(S,(k+1)) = divset(T,j1+n) by A169,A520,A521,A522,XBOOLE_1:28,XXREAL_1:34; j1-1 <= j1-0 by XREAL_1:13; then A524: j11-n <= mn1 by A495,XXREAL_0:2; A525: 2-1 <= j1-1 by A512,XREAL_1:9; then j11-n in NAT by INT_1:3; then reconsider j11n = j11-n as Nat; j11n in Seg mn1 by A524,A525; then A527: j11-n in dom TM1 by A428,FINSEQ_1:def 3; mn-1 <= mn-0 by XREAL_1:13; then 1 <= j11-n & j11-n <= mn by A524,A525,XXREAL_0:2; then j11n in Seg mn; then A528: j11-n in dom TM1B by A428,A447,FINSEQ_1:def 3; A529: H.(j-1) = H.(len H1 + (j11-n)) .= TM1B.(j11-n) by A528,FINSEQ_1:def 7 .= TM1.(j11-n) by A527,FINSEQ_1:def 7 .= T.(j1-1+n) by A428,A527; A530: upper_bound divset(H,j) = T.(j1+n) by A478,A485,A502,INTEGRA1:def 4 .= upper_bound divset(T,j1+n) by A505,A514,INTEGRA1:def 4; lower_bound divset(H,j) = T.(j1+n-1) by A478,A485,A529,INTEGRA1:def 4 .= lower_bound divset(T,j1+n) by A505,A514,INTEGRA1:def 4; hence F.j = |. vol(divset(H,j),rho) .| by A513,A522,A523,A530,INTEGRA1:4; end; end; suppose j <= len H1; then A531: j in Seg len H1 by A479; then A532: j in dom H1 by FINSEQ_1:def 3; then A533: H.j =H1.j by FINSEQ_1:def 7; j-1 in NAT by A478,INT_1:5,FINSEQ_3:25; then reconsider j1 = j-1 as Nat; 1 < j by A479,A485,XXREAL_0:1; then j-1 in Seg(len H1) by A531,FINSEQ_3:12; then j-1 in dom H1 by FINSEQ_1:def 3; then A534: H.j1 = H1.j1 by FINSEQ_1:def 7; A535: lower_bound divset(H,j) = H.(j-1) & upper_bound divset(H,j) = H.j by A478,A485,INTEGRA1:def 4; thus F.j = F1.j by A471,A532,FINSEQ_1:def 7 .= |. vol(divset(H1,j),rho) .| by A532,INTEGR22:def 2 .= |. vol(divset(H,j),rho) .| by A485,A532,A533,A534,A535,INTEGRA1:def 4; end; end; end; end; then reconsider F as var_volume of rho,H by A428,A449,A452,A468,A470,INTEGR22:def 2; take H,F; A536: for i be Nat st i in dom p holds (i <= n implies p.i = 0) & (i <= len q implies p.(n+i) = q.i) & (len q + n < i implies p.i = 0) proof let i be Nat; assume A537: i in dom p; then A538: 1<=i & i <= len p by FINSEQ_3:25; F: dom p = dom T by A153,FINSEQ_3:29; then A539: p.i = |. vol(divset(T,i) /\ divset(S,(k+1)),rho) .| by A153,A537; thus i <= n implies p.i = 0 proof assume A540: i <= n; per cases; suppose i = 1; then A542: lower_bound(divset(T,i)) = lower_bound A & upper_bound(divset(T,i)) = T.i by INTEGRA1:def 4,F,A537; divset(T,i) /\ divset(S,(k+1)) = [. lower_bound divset(T,i), upper_bound divset(T,i) .] /\ [. lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)) .] by A169,INTEGRA1:4; then divset(T,i) /\ divset(S,(k+1)) c= [.upper_bound divset(T,i),upper_bound divset(T,i) .] by A170,A364,A537,A540,F,A542,Th10; hence thesis by A539,COMPLEX1:44,Th11; end; suppose A543: i <> 1; then 1 < i by A538,XXREAL_0:1; then 1+1 <= i by NAT_1:13; then 1+1-1 <= i-1 by XREAL_1:13; then i-1 in NAT by INT_1:3; then reconsider i1 = i-1 as Nat; A544: lower_bound(divset(T,i)) = T.(i-1) & upper_bound(divset(T,i)) = T.i by A543,INTEGRA1:def 4,A537,F; divset(T,i) /\ divset(S,(k+1)) = [. lower_bound divset(T,i), upper_bound divset(T,i) .] /\ [. lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)) .] by A169,INTEGRA1:4; then divset(T,i) /\ divset(S,(k+1)) c= [.upper_bound divset(T,i), upper_bound divset(T,i) .] by A170,A364,A537,A540,A544,F,Th10; hence thesis by A539,COMPLEX1:44,Th11; end; end; thus i <= len q implies p.(n+i) = q.i proof assume A545: i <= len q; per cases; suppose A546: i = 1; A547: divset(T,n+1) = [. lower_bound divset(T,n+1), upper_bound divset(T,n+1) .] by INTEGRA1:4; n <> 0 by FINSEQ_3:25,A352; then A548: n+1 <> 1; A549: lower_bound(divset(T,n+1)) = T.(n+1-1) & upper_bound(divset(T,n+1)) = T.(n+1) by A548,A355,INTEGRA1:def 4; n < n+1 & n+1 < m by A370,A424,NAT_1:16,XXREAL_0:1; then A550: T.(n+1) < S.(k+1) by A355,A368; divset(T,n+1) /\ divset(S,(k+1)) = [. S.k, T.(n+1) .] by A169,A170,A352,A547,A549,A550,XXREAL_1:143; hence p.(n+i) = q.i by A153,Z,A456,A546,FINSEQ_3:25; end; suppose i <> 1; then 1 < i by A538,XXREAL_0:1; then A551: 1+1 <= i by NAT_1:13; per cases; suppose i <> mn; then i < mn by A452,A545,XXREAL_0:1; then i+1 <= mn by NAT_1:13; then i+1-1 <= mn-1 by XREAL_1:9; then A552: q.i = |. vol(divset(T,n+i) /\ divset(S,(k+1)),rho) .| by A451,A457,A551; i+n <= m-n+n by A452,A545,XREAL_1:7; then A553: i+n <= len T by A233,XXREAL_0:2; 1+0 <= i+n by A538,XREAL_1:7; then n+i in Seg len T by A553; then n+i in dom T by FINSEQ_1:def 3; hence p.(n+i)=q.i by A153,A552; end; suppose A554: i = mn; 1 <= n+1 by NAT_1:11; then A556: lower_bound(divset(T,m)) = T.(m-1) & upper_bound(divset(T,m)) = T.m by A425,A160,INTEGRA1:def 4; A557: m-1 < m-0 by XREAL_1:15; n+1-1 < m-1 by A425,XREAL_1:14; then A558: S.k < T.m1 < S.(k+1) by A234,A368,A557; divset(T,m) /\ divset(S,(k+1)) = [.lower_bound(divset(T,m)), upper_bound(divset(T,m)) .] /\ [.lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)).] by A169,INTEGRA1:4 .= [. T.m1,upper_bound B .] by A4,A5,A159,A160,A170,A556,A558,XXREAL_1:143; hence p.(n+i) = q.i by A153,A160,A452,A454,A554; end; end; end; thus len q + n < i implies p.i = 0 proof assume A559: len q + n < i; m-1 < m-0 by XREAL_1:15; then A560: 1 < m by A235,XXREAL_0:2; A561: lower_bound(divset(T,i)) = T.(i-1) & upper_bound(divset(T,i)) = T.i by A452,A559,A560,INTEGRA1:def 4,A537,F; m+1 <= i by A452,A559,NAT_1:13; then A562: m+1-1 <= i-1 by XREAL_1:13; then A563: 1 < i-1 by A560,XXREAL_0:2; i-1 in NAT by A562,INT_1:3; then reconsider i1 = i-1 as Nat; len T - 1 < len T - 0 by XREAL_1:15; then A565: i1 in dom T by A563,FINSEQ_3:25,A153,A538,XREAL_1:13; divset(T,i) /\ divset(S,(k+1)) = [. lower_bound divset(T,i), upper_bound divset(T,i) .] /\ [. lower_bound divset(S,(k+1)), upper_bound divset(S,(k+1)) .] by A169,INTEGRA1:4; then divset(T,i) /\ divset(S,(k+1)) c= [.upper_bound(divset(S,k+1)), upper_bound(divset(S,k+1)) .] by A4,A5,A159,A164,A170,A561,A562,A565,Th10; hence thesis by A539,COMPLEX1:44,Th11; end; end; len p - (len q + n) in NAT by A153,A233,A452,INT_1:5; then reconsider L = len p - (len q + n) as Nat; set s = (n |-> (0 qua Real)) ^ q ^ ( L |-> (0 qua Real)); reconsider nn = n, nL = L as Element of NAT by ORDINAL1:def 12; reconsider z0 = (0 qua Real) as Element of REAL by XREAL_0:def 1; A566: len(n |-> (0 qua Real)) = len(nn |-> z0) .= n by FINSEQ_2:133; A567: len(L |-> (0 qua Real)) = len(nL |-> z0) .= L by FINSEQ_2:133; A568: len s = len((n |-> (0 qua Real)) ^q) + len(L |-> (0 qua Real)) by FINSEQ_1:22 .= n + len q + L by A566,A567,FINSEQ_1:22 .= len p; for j be Nat st 1 <= j & j <= len p holds p.j = s.j proof let j be Nat; assume A569: 1 <= j <= len p; then A570: j in dom p by FINSEQ_3:25; set sw = (n |-> (0 qua Real)) ^ q; A571: len sw = n + len q by A566,FINSEQ_1:22; per cases; suppose A572: j <= n; then A573: p.j = 0 by A536,A570; j <= n + len q by A572,NAT_1:12; then j in Seg len(sw) by A569,A571; then j in dom sw by FINSEQ_1:def 3; then A574: s.j = sw.j by FINSEQ_1:def 7; j in Seg len(n |-> (0 qua Real)) by A566,A569,A572; then j in dom(n |-> (0 qua Real)) by FINSEQ_1:def 3; then A575: sw.j = (n |-> (0 qua Real)).j by FINSEQ_1:def 7; j in Seg n by A569,A572; hence p.j = s.j by A573,A574,A575,FINSEQ_2:57; end; suppose A576: n < j; per cases; suppose A577: j <= len q + n; j - n in NAT by A576,INT_1:5; then reconsider jn = j-n as Nat; A578: 0+1 <= jn by A576,NAT_1:13,XREAL_1:50; A579: j - n <= len q + n - n by A577,XREAL_1:9; then A580: jn in dom q by A578,FINSEQ_3:25; len q <= len q + n by NAT_1:11; then len q <= len p by A153,A233,A452,XXREAL_0:2; then jn <= len p by A579,XXREAL_0:2; then jn in dom p by FINSEQ_3:25,A578; then A581: p.(n+jn)=q.jn by A536,A579; A582: j in dom sw by A569,A571,A577,FINSEQ_3:25; s.j = sw.(n+jn) by A582,FINSEQ_1:def 7 .= q.jn by A566,A580,FINSEQ_1:def 7; hence p.j = s.j by A581; end; suppose A583: len q + n < j; j - (len q + n) in NAT by A583,INT_1:5; then reconsider j1 = j - (len q + n) as Nat; A584: 0+1 <= j1 by A583,NAT_1:13,XREAL_1:50; j - (len q + n) <= len p - (len q + n) by A569,XREAL_1:9; then A585: j1 in Seg L by A584; then A586: j1 in dom(L |-> (0 qua Real)) by A567,FINSEQ_1:def 3; s.j = s.(len sw + j1) by A571 .= ( L |-> (0 qua Real) ).j1 by A586,FINSEQ_1:def 7 .= 0 by A585,FINSEQ_2:57; hence p.j = s.j by A536,A570,A583; end; end; end; then A587: p = s by A568; A588: Sum p = Sum(( n |-> (0 qua Real)) ^ q) + Sum( L |-> (0 qua Real)) by A587,RVSUM_1:75 .= Sum(( n |-> (0 qua Real))) + Sum q + Sum(L |-> (0 qua Real)) by RVSUM_1:75 .= 0 + Sum q +Sum(L |-> (0 qua Real)) by RVSUM_1:81 .= 0 + Sum q by RVSUM_1:81; thus Sum ST = Sum(F1) + Sum p by A150,A152,A153,RVSUM_1:74 .= Sum(F) by A588,RVSUM_1:75; end; end; end; end; end; for k be Nat holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; Lm2: for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, T,S be Division of A, ST be FinSequence of REAL st rho is bounded_variation & len ST = len S & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .| holds ex H be Division of A, F be var_volume of rho,H st Sum ST = Sum(F) proof let A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, T,S be Division of A, ST be FinSequence of REAL; assume A1: rho is bounded_variation & len ST = len S & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .|; A c= A & lower_bound A = lower_bound A; hence thesis by A1,Th18; end; theorem Th19: for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, T,S be Division of A st rho is bounded_variation holds ex ST be FinSequence of REAL st len ST = len S & Sum ST <= total_vd(rho) & for j be Nat st j in dom S holds ex p be FinSequence of REAL st ST.j = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .| proof let A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, T,S be Division of A; assume A1: rho is bounded_variation; defpred P[Nat,object] means ex p be FinSequence of REAL st $2 = Sum p & len p = len T & for i be Nat st i in dom T holds p.i = |. vol(divset(T,i) /\ divset(S,$1),rho) .|; A2: for j be Nat st j in Seg len S holds ex x be Element of REAL st P[j,x] proof let j be Nat; assume j in Seg len S; defpred Q[Nat,object] means $2= |. vol (divset(T,$1) /\ divset(S,j),rho) .|; A3: for i be Nat st i in Seg len T holds ex y be Element of REAL st Q[i,y] proof let i be Nat; assume i in Seg len T; |. vol (divset(T,i) /\ divset(S,j),rho) .| in REAL by XREAL_0:def 1; hence thesis; end; consider p be FinSequence of REAL such that A4: dom p = Seg len T & for i be Nat st i in Seg len T holds Q[i,p.i] from FINSEQ_1:sch 5(A3); reconsider x = Sum p as Element of REAL by XREAL_0:def 1; Z2: dom T = Seg len T by FINSEQ_1:def 3; len p = len T by A4,FINSEQ_1:def 3; then P[j,x] by A4,Z2; hence ex x be Element of REAL st P[j,x]; end; consider ST be FinSequence of REAL such that A5: dom ST = Seg len S & for j be Nat st j in Seg len S holds P[j,ST.j] from FINSEQ_1:sch 5(A2); take ST; thus A6: len ST = len S by A5,FINSEQ_1:def 3; a6: dom ST = dom S by A5,FINSEQ_1:def 3; then consider H be Division of A, F be var_volume of rho,H such that A7: Sum ST = Sum(F) by A1,A5,A6,Lm2; thus thesis by A1,A5,A7,INTEGR22:5,a6; end; theorem Th20: for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, u be PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u|A is uniformly_continuous holds for T being DivSequence of A, S be middle_volume_Sequence of rho,u,T st delta T is convergent & lim delta T = 0 holds middle_sum(S) is convergent proof let A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, u be PartFunc of REAL,REAL; assume that A1: rho is bounded_variation & dom u = A and A2: u|A is uniformly_continuous; thus for T being DivSequence of A, S be middle_volume_Sequence of rho,u,T st delta T is convergent & lim delta T = 0 holds middle_sum(S) is convergent proof let T being DivSequence of A, S be middle_volume_Sequence of rho,u,T; assume A4: delta T is convergent & lim delta T = 0; defpred P[Element of NAT, set] means ex p being FinSequence of REAL st p = $2 & len p = len (T.$1) & for i be Nat st i in dom (T.$1) holds (p.i) in dom (u|divset((T.$1),i)) & ex z be Real st z = (u|divset((T.$1),i)).(p.i) & (S.$1).i = z * (vol (divset((T.$1),i),rho)); A5: for k be Element of NAT ex p be Element of (REAL)* st P[k, p] proof let k be Element of NAT; defpred P1[Nat,set] means $2 in dom (u|divset((T.k),$1)) & ex c be Real st c = (u|divset((T.k),$1)).($2) & (S.k).$1 = c * (vol (divset((T.k),$1),rho)); A6: Seg len(T.k) = dom(T.k) by FINSEQ_1:def 3; A7: for i be Nat st i in Seg len (T.k) ex x be Element of REAL st P1[i,x] proof let i be Nat; assume i in Seg len(T.k); then i in dom (T.k) by FINSEQ_1:def 3; then consider c be Real such that A8: c in rng (u|divset((T.k),i)) & (S.k).i = c * (vol(divset((T.k),i),rho)) by A1,INTEGR22:def 5; consider x be object such that A9: x in dom (u|divset(T.k,i)) & c = (u|divset(T.k,i)).x by A8,FUNCT_1:def 3; reconsider x as Element of REAL by A9; take x; thus thesis by A8,A9; end; consider p be FinSequence of REAL such that A10: dom p = Seg len(T.k) & for i be Nat st i in Seg len(T.k) holds P1[i,p.i] from FINSEQ_1:sch 5(A7); take p; len p = len (T.k) by A10,FINSEQ_1:def 3; hence thesis by A6,A10,FINSEQ_1:def 11; end; consider Fn be sequence of (REAL)* such that A11: for x be Element of NAT holds P[x, Fn.x] from FUNCT_2:sch 3(A5); consider Fm be sequence of (REAL)* such that A12: for x be Element of NAT holds P[x, Fm.x] from FUNCT_2:sch 3(A5); set TVD = total_vd(rho); A13: 0 <= TVD by A1,INTEGR22:6; now let p be Real; set pp2= p/2; set pv = pp2 / (TVD + 1); assume B13: p > 0; then A14: 0 < pp2 & pp2 < p by XREAL_1:215,216; then A15: 0 < pv by A13,XREAL_1:139; then pv*(TVD) < pv *(TVD + 1) by XREAL_1:29,68; then pv*(TVD) < pp2 by A13,XCMPLX_1:87; then A16: pv*(TVD) < p by A14,XXREAL_0:2; set p2v = pv/2; consider sk be Real such that A17: 0 < sk & for x1,x2 be Real st x1 in dom (u|A) & x2 in dom (u|A) & |. x1-x2 .| < sk holds |.(u|A).x1-(u|A).x2 .| < p2v by A2,A15,FCONT_2:def 1,XREAL_1:215; consider m be Nat such that A18: for i be Nat st m <= i holds |. (delta T).i - 0 .| < sk by A4,A17,SEQ_2:def 7; take m; let n be Nat; A19: n in NAT & m in NAT by ORDINAL1:def 12; assume n >= m; then |. (delta T).n - 0 .| < sk & |. (delta T).m - 0 .| < sk by A18; then |. delta(T.n) .| < sk & |. delta(T.m) .| < sk by A19,INTEGRA3:def 2; then A20: delta(T.n) < sk & delta(T.m) < sk by ABSVALUE:def 1,INTEGRA3:9; A21: (middle_sum(S)).n = Sum(S.n) & (middle_sum(S)).m = Sum(S.m) by INTEGR22:def 7; consider p1 be FinSequence of REAL such that A22: p1 = Fn.n & len p1 = len (T.n) & for i be Nat st i in dom (T.n) holds p1.i in dom (u|divset(T.n,i)) & ex z be Real st z = (u|divset(T.n,i)).(p1.i) & (S.n).i = z * (vol (divset(T.n,i),rho)) by A11,A19; consider p2 be FinSequence of REAL such that A23: p2 = Fm.m & len p2 = len (T.m) & for i be Nat st i in dom (T.m) holds p2.i in dom (u|divset(T.m,i)) & ex z be Real st z = (u|divset(T.m,i)).(p2.i) & (S.m).i = z * (vol (divset(T.m,i),rho)) by A12,A19; defpred H1[object,object,object] means ex i,j being Nat, z be Real st $1=i & $2=j & z = (u|divset(T.n,i)).(p1.i) & $3 = (vol (divset(T.n,i) /\ divset(T.m,j),rho))* z; A24: for x,y be object st x in Seg len(T.n) & y in Seg len (T.m) ex w be object st w in REAL & H1[x,y,w] proof let x,y be object; assume A25: x in Seg len (T.n) & y in Seg len (T.m); then reconsider i=x,j=y as Nat; i in dom (T.n) by A25,FINSEQ_1:def 3; then consider z be Real such that A26: z = (u|divset(T.n,i)).(p1.i) & (S.n).i = z * (vol (divset(T.n,i),rho)) by A22; (vol (divset(T.n,i) /\ divset(T.m,j),rho)) * z in REAL by XREAL_0:def 1; hence thesis by A26; end; consider Snm being Function of [: Seg len (T.n),Seg len (T.m) :],REAL such that A27: for x,y be object st x in Seg len(T.n) & y in Seg len(T.m) holds H1[x,y,Snm.(x,y)] from BINOP_1:sch 1(A24); A28: for i,j being Nat st i in Seg len (T.n) & j in Seg len (T.m) holds ex z be Real st z = (u|divset(T.n,i)).(p1.i) & Snm.(i,j) = (vol (divset(T.n,i) /\ divset(T.m,j),rho))* z proof let i,j being Nat; assume i in Seg len (T.n) & j in Seg len (T.m); then ex i1,j1 being Nat, z be Real st i=i1 & j=j1 & z = (u|divset(T.n,i1)).(p1.i1) & Snm.(i,j)= (vol (divset(T.n,i1) /\ divset(T.m,j1),rho))* z by A27; hence thesis; end; defpred P1[Nat,object] means ex r be FinSequence of REAL st dom r = Seg len (T.m) & $2=Sum r & for j be Nat st j in dom r holds r.j = Snm.($1,j); A29: for k be Nat st k in Seg len (T.n) ex x be object st P1[k,x] proof let k be Nat; assume A30: k in Seg len (T.n); deffunc G(set) = Snm.(k,$1); consider r being FinSequence such that A31: len r = len (T.m) and A32: for j be Nat st j in dom r holds r.j = G(j) from FINSEQ_1:sch 2; A33: dom r = Seg len (T.m) by A31,FINSEQ_1:def 3; for j be Nat st j in dom r holds r.j in REAL proof let j be Nat; assume A34: j in dom r; then [k,j] in [: Seg len (T.n), Seg len (T.m) :] by A30,A33,ZFMISC_1:87; then Snm.(k,j) in REAL by FUNCT_2:5; hence thesis by A32,A34; end; then reconsider r as FinSequence of REAL by FINSEQ_2:12; take x = Sum r; thus thesis by A32,A33; end; consider Xp be FinSequence such that A35: dom Xp = Seg len (T.n) & for k be Nat st k in Seg len (T.n) holds P1[k,Xp.k] from FINSEQ_1:sch 1(A29); for i be Nat st i in dom Xp holds Xp.i in REAL proof let i be Nat; assume i in dom Xp; then ex r be FinSequence of REAL st dom r = Seg len (T.m) & Xp.i = Sum r & for j be Nat st j in dom r holds r.j=Snm.(i,j) by A35; hence thesis by XREAL_0:def 1; end; then reconsider Xp as FinSequence of REAL by FINSEQ_2:12; A36: len Xp = len (T.n) by A35,FINSEQ_1:def 3; for k be Nat st 1 <= k & k <= len Xp holds Xp.k = (S.n).k proof let k be Nat; assume 1 <= k & k <= len Xp; then A38: k in Seg len Xp & k in Seg len (T.n) by A36; then A39: k in dom Xp & k in dom (T.n) by FINSEQ_1:def 3; then consider z be Real such that A40: z = (u|divset(T.n,k)).(p1.k) & (S.n).k = z * (vol (divset(T.n,k),rho)) by A22; consider r be FinSequence of REAL such that A41: dom r = Seg len (T.m) & Xp.k = Sum r & for j be Nat st j in dom r holds r.j=Snm.(k,j) by A35,A38; defpred P11[Nat,set] means $2 = vol (divset(T.n,k) /\ divset(T.m,$1),rho); A42: for i be Nat st i in Seg len r holds ex x be Element of REAL st P11[i,x] proof let i be Nat; assume i in Seg len r; vol(divset(T.n,k) /\ divset(T.m,i), rho) in REAL by XREAL_0:def 1; hence thesis; end; consider vtntm be FinSequence of REAL such that A43: dom vtntm = Seg len r & for i be Nat st i in Seg len r holds P11[i,vtntm.i] from FINSEQ_1:sch 5(A42); A44: dom vtntm = dom r & for j be Nat st j in dom vtntm holds vtntm.j=vol (divset(T.n,k) /\ divset(T.m,j),rho) by A43,FINSEQ_1:def 3; A45: len vtntm = len r & len (T.m) = len r by A41,A43,FINSEQ_1:def 3; then A46: Sum vtntm = vol(divset((T.n),k),rho) by A39,A43,INTEGR22:1,INTEGRA1:8; for j be Nat st j in dom r holds ex x be Real st x = vtntm.j & r.j = x * z proof let j be Nat; assume A47: j in dom r; then A48: ex w be Real st w = (u|divset(T.n,k)).(p1.k) & Snm.(k,j) = (vol(divset(T.n,k) /\ divset(T.m,j),rho)) * w by A28,A38,A41; take vtntm.j; r.j = (vol(divset(T.n,k) /\ divset(T.m,j),rho)) * z by A40,A41,A47,A48; hence thesis by A44,A47; end; hence thesis by A40,A41,A45,A46,Th1; end; then A49: Xp = S.n by A1,A36,INTEGR22:def 5; defpred P2[Nat,object] means ex s be FinSequence of REAL st dom s = Seg len (T.n) & $2 = Sum s & for i be Nat st i in dom s holds s.i = Snm.(i,$1); A50: for k be Nat st k in Seg len (T.m) ex x be object st P2[k,x] proof let k be Nat; assume A51: k in Seg len (T.m); deffunc G(set)= Snm.($1,k); consider s being FinSequence such that A52: len s = len (T.n) and A53: for i be Nat st i in dom s holds s.i = G(i) from FINSEQ_1:sch 2; A54: dom s = Seg len (T.n) by A52,FINSEQ_1:def 3; for i be Nat st i in dom s holds s.i in REAL proof let i be Nat; assume A55: i in dom s; then [i,k] in [: Seg len (T.n), Seg len (T.m) :] by A51,A54,ZFMISC_1:87; then Snm.(i,k) in REAL by FUNCT_2:5; hence thesis by A53,A55; end; then reconsider s as FinSequence of REAL by FINSEQ_2:12; take x = Sum s; thus thesis by A53,A54; end; consider Xq be FinSequence such that A56: dom Xq = Seg len (T.m) & for k be Nat st k in Seg len (T.m) holds P2[k,Xq.k] from FINSEQ_1:sch 1(A50); for j be Nat st j in dom Xq holds Xq.j in REAL proof let j be Nat; assume j in dom Xq; then ex s be FinSequence of REAL st dom s = Seg len(T.n) & Xq.j = Sum s & for i be Nat st i in dom s holds s.i = Snm.(i,j) by A56; hence thesis by XREAL_0:def 1; end; then reconsider Xq as FinSequence of REAL by FINSEQ_2:12; defpred H2[object,object,object] means ex i,j being Nat, z be Real st $1 = i & $2 = j & z = (u|divset(T.m,j)).(p2.j) & $3 = (vol((divset(T.n,i) /\ divset(T.m,j)),rho)) * z; A57: for x,y be object st x in Seg len (T.n) & y in Seg len (T.m) ex w be object st w in REAL & H2[x,y,w] proof let x,y be object; assume A58: x in Seg len (T.n) & y in Seg len (T.m); then reconsider i=x,j=y as Nat; j in dom (T.m) by A58,FINSEQ_1:def 3; then consider z be Real such that A59: z = (u|divset(T.m,j)).(p2.j) & (S.m).j = z * (vol (divset(T.m,j),rho)) by A23; (vol(divset(T.n,i) /\ divset(T.m,j),rho)) * z in REAL by XREAL_0:def 1; hence thesis by A59; end; consider Smn being Function of [: Seg len (T.n),Seg len (T.m) :], REAL such that A60: for x,y be object st x in Seg len(T.n) & y in Seg len(T.m) holds H2[x,y,Smn.(x,y)] from BINOP_1:sch 1(A57); A61: for i,j being Nat st i in Seg len(T.n) & j in Seg len(T.m) holds ex z be Real st z = (u|divset(T.m,j)).(p2.j) & Smn.(i,j) = (vol(divset(T.n,i) /\ divset(T.m,j),rho)) * z proof let i,j being Nat; assume i in Seg len (T.n) & j in Seg len (T.m); then ex i1,j1 being Nat, z be Real st i = i1 & j = j1 & z = (u|divset(T.m,j1)).(p2.j1) & Smn.(i,j) = (vol(divset(T.n,i1) /\ divset(T.m,j1),rho)) * z by A60; hence thesis; end; defpred P3[Nat,object] means ex s be FinSequence of REAL st dom s = Seg len(T.n) & $2 = Sum s & for i be Nat st i in dom s holds s.i = Smn.(i,$1); A62: for k be Nat st k in Seg len(T.m) ex x be object st P3[k,x] proof let k be Nat; assume A63: k in Seg len(T.m); deffunc G(set)= Smn.($1,k); consider s being FinSequence such that A64: len s = len (T.n) and A65: for i be Nat st i in dom s holds s.i = G(i) from FINSEQ_1:sch 2; A66: dom s = Seg len (T.n) by A64,FINSEQ_1:def 3; for i be Nat st i in dom s holds s.i in REAL proof let i be Nat; assume A67: i in dom s; then [i,k] in [: Seg len (T.n), Seg len (T.m) :] by A63,A66,ZFMISC_1:87; then Smn.(i,k) in REAL by FUNCT_2:5; hence thesis by A65,A67; end; then reconsider s as FinSequence of REAL by FINSEQ_2:12; take x = Sum s; thus thesis by A65,A66; end; consider Zq be FinSequence such that A68: dom Zq = Seg len (T.m) & for k be Nat st k in Seg len (T.m) holds P3[k,Zq.k] from FINSEQ_1:sch 1(A62); for j be Nat st j in dom Zq holds Zq.j in REAL proof let j be Nat; assume j in dom Zq; then ex s be FinSequence of REAL st dom s = Seg len (T.n) & Zq.j=Sum s & for i be Nat st i in dom s holds s.i = Smn.(i,j) by A68; hence thesis by XREAL_0:def 1; end; then reconsider Zq as FinSequence of REAL by FINSEQ_2:12; A69: len Zq = len(T.m) by A68,FINSEQ_1:def 3; for k be Nat st 1 <= k & k <= len Zq holds Zq.k = (S.m).k proof let k be Nat; assume A71: 1 <= k <= len Zq; then consider s be FinSequence of REAL such that A72: dom s = Seg len(T.n) & Zq.k = Sum s & for i be Nat st i in dom s holds s.i = Smn.(i,k) by A68,FINSEQ_3:25; A73: k in Seg len(T.m) by A69,A71; A74: k in dom (T.m) by A69,A71,FINSEQ_3:25; then consider z be Real such that A75: z = (u|divset((T.m),k)).(p2.k) & (S.m).k = z * (vol(divset((T.m),k),rho)) by A23; defpred P11[Nat,set] means $2 = vol(divset(T.n,$1) /\ divset(T.m,k),rho); A76: for i be Nat st i in Seg len s holds ex x be Element of REAL st P11[i,x] proof let i be Nat; assume i in Seg len s; vol(divset(T.n,i) /\ divset(T.m,k),rho) in REAL by XREAL_0:def 1; hence thesis; end; consider vtntm be FinSequence of REAL such that A77: dom vtntm = Seg len s & for i be Nat st i in Seg len s holds P11[i,vtntm.i] from FINSEQ_1:sch 5(A76); A78: dom vtntm = dom s & len vtntm = len s by A77,FINSEQ_1:def 3; A79: for j be Nat st j in dom vtntm holds vtntm.j = vol(divset(T.m,k) /\ divset(T.n,j),rho) by A77; len s = len (T.n) by A72,FINSEQ_1:def 3; then A80: Sum vtntm = vol (divset(T.m,k),rho) by A74,A78,A79,INTEGR22:1,INTEGRA1:8; for j be Nat st j in dom s holds ex x be Real st x = vtntm.j & s.j = x * z proof let j be Nat; assume A81: j in dom s; then A82: ex w be Real st w = (u|divset((T.m),k)).(p2.k) & Smn.(j,k) = (vol(divset(T.n,j) /\ divset(T.m,k),rho)) * w by A61,A72,A73; take vtntm.j; s.j = (vol(divset(T.n,j) /\ divset(T.m,k),rho))* z by A72,A75,A81,A82; hence thesis by A77,A78,A81; end; hence thesis by A72,A75,A78,A80,Th1; end; then Zq = S.m by A1,A69,INTEGR22:def 5; then A83: Sum(S.n) - Sum(S.m) = Sum Xq - Sum Zq by A35,A49,A56,INTEGR22:2; set XZq = Xq - Zq; A84: dom XZq = dom Xq /\ dom Zq by VALUED_1:12; reconsider XZq = Xq - Zq as FinSequence of REAL; len Xq = len Zq by A56,A68,FINSEQ_3:29; then A86: Xq is Element of (len Xq)-tuples_on REAL & Zq is Element of (len Xq)-tuples_on REAL by FINSEQ_2:92; A87: for i,j be Nat, Snmij,Smnij be Real st i in Seg len (T.n) & j in Seg len (T.m) & Snmij = Snm.(i,j) & Smnij = Smn.(i,j) holds |. Snmij - Smnij .| <= |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| * pv proof let i,j be Nat, Snmij,Smnij be Real; assume A88: i in Seg len (T.n) & j in Seg len (T.m) & Snmij = Snm.(i,j) & Smnij = Smn.(i,j); then consider z1 be Real such that A89: z1 = (u|divset(T.n,i)).(p1.i) & Snm.(i,j) = (vol(divset(T.n,i) /\ divset(T.m,j),rho)) * z1 by A28; consider z2 be Real such that A90: z2 = (u|divset((T.m),j)).(p2.j) & Smn.(i,j) = (vol(divset(T.n,i) /\ divset(T.m,j),rho)) * z2 by A61,A88; A91: i in dom (T.n) & j in dom (T.m) by A88,FINSEQ_1:def 3; then A92: p1.i in dom (u|divset(T.n,i)) & p2.j in dom (u|divset(T.m,j)) by A22,A23; then p1.i in dom u /\ divset(T.n,i) & p2.j in dom u /\ divset(T.m,j) by RELAT_1:61; then A93: p1.i in dom u & p1.i in divset(T.n,i) & p2.j in dom u & p2.j in divset(T.m,j) by XBOOLE_0:def 4; A94: z1 = u.(p1.i) & z2 = u.(p2.j) by A89,A90,A92,FUNCT_1:47; per cases; suppose divset(T.n,i) /\ divset(T.m,j) = {}; then vol(divset(T.n,i) /\ divset(T.m,j),rho) = (0 qua Real) by INTEGR22:def 1; hence |. Snmij - Smnij .| <= |. (vol (divset(T.n,i) /\ divset(T.m,j),rho)) .| * pv by A88,A89,A90,COMPLEX1:44; end; suppose divset(T.n,i) /\ divset(T.m,j) <> {}; then consider t be object such that A97: t in divset(T.n,i) /\ divset(T.m,j) by XBOOLE_0:def 1; reconsider t as Real by A97; A98: divset(T.m,j) c= A by A91,INTEGRA1:8; A99: t in divset(T.n,i) & t in divset(T.m,j) by A97,XBOOLE_0:def 4; then |. (p1.i)-t .| < sk & |. t-(p2.j) .| < sk by A20,A91,A93,INTEGR20:12; then A100: |. u.(p1.i)-u.t .| < p2v & |. u.t-u.(p2.j) .| < p2v by A1,A17,A93,A98,A99; reconsider DMN = divset(T.n,i) /\ divset(T.m,j) as real-bounded Subset of REAL by XBOOLE_1:17,XXREAL_2:45; Snmij - Smnij = (vol (DMN,rho)) * (u.(p1.i) - u.t) + (vol (DMN,rho)) * (u.t - u.(p2.j)) by A88,A89,A90,A94; then A101: |. Snmij - Smnij .| <= |. (vol (DMN,rho)) * (u.(p1.i) -u.t) .| + |. (vol (DMN,rho)) * (u.t - u.(p2.j)) .| by COMPLEX1:56; A102: |. (vol (DMN,rho)) * (u.(p1.i) - u.t) .| = |. vol (DMN,rho) .| * |. u.(p1.i) - u.t .| & |. (vol (DMN,rho)) * (u.t - u.(p2.j)) .| = |.vol (DMN,rho).| * |. u.t - u.(p2.j) .| by COMPLEX1:65; 0 <= |.vol (DMN,rho).| by COMPLEX1:46; then |. (vol(DMN,rho)) * (u.(p1.i) - u.t) .| <= |.vol(DMN,rho).| * p2v & |. (vol(DMN,rho)) * (u.t - u.(p2.j)) .| <= |.vol(DMN,rho).| * p2v by A100,A102,XREAL_1:64; then |. (vol (DMN,rho)) * (u.(p1.i) - u.t) .| + |. (vol (DMN,rho)) * (u.t - u.(p2.j)) .| <= |.vol (DMN,rho).| * p2v + |.vol (DMN,rho).| * p2v by XREAL_1:7; hence |. Snmij - Smnij .| <= |. vol (divset(T.n,i) /\ divset(T.m,j),rho) .| * pv by A101,XXREAL_0:2; end; end; consider vtntm be FinSequence of REAL such that A103: len vtntm = len(T.m) & Sum vtntm <= total_vd(rho) & for j be Nat st j in dom (T.m) holds ex p be FinSequence of REAL st vtntm.j = Sum p & len p = len (T.n) & for i be Nat st i in dom (T.n) holds p.i = |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| by A1,Th19; reconsider PVD = pv * vtntm as FinSequence of REAL; dom PVD = dom vtntm by VALUED_1:def 5; then dom PVD = Seg len(T.m) by A103,FINSEQ_1:def 3; then A104: len PVD = len (T.m) by FINSEQ_1:def 3; A105: for j be Nat st j in Seg len (T.m) holds ex pvtntm be FinSequence of REAL st PVD.j = Sum pvtntm & len (pvtntm) = len (T.n) & for i be Nat st i in Seg len (T.n) holds (pvtntm).i = pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| proof let j be Nat; assume j in Seg len (T.m); then j in dom (T.m) by FINSEQ_1:def 3; then consider v be FinSequence of REAL such that A107: vtntm.j = Sum v & len v = len (T.n) & for i be Nat st i in dom (T.n) holds v.i = |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| by A103; reconsider pvtntm = pv * v as FinSequence of REAL; take pvtntm; thus PVD.j = pv * vtntm.j by VALUED_1:6 .= Sum pvtntm by A107,RVSUM_1:87; dom pvtntm = dom v by VALUED_1:def 5; then dom pvtntm = Seg len(T.n) by A107,FINSEQ_1:def 3; hence len pvtntm = len(T.n) by FINSEQ_1:def 3; let i be Nat; assume i in Seg len (T.n); then a108: i in dom (T.n) by FINSEQ_1:def 3; thus (pvtntm).i = pv * v.i by VALUED_1:6 .= pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| by A107,a108; end; A109: Sum(PVD) = pv * Sum(vtntm) by RVSUM_1:87; A110: pv * Sum(vtntm) <= pv * total_vd(rho) by A13,B13,A103,XREAL_1:64; A111: len XZq = len (T.m) by A56,A68,A84,FINSEQ_1:def 3; for j be Nat st j in dom XZq holds |. XZq.j .| <= PVD.j proof let j be Nat; assume A112: j in dom XZq; then A113: XZq.j = Xq.j - Zq.j by VALUED_1:13; consider Xsq be FinSequence of REAL such that A114: dom Xsq = Seg len (T.n) & Xq.j = Sum Xsq & for i be Nat st i in dom Xsq holds Xsq.i = Snm.(i,j) by A56,A68,A84,A112; consider Zsq be FinSequence of REAL such that A115: dom Zsq = Seg len (T.n) & Zq.j = Sum Zsq & for i be Nat st i in dom Zsq holds Zsq.i = Smn.(i,j) by A56,A68,A84,A112; set XZsq = Xsq - Zsq; A116: dom XZsq = dom Xsq /\ dom Zsq by VALUED_1:12; reconsider XZsq as FinSequence of REAL; A117: len XZsq = len (T.n) by A114,A115,A116,FINSEQ_1:def 3; consider pvtntm be FinSequence of REAL such that A118: PVD.j = Sum pvtntm & len (pvtntm) = len (T.n) & for i be Nat st i in Seg len (T.n) holds (pvtntm).i = pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| by A105,A56,A68,A84,A112; for i be Nat st i in dom XZsq holds |. XZsq.i .| <= (pvtntm).i proof let i be Nat; assume A119: i in dom XZsq; then A120: XZsq.i = Xsq.i - Zsq.i by VALUED_1:13; A121: (pvtntm).i = pv * |. vol(divset(T.n,i) /\ divset(T.m,j),rho) .| by A118,A114,A115,A116,A119; Xsq.i = Snm.(i,j) & Zsq.i = Smn.(i,j) by A114,A115,A116,A119; hence |.XZsq.i.| <= pvtntm.i by A56,A68,A84,A87,A112,A114,A115,A116,A119,A120,A121; end; then A122: |. Sum XZsq .| <= PVD.j by A117,A118,Th3; len Xsq = len Zsq by A114,A115,FINSEQ_3:29; then Xsq is Element of (len Xsq)-tuples_on REAL & Zsq is Element of (len Xsq)-tuples_on REAL by FINSEQ_2:92; hence thesis by A113,A114,A115,A122,RVSUM_1:90; end; then |. Sum XZq .| <= Sum PVD by A104,A111,Th3; then A124: |. Sum XZq .| <= TVD * pv by A109,A110,XXREAL_0:2; Sum (XZq) = ((middle_sum(S)).n) - ((middle_sum(S)).m) by A21,A83,A86,RVSUM_1:90; hence |.((middle_sum(S)).n) - ((middle_sum(S)).m).| < p by A16,A124,XXREAL_0:2; end; hence middle_sum(S) is convergent by SEQ_4:41; end; end; theorem Th21: for A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, u be PartFunc of REAL,REAL, T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of rho,u,T0, S be middle_volume_Sequence of rho,u,T st for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i ex S1 be middle_volume_Sequence of rho,u,T1 st for i be Nat holds S1.(2*i) = S0.i & S1.(2*i+1) = S.i proof let A be non empty closed_interval Subset of REAL, rho be Function of A,REAL, u be PartFunc of REAL,REAL, T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of rho,u,T0, S be middle_volume_Sequence of rho,u,T; assume A2: for k be Nat holds T1.(2*k) = T0.k & T1.(2*k+1) = T.k; reconsider SS0 = S0, SS = S as sequence of (REAL)*; deffunc F(Nat) = In(SS0.$1, (REAL)*); deffunc G(Nat) = In(SS.$1, (REAL)*); consider S1 being sequence of (REAL)* such that A3: for n be Nat holds S1.(2*n) = F(n) & S1.(2*n+1) = G(n) from INTEGR20:sch 1; for i be Element of NAT holds S1.i is middle_volume of rho,u,T1.i proof let i be Element of NAT; consider k be Nat such that A4: i = 2*k or i = 2*k+1 by INTEGR20:14; reconsider k as Element of NAT by ORDINAL1:def 12; per cases by A4; suppose A5: i = 2*k; then S1.i = In(SS0.k, (REAL)*) by A3 .= S0.k by FUNCT_2:5,SUBSET_1:def 8; hence S1.i is middle_volume of rho,u,T1.i by A2,A5; end; suppose A6: i = 2*k + 1; then S1.i = In(SS.k, (REAL)*) by A3 .= S.k by FUNCT_2:5,SUBSET_1:def 8; hence S1.i is middle_volume of rho,u,T1.i by A2,A6; end; end; then reconsider S1 as middle_volume_Sequence of rho,u,T1 by INTEGR22:def 6; take S1; let i be Nat; A7: i is Element of NAT by ORDINAL1:def 12; A8: S1.(2*i) = In(SS0.i,(REAL)*) by A3 .= S0.i by A7,FUNCT_2:5,SUBSET_1:def 8; S1.(2*i+1) = In(SS.i,(REAL)*) by A3 .= S.i by A7,FUNCT_2:5,SUBSET_1:def 8; hence thesis by A8; end; theorem Th22: for Sq0,Sq,Sq1 be Real_Sequence st Sq1 is convergent & for i be Nat holds Sq1.(2*i) = Sq0.i & Sq1.(2*i+1) = Sq.i holds Sq0 is convergent & lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 proof let Sq0,Sq,Sq1 be Real_Sequence; assume that A1: Sq1 is convergent and A2: for i be Nat holds Sq1.(2*i) = Sq0.i & Sq1.(2*i+1) = Sq.i; A3: for r be Real st 0 < r ex m1 be Nat st for i be Nat st m1 <= i holds |. Sq0.i - lim Sq1 .|