= p by A2; hence thesis by A4; end; then A5: p is LowerBound of rng seq by XXREAL_2:def 2; reconsider INFSEQ = inferior_realsequence seq as sequence of ExtREAL; consider Y be non empty Subset of ExtREAL such that A6: Y = {seq.k where k is Nat: 0 <= k} and A7: INFSEQ.0 = inf Y by RINFSUP2:def 6; now let x be object; assume x in rng seq; then consider k be object such that A8: k in dom seq and A9: x = seq.k by FUNCT_1:def 3; thus x in Y by A6,A8,A9; end; then A10: rng seq c= Y; for n be Element of NAT holds sup INFSEQ >= INFSEQ.n proof let n be Element of NAT; NAT = dom INFSEQ by FUNCT_2:def 1; then INFSEQ.n in rng INFSEQ by FUNCT_1:def 3; hence thesis by XXREAL_2:4; end; then A11: sup INFSEQ >= INFSEQ.0; now let x be object; assume x in Y; then consider k be Nat such that A12: x = seq.k & 0 <= k by A6; A13: k in NAT by ORDINAL1:def 12; dom seq = NAT by FUNCT_2:def 1; hence x in rng seq by A12,FUNCT_1:3,A13; end; then Y c= rng seq; then Y = rng seq by A10,XBOOLE_0:def 10; then (inferior_realsequence seq).0 >= p by A5,A7,XXREAL_2:def 4; then lim_inf seq >= p by A11,XXREAL_0:2; hence thesis by A1,RINFSUP2:41; end; reconsider zz=0 as ExtReal; theorem Th11: seq1 is convergent & seq2 is convergent & seq1 is nonnegative & seq2 is nonnegative & (for k be Nat holds seq.k = seq1.k + seq2.k) implies seq is nonnegative & seq is convergent & lim seq = lim seq1 + lim seq2 proof assume that A1: seq1 is convergent and A2: seq2 is convergent and A3: seq1 is nonnegative and A4: seq2 is nonnegative and A5: for k be Nat holds seq.k = seq1.k + seq2.k; A6: not seq2 is convergent_to_-infty by A4,Th8; for n be object st n in dom seq holds 0. <= seq.n proof let n be object; assume n in dom seq; then reconsider n1=n as Nat; A7: 0 <= seq2.n1 by A4,SUPINF_2:51; A8: seq.n1 = seq1.n1 + seq2.n1 by A5; 0 <= seq1.n1 by A3,SUPINF_2:51; hence thesis by A7,A8; end; hence seq is nonnegative by SUPINF_2:52; A9: not seq1 is convergent_to_-infty by A3,Th8; for n be Nat holds 0 <= seq2.n by A4,SUPINF_2:51; then A10: lim seq2 <> -infty by A2,Th10; per cases by A1,A9; suppose A11: seq1 is convergent_to_+infty; for g be Real st 0 < g ex n be Nat st for m be Nat st n<=m holds g <= seq.m proof let g be Real; assume 0 < g; then consider n be Nat such that A12: for m be Nat st n <= m holds g <= seq1.m by A11; take n; let m be Nat; assume n<=m; then A13: g <= seq1.m by A12; 0 <= seq2.m by A4,SUPINF_2:51; then g + zz <= seq1.m + seq2.m by A13,XXREAL_3:36; then g <= seq1.m + seq2.m by XXREAL_3:4; hence thesis by A5; end; then A14: seq is convergent_to_+infty; hence seq is convergent; then A15: lim seq = +infty by A14,MESFUNC5:def 12; lim seq1 = +infty by A1,A11,MESFUNC5:def 12; hence thesis by A10,A15,XXREAL_3:def 2; end; suppose A16: seq1 is convergent_to_finite_number; then A17: not seq1 is convergent_to_-infty by MESFUNC5:51; not seq1 is convergent_to_+infty by A16,MESFUNC5:50; then consider g be Real such that A18: lim seq1 = g and A19: for p be Real st 0

-infty by XXREAL_3:19; A43: 0 <= seq1.m by A3,SUPINF_2:51; A44: |. seq1.m - g .| = |.e1 qua Complex.| by A38,EXTREAL1:12; then A45: |. seq2.m - h .| + |. seq1.m - g .| = |.e1 qua Complex.| + |.e2 qua Complex.| by A40,SUPINF_2:1; (g+h) = g + (h qua ExtReal); then seq.m - (g+h) = seq.m - h - g by XXREAL_3:31 .= seq1.m + seq2.m - h - g by A5 .= seq1.m + (seq2.m - h) - g by A43,A41,XXREAL_3:30 .= (seq2.m - h) + (seq1.m - g) by A43,A42,XXREAL_3:30; then A46: |. seq.m - (g+h) .| <= |. seq2.m - h .| + |. seq1.m - g .| by EXTREAL1:24; |.e1 qua Complex.| + |.e2 qua Complex.| < p/2 + p/2 by A18,A27,A37,A35,A44,A40,XREAL_1:8; hence thesis by A46,A45,XXREAL_0:2; end; then A47: seq is convergent_to_finite_number; hence seq is convergent; then lim seq = gh by A29,A47,MESFUNC5:def 12; hence thesis by A18,A27,SUPINF_2:1; end; end; end; theorem Th12: (for n be Nat holds G.n = (F.n)|D) & x in D implies (F#x is convergent_to_+infty implies G#x is convergent_to_+infty) & (F#x is convergent_to_-infty implies G#x is convergent_to_-infty) & (F#x is convergent_to_finite_number implies G#x is convergent_to_finite_number) & (F#x is convergent implies G#x is convergent) proof assume that A1: for n be Nat holds G.n = (F.n)|D and A2: x in D; thus A3: F#x is convergent_to_+infty implies G#x is convergent_to_+infty proof assume A4: F#x is convergent_to_+infty; let g be Real; assume 0 < g; then consider n be Nat such that A5: for m be Nat st n <= m holds g <= (F#x).m by A4; take n; let m be Nat; assume n <= m; then g <= (F#x).m by A5; then g <= (F.m).x by MESFUNC5:def 13; then g <= ((F.m)|D).x by A2,FUNCT_1:49; then g <= (G.m).x by A1; hence g <= (G#x).m by MESFUNC5:def 13; end; thus A6: F#x is convergent_to_-infty implies G#x is convergent_to_-infty proof assume A7: F#x is convergent_to_-infty; let g be Real; assume g < 0; then consider n be Nat such that A8: for m be Nat st n <= m holds (F#x).m <= g by A7; take n; let m be Nat; assume n <= m; then (F#x).m <= g by A8; then (F.m).x <= g by MESFUNC5:def 13; then ((F.m)|D).x <= g by A2,FUNCT_1:49; then (G.m).x <= g by A1; hence (G#x).m <= g by MESFUNC5:def 13; end; thus A9: F#x is convergent_to_finite_number implies G#x is convergent_to_finite_number proof assume F#x is convergent_to_finite_number; then consider g be Real such that A10: lim(F#x) = g and A11: for p be Real st 0

0 implies Integral(M,f) = +infty proof assume that A1: E = dom f and A2: f is_measurable_on E and A3: f is nonnegative and A4: M.(E /\ eq_dom(f,+infty)) <> 0; reconsider EE = E /\ eq_dom(f,+infty) as Element of S by A1,A2,MESFUNC1:33; A5: dom(f|E) = E by A1; E = dom f /\ E by A1; then A6: f|E is_measurable_on E by A2,MESFUNC5:42; integral+(M,f|EE) <= integral+(M,f|E) by A1,A2,A3,MESFUNC5:83,XBOOLE_1:17; then A7: integral+(M,f|EE) <= Integral(M,f|E) by A3,A6,A5,MESFUNC5:15,88; A8: EE = dom f /\ EE by A1,XBOOLE_1:17,28; f is_measurable_on EE by A2,MESFUNC1:30,XBOOLE_1:17; then A9: f|EE is_measurable_on EE by A8,MESFUNC5:42; A10: f|EE is nonnegative by A3,MESFUNC5:15; reconsider ES = {} as Element of S by PROB_1:4; deffunc G(Element of NAT) = $1(#)((chi(EE,X))|EE); consider G be Function such that A11: dom G = NAT & for n be Element of NAT holds G.n = G(n) from FUNCT_1 :sch 4; now let g be object; assume g in rng G; then consider m be object such that A12: m in dom G and A13: g = G.m by FUNCT_1:def 3; reconsider m as Element of NAT by A11,A12; g = m(#)((chi(EE,X))|EE) by A11,A13; hence g in PFuncs(X,ExtREAL) by PARTFUN1:45; end; then rng G c= PFuncs(X,ExtREAL); then reconsider G as Functional_Sequence of X,ExtREAL by A11,FUNCT_2:def 1 ,RELSET_1:4; A14: for n be Nat holds dom(G.n) = EE & for x be set st x in dom(G.n) holds ( G.n).x = n proof let n be Nat; reconsider n1 = n as Element of NAT by ORDINAL1:def 12; EE c= X; then EE c= dom(chi(EE,X)) by FUNCT_3:def 3; then A15: dom((chi(EE,X))|EE) = EE by RELAT_1:62; A16: G.n = n1(#)((chi(EE,X))|EE) by A11; hence A17: dom(G.n) = EE by A15,MESFUNC1:def 6; let x be set; assume A18: x in dom(G.n); then reconsider x1=x as Element of X; chi(EE,X).x1 = 1. by A17,A18,FUNCT_3:def 3; then ((chi(EE,X))|EE).x1 = 1. by A15,A17,A18,FUNCT_1:47; then (G.n).x = ( n1) * 1. by A16,A18,MESFUNC1:def 6; hence thesis by XXREAL_3:81; end; A19: for n be Nat holds G.n is nonnegative proof let n be Nat; for x be object st x in dom(G.n) holds 0 <= (G.n).x by A14; hence thesis by SUPINF_2:52; end; deffunc K(Element of NAT) = integral'(M,G.$1); consider K be sequence of ExtREAL such that A20: for n be Element of NAT holds K.n = K(n) from FUNCT_2:sch 4; reconsider K as ExtREAL_sequence; A21: for n be Nat holds K.n=integral'(M,G.n) proof let n be Nat; reconsider n1=n as Element of NAT by ORDINAL1:def 12; K.n = integral'(M,G.n1) by A20; hence thesis; end; A22: dom(f|EE) = EE by A1,RELAT_1:62,XBOOLE_1:17; A23: for n,m be Nat st n <=m holds for x be Element of X st x in dom(f|EE) holds (G.n).x <= (G.m).x proof let n,m be Nat such that A24: n <= m; let x be Element of X; assume A25: x in dom(f|EE); then x in dom(G.n) by A22,A14; then A26: (G.n).x = n by A14; x in dom(G.m) by A22,A14,A25; hence thesis by A14,A24,A26; end; A27: for n be Nat holds dom(G.n) = dom(f|EE) & G.n is_simple_func_in S proof let n be Nat; reconsider n1 = n as Element of NAT by ORDINAL1:def 12; thus A28: dom(G.n) = dom(f|EE) by A22,A14; for x be object st x in dom(G.n) holds (G.n).x = n1 by A14; hence thesis by A22,A28,MESFUNC6:2; end; A29: for i be Element of NAT holds K.i = ( i)*(M.(dom(G.i))) proof let i be Element of NAT; reconsider ii=i as R_eal by XXREAL_0:def 1; for x be object st x in dom(G.i) holds (G.ii).x = ii by A14; then integral'(M,G.i) = (ii)*(M.(dom(G.ii))) by A27,MESFUNC5:71; hence thesis by A21; end; M.ES <= M.EE by MEASURE1:31,XBOOLE_1:2; then A30: In(0,REAL) < M.EE by A4,VALUED_0:def 19; A31: not rng K is bounded_above proof assume rng K is bounded_above; then consider UB be Real such that A32: UB is UpperBound of rng K by XXREAL_2:def 10; reconsider r = UB as Real; per cases by A30,XXREAL_0:10; suppose A33: M.EE = +infty; K.1 = ( 1) * (M.(dom(G.1))) by A29; then K.1 = ( 1) * (M.EE) by A14; then A34: K.1 = +infty by A33,XXREAL_3:def 5; dom K = NAT by FUNCT_2:def 1; then K.1 in rng K by FUNCT_1:3; then K.1 <= UB by A32,XXREAL_2:def 1; hence contradiction by A34,XXREAL_0:4; end; suppose M.EE in REAL; then reconsider ee = M.EE as Real; consider n be Nat such that A35: r/ee < n by SEQ_4:3; A36: n in NAT by ORDINAL1:def 12; K.n = ( n) * (M.(dom(G.n))) by A29,A36; then K.n = ( n) * (M.EE) by A14; then A37: K.n = n * ee by EXTREAL1:1; (r/ee) * ee < n * ee by A30,A35,XREAL_1:68; then r / (ee/ee) < K.n by A37,XCMPLX_1:82; then A38: r < K.n by A4,XCMPLX_1:51; dom K = NAT by FUNCT_2:def 1; then K.n in rng K by FUNCT_1:3,A36; then K.n <= r by A32,XXREAL_2:def 1; hence contradiction by A38; end; end; for n,m be Nat st m <= n holds K.m <= K.n proof let n,m be Nat; A39: n in NAT by ORDINAL1:def 12; A40: m in NAT by ORDINAL1:def 12; dom(G.m) = EE by A14; then A41: K.m = ( m)*M.EE by A29,A40; dom(G.n) = EE by A14; then A42: K.n = ( n)*M.EE by A29,A39; assume m <= n; hence thesis by A30,A41,A42,XXREAL_3:71; end; then A43: K is non-decreasing by RINFSUP2:7; then A44: lim K = sup K by RINFSUP2:37; A45: for x be Element of X st x in dom(f|EE) holds G#x is convergent & lim(G# x) = (f|EE).x proof let x be Element of X; assume A46: x in dom(f|EE); then A47: x in EE by A1,RELAT_1:62,XBOOLE_1:17; then x in eq_dom(f,+infty) by XBOOLE_0:def 4; then f.x = +infty by MESFUNC1:def 15; then A48: (f|EE).x = +infty by A47,FUNCT_1:49; A49: rng(G#x) is not bounded_above proof assume rng(G#x) is bounded_above; then consider UB be Real such that A50: UB is UpperBound of rng(G#x) by XXREAL_2:def 10; reconsider r = UB as Real; consider n be Nat such that A51: r < n by SEQ_4:3; x in dom(G.n) by A14,A47; then (G.n).x = n by A14; then A52: UB < (G#x).n by A51,MESFUNC5:def 13; A53: n in NAT by ORDINAL1:def 12; dom(G#x) = NAT by FUNCT_2:def 1; then (G#x).n in rng(G#x) by FUNCT_1:3,A53; hence contradiction by A52,A50,XXREAL_2:def 1; end; for n,m be Nat st m<=n holds (G#x).m <= (G#x).n proof let n,m be Nat; dom(G.n) = EE by A14; then A54: (G.n).x = n by A22,A14,A46; dom(G.m) = EE by A14; then (G.m).x = m by A22,A14,A46; then A55: (G#x).m = m by MESFUNC5:def 13; assume m <= n; hence thesis by A54,A55,MESFUNC5:def 13; end; then A56: G#x is non-decreasing by RINFSUP2:7; sup rng(G#x) is UpperBound of rng(G#x) by XXREAL_2:def 3; then sup(G#x) = +infty by A49,XXREAL_2:53; hence thesis by A56,A48,RINFSUP2:37; end; sup rng K is UpperBound of rng K by XXREAL_2:def 3; then A57: sup K = +infty by A31,XXREAL_2:53; K is convergent by A43,RINFSUP2:37; then integral+(M,f|EE) = +infty by A10,A22,A9,A27,A19,A23,A45,A21,A44,A57, MESFUNC5:def 15; then Integral(M,f|E) = +infty by A7,XXREAL_0:4; hence thesis by A1; end; reconsider jj=1 as Real; theorem Integral(M,chi(E,X)) = M.E & Integral(M,(chi(E,X))|E) = M.E proof reconsider XX = X as Element of S by MEASURE1:7; set F = XX \ E; A1: now let x be Element of X; assume A2: x in dom(max- chi(E,X)); per cases; suppose x in E; then chi(E,X).x = 1 by FUNCT_3:def 3; then max(-(chi(E,X).x),0.) = 0. by XXREAL_0:def 10; hence (max-(chi(E,X))).x = 0 by A2,MESFUNC2:def 3; end; suppose not x in E; then chi(E,X).x = 0. by FUNCT_3:def 3; then -chi(E,X).x = 0; then max(-(chi(E,X).x),0.) = 0; hence (max-(chi(E,X))).x = 0 by A2,MESFUNC2:def 3; end; end; A3: XX = dom chi(E,X) by FUNCT_3:def 3; then A4: XX = dom(max+(chi(E,X))) by MESFUNC7:23; A5: XX /\ F = F by XBOOLE_1:28; then A6: dom((max+(chi(E,X)))|F) = F by A4,RELAT_1:61; A7: now let x be Element of X; assume A8: x in dom((max+(chi(E,X)))|F); then chi(E,X).x = 0 by A6,FUNCT_3:37; then (max+(chi(E,X))).x = 0 by MESFUNC7:23; hence ((max+(chi(E,X)))|F).x = 0 by A8,FUNCT_1:47; end; A9: chi(E,X) is_measurable_on XX by MESFUNC2:29; then A10: max+(chi(E,X)) is_measurable_on XX by MESFUNC7:23; then max+(chi(E,X)) is_measurable_on F by MESFUNC1:30; then A11: integral+(M,(max+ chi(E,X))|F) = 0 by A4,A5,A6,A7,MESFUNC5:42,87; A12: XX /\ E = E by XBOOLE_1:28; then A13: dom((max+(chi(E,X)))|E) = E by A4,RELAT_1:61; E \/ F = XX by A12,XBOOLE_1:51; then A14: (max+ chi(E,X))|(E\/F) = max+ chi(E,X); A15: for x be object st x in dom max+(chi(E,X)) holds 0. <= (max+(chi(E,X))).x by MESFUNC2:12; then A16: max+(chi(E,X)) is nonnegative by SUPINF_2:52; then integral+(M,(max+ chi(E,X))|(E\/F)) = integral+(M,(max+ chi(E,X))|E) + integral+(M,(max+ chi(E,X))|F) by A4,A10,MESFUNC5:81,XBOOLE_1:79; then A17: integral+(M,max+ chi(E,X)) = integral+(M,(max+ chi(E,X))|E) by A14,A11, XXREAL_3:4; A18: now let x be object; assume A19: x in dom((max+(chi(E,X)))|E); then chi(E,X).x = 1 by A13,FUNCT_3:def 3; then (max+(chi(E,X))).x = 1 by MESFUNC7:23; hence ((max+(chi(E,X)))|E).x = 1 by A19,FUNCT_1:47; end; then (max+(chi(E,X)))|E is_simple_func_in S by A13,MESFUNC6:2; then integral+(M,max+ chi(E,X)) = integral'(M,(max+ chi(E,X))|E) by A16,A17, MESFUNC5:15,77; then A20: integral+(M,max+ chi(E,X)) = jj * M.(dom((max+(chi(E,X)))|E)) by A13,A18,MESFUNC5:104; max+(chi(E,X)) is_measurable_on E by A10,MESFUNC1:30; then (max+(chi(E,X)))|E is_measurable_on E by A4,A12,MESFUNC5:42; then A21: (chi(E,X))|E is_measurable_on E by MESFUNC7:23; (max+(chi(E,X)))|E is nonnegative by A15,MESFUNC5:15,SUPINF_2:52; then A22: (chi(E,X))|E is nonnegative by MESFUNC7:23; E = dom((chi(E,X))|E) by A13,MESFUNC7:23; then A23: Integral(M,(chi(E,X))|E) =integral+(M,(chi(E,X))|E) by A21,A22,MESFUNC5:88 ; XX = dom(max- chi(E,X)) by A3,MESFUNC2:def 3; then integral+(M,max- chi(E,X)) = 0 by A3,A9,A1,MESFUNC2:26,MESFUNC5:87; then Integral(M,chi(E,X)) = 1 * M.E by A13,A20,XXREAL_3:15; hence Integral(M,chi(E,X)) = M.E by XXREAL_3:81; (chi(E,X))|E = (max+ chi(E,X))|E by MESFUNC7:23; hence thesis by A13,A17,A20,A23,XXREAL_3:81; end; theorem Th15: E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonnegative & (for x be Element of X st x in E holds f.x <= g.x) implies Integral(M,f|E) <= Integral(M,g|E) proof assume that A1: E c= dom f and A2: E c= dom g and A3: f is_measurable_on E and A4: g is_measurable_on E and A5: f is nonnegative and A6: for x be Element of X st x in E holds f.x <= g.x; set F2 = g|E; A7: E = dom(f|E) by A1,RELAT_1:62; set F1 = f|E; A8: F1 is nonnegative by A5,MESFUNC5:15; A9: E = dom(g|E) by A2,RELAT_1:62; A10: for x be Element of X st x in dom F1 holds F1.x <= F2.x proof let x be Element of X; assume A11: x in dom F1; then A12: F1.x = f.x by FUNCT_1:47; F2.x = g.x by A7,A9,A11,FUNCT_1:47; hence thesis by A6,A7,A11,A12; end; for x be object st x in dom F2 holds 0 <= F2.x proof let x be object; assume A13: x in dom F2; 0 <= F1.x by A8,SUPINF_2:51; hence thesis by A7,A9,A10,A13; end; then A14: F2 is nonnegative by SUPINF_2:52; A15: dom g /\ E = E by A2,XBOOLE_1:28; then A16: F2 is_measurable_on E by A4,MESFUNC5:42; A17: dom f /\ E = E by A1,XBOOLE_1:28; then F1 is_measurable_on E by A3,MESFUNC5:42; then integral+(M,F1) <= integral+(M,F2) by A8,A7,A9,A10,A14,A16,MESFUNC5:85; then Integral(M,F1) <= integral+(M,F2) by A3,A8,A7,A17,MESFUNC5:42,88; hence thesis by A4,A9,A14,A15,MESFUNC5:42,88; end; begin :: Selected Properties of Extended Real Sequence definition let s be ext-real-valued Function; func Partial_Sums s -> ExtREAL_sequence means :Def1: it.0=s.0 & for n be Nat holds it.(n+1) = it.n + s.(n+1); existence proof deffunc U(Nat,R_eal) = $2 + s.($1+1); consider f being sequence of ExtREAL such that A1: f.0 = s.0 & for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1: sch 12; take f; thus thesis by A1; end; uniqueness proof let s1,s2 be ExtREAL_sequence; assume that A2: s1.0=s.0 and A3: for n be Nat holds s1.(n+1)=s1.n + s.(n+1) and A4: s2.0=s.0 and A5: for n be Nat holds s2.(n+1)=s2.n + s.(n+1); defpred X[Nat] means s1.$1 = s2.$1; A6: for k be Nat st X[k] holds X[k+1] proof let k be Nat; assume s1.k =s2.k; hence s1.(k+1) = s2.k + s.(k+1) by A3 .= s2.(k+1) by A5; end; A7: X[ 0 ] by A2,A4; for n be Nat holds X[n] from NAT_1:sch 2(A7,A6); hence s1 = s2; end; end; definition let s be ext-real-valued Function; attr s is summable means Partial_Sums s is convergent; end; definition let s be ext-real-valued Function; func Sum s -> R_eal equals lim Partial_Sums s; correctness; end; theorem Th16: seq is nonnegative implies Partial_Sums seq is nonnegative & Partial_Sums seq is non-decreasing proof set PS = Partial_Sums seq; defpred P[Nat] means 0 <= PS.$1; assume A1: seq is nonnegative; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; A4: PS.(k+1) = PS.k + seq.(k+1) by Def1; seq.(k+1) >= 0 by A1,SUPINF_2:51; hence thesis by A3,A4; end; PS.0 = seq.0 by Def1; then A5: P[ 0 ] by A1,SUPINF_2:51; for m be Nat holds P[m] from NAT_1:sch 2(A5,A2); then for k be object st k in dom PS holds 0 <= PS.k; hence PS is nonnegative by SUPINF_2:52; for n,m be Nat st m <= n holds (Partial_Sums seq).m <= ( Partial_Sums seq).n proof let n,m be Nat; reconsider m1=m as Nat; defpred Q[Nat] means PS.m1 <= PS.$1; A6: for k be Nat holds PS.k <= PS.(k+1) proof let k be Nat; A7: 0 <= seq.(k+1) by A1,SUPINF_2:51; PS.(k+1) = PS.k + seq.(k+1) by Def1; hence thesis by A7,XXREAL_3:39; end; A8: for k be Nat st k >= m1 & (for l be Nat st l >= m1 & l < k holds Q[l]) holds Q[k] proof let k be Nat; assume that A9: k >= m1 and A10: for l be Nat st l >= m1 & l < k holds Q[l]; now assume k > m1; then A11: k >= m1 + 1 by NAT_1:13; per cases by A11,XXREAL_0:1; suppose k = m1 + 1; hence thesis by A6; end; suppose A12: k > m1 + 1; then reconsider l = k-1 as Element of NAT by NAT_1:20; k < k+1 by NAT_1:13; then A13: k > l by XREAL_1:19; k = l+1; then A14: PS.l <= PS.k by A6; l >= m1 by A12,XREAL_1:19; then PS.m1 <= PS.l by A10,A13; hence thesis by A14,XXREAL_0:2; end; end; hence thesis by A9,XXREAL_0:1; end; A15: for k be Nat st k >= m1 holds Q[k] from NAT_1:sch 9(A8); assume m <= n; hence thesis by A15; end; hence thesis by RINFSUP2:7; end; theorem (for n be Nat holds 0 < seq.n) implies for m be Nat holds 0 < ( Partial_Sums seq).m proof defpred P[Nat] means 0 < (Partial_Sums seq).$1; assume A1: for n be Nat holds 0 < seq.n; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; A4: (Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1) by Def1; seq.(k+1) > 0 by A1; hence thesis by A3,A4; end; (Partial_Sums seq).0 = seq.0 by Def1; then A5: P[ 0 ] by A1; thus for m be Nat holds P[m] from NAT_1:sch 2(A5,A2); end; theorem Th18: F is with_the_same_dom & (for n be Nat holds G.n = (F.n)|D) implies G is with_the_same_dom proof assume that A1: F is with_the_same_dom and A2: for n be Nat holds G.n = (F.n)|D; let n,m be Nat; G.m = (F.m)|D by A2; then A3: dom(G.m) = dom(F.m) /\ D by RELAT_1:61; G.n = (F.n)|D by A2; then dom(G.n) = dom(F.n) /\ D by RELAT_1:61; hence thesis by A1,A3; end; theorem Th19: D c= dom(F.0) & (for n be Nat holds G.n = (F.n)|D) & (for x be Element of X st x in D holds F#x is convergent) implies (lim F)|D = lim G proof assume that A1: D c= dom(F.0) and A2: for n be Nat holds G.n = (F.n)|D and A3: for x be Element of X st x in D holds F#x is convergent; G.0 = (F.0)|D by A2; then A4: dom(G.0) = D by A1,RELAT_1:62; A5: dom((lim F)|D) = dom(lim F) /\ D by RELAT_1:61; then dom((lim F)|D) = dom(F.0) /\ D by MESFUNC8:def 9; then dom((lim F)|D) = D by A1,XBOOLE_1:28; then A6: dom((lim F)|D) = dom(lim G) by A4,MESFUNC8:def 9; now let x be Element of X; assume A7: x in dom((lim F)|D); then A8: ((lim F)|D).x = (lim F).x by FUNCT_1:47; x in dom(lim F) by A5,A7,XBOOLE_0:def 4; then A9: ((lim F)|D).x = lim(F#x) by A8,MESFUNC8:def 9; A10: x in D by A7,RELAT_1:57; then A11: F#x is convergent by A3; per cases by A11; suppose A12: F#x is convergent_to_+infty; then G#x is convergent_to_+infty by A2,A10,Th12; then lim(G#x) = +infty by Th7; then (lim G).x = +infty by A6,A7,MESFUNC8:def 9; hence (lim G).x = ((lim F)|D).x by A9,A12,Th7; end; suppose A13: F#x is convergent_to_-infty; then G#x is convergent_to_-infty by A2,A10,Th12; then lim(G#x) = -infty by Th7; then (lim G).x = -infty by A6,A7,MESFUNC8:def 9; hence (lim G).x = ((lim F)|D).x by A9,A13,Th7; end; suppose A14: F#x is convergent_to_finite_number; then consider g be Real such that A15: lim(F#x) = g and A16: for p be Real st 0

Functional_Sequence of X,ExtREAL means :Def4: it.0 = F.0 & for n be Nat holds it.(n+1) = it.n + F.(n+1); existence proof defpred P[Nat,set,set] means (not $2 is PartFunc of X,ExtREAL & $3 = F.$1) or ($2 is PartFunc of X,ExtREAL & for F2 be PartFunc of X,ExtREAL st F2 = $2 holds $3 = F2 + F.($1+1)); A1: for n being Nat for x being set ex y being set st P[n,x,y] proof let n be Nat; let x be set; thus ex y be set st P[n,x,y] proof per cases; suppose A2: not x is PartFunc of X,ExtREAL; take y = F.n; thus not x is PartFunc of X,ExtREAL & y = F.n or (x is PartFunc of X ,ExtREAL & for F2 be PartFunc of X,ExtREAL st F2 = x holds y = F2 + F.(n+1)) by A2; end; suppose x is PartFunc of X,ExtREAL; then reconsider G2 = x as PartFunc of X,ExtREAL; take y = G2 + F.(n+1); thus not x is PartFunc of X,ExtREAL & y = F.n or (x is PartFunc of X ,ExtREAL & for F2 be PartFunc of X,ExtREAL st F2 = x holds y = F2 + F.(n+1)); end; end; end; consider IT being Function such that A3: dom IT = NAT & IT.0 = F.0 & for n being Nat holds P[n, IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1); now defpred IND[Nat] means IT.$1 is PartFunc of X,ExtREAL; let f be object; assume f in rng IT; then consider m be object such that A4: m in dom IT and A5: f = IT.m by FUNCT_1:def 3; reconsider m as Element of NAT by A3,A4; A6: for n be Nat st IND[n] holds IND[n+1] proof let n be Nat; assume IND[n]; then reconsider F2 = IT.n as PartFunc of X,ExtREAL; IT.(n+1) = F2 + F.(n+1) by A3; hence thesis; end; A7: IND[ 0 ] by A3; for n be Nat holds IND[n] from NAT_1:sch 2(A7,A6); then IT.m is PartFunc of X,ExtREAL; hence f in PFuncs(X,ExtREAL) by A5,PARTFUN1:45; end; then rng IT c= PFuncs(X,ExtREAL); then reconsider IT as Functional_Sequence of X,ExtREAL by A3,FUNCT_2:def 1 ,RELSET_1:4; take IT; thus thesis by A3; end; uniqueness proof let PS1,PS2 be Functional_Sequence of X,ExtREAL; assume that A8: PS1.0 = F.0 and A9: for n be Nat holds PS1.(n+1) = PS1.n + F.(n+1) and A10: PS2.0 = F.0 and A11: for n be Nat holds PS2.(n+1) = PS2.n + F.(n+1); defpred IND[Nat] means PS1.$1 = PS2.$1; A12: for n be Nat st IND[n] holds IND[n+1] proof let n be Nat; assume A13: IND[n]; PS1.(n+1) = PS1.n + F.(n+1) by A9; hence thesis by A11,A13; end; A14: IND[ 0 ] by A8,A10; for n be Nat holds IND[n] from NAT_1:sch 2(A14,A12); then for m be Element of NAT holds PS1.m = PS2.m; hence thesis; end; end; definition let X be set, F be Functional_Sequence of X,ExtREAL; attr F is additive means for n,m be Nat st n <> m holds for x be set st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or (F.m).x <> -infty; end; Lm1: z in dom((Partial_Sums F).n) & m <= n implies z in dom((Partial_Sums F).m ) proof set PF = Partial_Sums F; assume that A1: z in dom(PF.n) and A2: m <= n; defpred P[Nat] means m <= $1 & $1 <= n implies not z in dom(PF.$1); assume A3: not z in dom(PF.m); A4: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A5: P[k]; assume that A6: m <= k+1 and A7: k+1 <= n; per cases by A6,NAT_1:8; suppose A8: m <= k; PF.(k+1) = PF.k + F.(k+1) by Def4; then A9: dom(PF.(k+1)) = (dom(PF.k) /\ dom(F.(k+1))) \(((PF.k)"{-infty} /\ ( F.(k+1))"{+infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty})) by MESFUNC1:def 3; not z in dom(PF.k) /\ dom(F.(k+1)) by A5,A7,A8,NAT_1:13,XBOOLE_0:def 4; hence thesis by A9,XBOOLE_0:def 5; end; suppose m = k+1; hence thesis by A3; end; end; A10: P[ 0 ] by A3; for k be Nat holds P[k] from NAT_1:sch 2(A10,A4); hence contradiction by A1,A2; end; theorem Th22: z in dom((Partial_Sums F).n) & m <= n implies z in dom(( Partial_Sums F).m) & z in dom(F.m) proof set PF = Partial_Sums F; assume that A1: z in dom(PF.n) and A2: m <= n; thus A3: z in dom(PF.m) by A1,A2,Lm1; per cases; suppose m = 0; then PF.m = F.m by Def4; hence thesis by A1,A2,Lm1; end; suppose m <> 0; then consider k be Nat such that A4: m = k + 1 by NAT_1:6; PF.m = PF.k + F.m by A4,Def4; then dom(PF.m) = (dom(PF.k) /\ dom(F.m)) \(((PF.k)"{-infty} /\ (F.m)"{ +infty}) \/ ((PF.k)"{+infty} /\ (F.m)"{-infty})) by MESFUNC1:def 3; then z in dom(PF.k) /\ dom(F.m) by A3,XBOOLE_0:def 5; hence thesis by XBOOLE_0:def 4; end; end; theorem Th23: z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = +infty implies ex m be Nat st m <= n & (F.m).z = +infty proof set PF = Partial_Sums F; assume that A1: z in dom(PF.n) and A2: (PF.n).z = +infty; now defpred P[Nat] means $1 <= n implies (PF.$1).z <> +infty; assume A3: for m be Element of NAT st m <= n holds (F.m).z <> +infty; A4: for k being Nat st P[k] holds P[k + 1] proof let k be Nat; assume A5: P[k]; assume A6: k+1 <= n; then k <= n by NAT_1:13; then A7: z in dom(PF.k) by A1,Th22; not (PF.k).z in {+infty} by A5,A6,NAT_1:13,TARSKI:def 1; then not z in (PF.k)"{+infty} by FUNCT_1:def 7; then A8: not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} by XBOOLE_0:def 4; z in dom(F.(k+1)) by A1,A6,Th22; then A9: z in dom(PF.k) /\ dom(F.(k+1)) by A7,XBOOLE_0:def 4; A10: PF.(k+1) = PF.k + F.(k+1) by Def4; A11: (F.(k+1)).z <> +infty by A3,A6; then not (F.(k+1)).z in {+infty} by TARSKI:def 1; then not z in (F.(k+1))"{+infty} by FUNCT_1:def 7; then not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} by XBOOLE_0:def 4; then not z in ((PF.k)"{+infty} /\ (F.(k+1))"{-infty}) \/ ((PF.k)"{-infty } /\ (F.(k+1))"{+infty}) by A8,XBOOLE_0:def 3; then z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{+infty} /\ (F.(k+1))"{ -infty}) \/ ((PF.k)"{-infty} /\ (F.(k+1))"{+infty})) by A9,XBOOLE_0:def 5; then z in dom(PF.(k+1)) by A10,MESFUNC1:def 3; then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by A10,MESFUNC1:def 3; hence thesis by A5,A6,A11,NAT_1:13,XXREAL_3:16; end; PF.0 = F.0 by Def4; then A12: P[ 0 ] by A3; for k being Nat holds P[k] from NAT_1:sch 2(A12,A4); hence contradiction by A2; end; hence thesis; end; theorem F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = +infty & m <= n implies (F.m).z <> -infty proof assume that A1: F is additive and A2: z in dom((Partial_Sums F).n) and A3: ((Partial_Sums F).n).z = +infty and A4: m <= n; A5: z in dom(F.m) by A2,A4,Th22; consider k be Nat such that A6: k <= n and A7: (F.k).z = +infty by A2,A3,Th23; z in dom(F.k) by A2,A6,Th22; then z in dom(F.m) /\ dom(F.k) by A5,XBOOLE_0:def 4; hence thesis by A1,A7; end; theorem Th25: z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = -infty implies ex m be Nat st m <= n & (F.m).z = -infty proof set PF = Partial_Sums F; assume that A1: z in dom(PF.n) and A2: (PF.n).z = -infty; now defpred P[Nat] means $1 <= n implies (PF.$1).z <> -infty; assume A3: for m be Nat st m <= n holds (F.m).z <> -infty; A4: for k being Nat st P[k] holds P[k + 1] proof let k be Nat; assume A5: P[k]; assume A6: k+1 <= n; then k <= n by NAT_1:13; then A7: z in dom(PF.k) by A1,Th22; not (PF.k).z in {-infty} by A5,A6,NAT_1:13,TARSKI:def 1; then not z in (PF.k)"{-infty} by FUNCT_1:def 7; then A8: not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} by XBOOLE_0:def 4; z in dom(F.(k+1)) by A1,A6,Th22; then A9: z in dom(PF.k) /\ dom(F.(k+1)) by A7,XBOOLE_0:def 4; A10: PF.(k+1) = PF.k + F.(k+1) by Def4; A11: (F.(k+1)).z <> -infty by A3,A6; then not (F.(k+1)).z in {-infty} by TARSKI:def 1; then not z in (F.(k+1))"{-infty} by FUNCT_1:def 7; then not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} by XBOOLE_0:def 4; then not z in ((PF.k)"{-infty} /\ (F.(k+1))"{+infty}) \/ ((PF.k)"{+infty } /\ (F.(k+1))"{-infty}) by A8,XBOOLE_0:def 3; then z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{-infty} /\ (F.(k+1))"{ +infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty})) by A9,XBOOLE_0:def 5; then z in dom(PF.(k+1)) by A10,MESFUNC1:def 3; then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by A10,MESFUNC1:def 3; hence thesis by A5,A6,A11,NAT_1:13,XXREAL_3:17; end; PF.0 = F.0 by Def4; then A12: P[ 0 ] by A3; for k being Nat holds P[k] from NAT_1:sch 2(A12,A4); hence contradiction by A2; end; hence thesis; end; theorem F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = -infty & m <= n implies (F.m).z <> +infty proof assume A1: F is additive; assume that A2: z in dom((Partial_Sums F).n) and A3: ((Partial_Sums F).n).z = -infty; assume m <= n; then A4: z in dom(F.m) by A2,Th22; consider k be Nat such that A5: k <= n and A6: (F.k).z = -infty by A2,A3,Th25; z in dom(F.k) by A2,A5,Th22; then z in dom(F.m) /\ dom(F.k) by A4,XBOOLE_0:def 4; hence thesis by A1,A6; end; theorem Th27: F is additive implies ((Partial_Sums F).n)"{-infty} /\ (F.(n+1)) "{+infty} = {} & ((Partial_Sums F).n)"{+infty} /\ (F.(n+1))"{-infty} = {} proof set PF = Partial_Sums F; assume A1: F is additive; now given z be object such that A2: z in (PF.n)"{-infty} and A3: z in (F.(n+1))"{+infty}; A4: z in dom(PF.n) by A2,FUNCT_1:def 7; (PF.n).z in {-infty} by A2,FUNCT_1:def 7; then (PF.n).z = -infty by TARSKI:def 1; then consider k be Nat such that A5: k <= n and A6: (F.k).z = -infty by A4,Th25; A7: z in dom(F.(n+1)) by A3,FUNCT_1:def 7; (F.(n+1)).z in {+infty} by A3,FUNCT_1:def 7; then A8: (F.(n+1)).z = +infty by TARSKI:def 1; z in dom(F.k) by A4,A5,Th22; then z in dom(F.k) /\ dom(F.(n+1)) by A7,XBOOLE_0:def 4; hence contradiction by A1,A8,A6; end; then (PF.n)"{-infty} misses (F.(n+1))"{+infty} by XBOOLE_0:3; hence (PF.n)"{-infty} /\ (F.(n+1))"{+infty} = {} by XBOOLE_0:def 7; now given z be object such that A9: z in (PF.n)"{+infty} and A10: z in (F.(n+1))"{-infty}; A11: z in dom(PF.n) by A9,FUNCT_1:def 7; (PF.n).z in {+infty} by A9,FUNCT_1:def 7; then (PF.n).z = +infty by TARSKI:def 1; then consider k be Nat such that A12: k <= n and A13: (F.k).z = +infty by A11,Th23; A14: z in dom(F.(n+1)) by A10,FUNCT_1:def 7; (F.(n+1)).z in {-infty} by A10,FUNCT_1:def 7; then A15: (F.(n+1)).z = -infty by TARSKI:def 1; z in dom(F.k) by A11,A12,Th22; then z in dom(F.k) /\ dom(F.(n+1)) by A14,XBOOLE_0:def 4; hence contradiction by A1,A15,A13; end; then (PF.n)"{+infty} misses (F.(n+1))"{-infty} by XBOOLE_0:3; hence thesis by XBOOLE_0:def 7; end; theorem Th28: F is additive implies dom((Partial_Sums F).n) = meet{dom(F.k) where k is Element of NAT : k <= n} proof deffunc DOM1(Nat) = {dom(F.k) where k is Element of NAT : k <= $1}; set PF = Partial_Sums F; defpred P[Nat] means dom(PF.$1) = meet {dom(F.k) where k is Element of NAT : k <= $1}; A1: dom(PF.0) = dom(F.0) by Def4; now let V be object; assume V in DOM1(0); then consider k be Element of NAT such that A2: V = dom(F.k) and A3: k <= 0; k = 0 by A3; hence V in {dom(F.0)} by A2,TARSKI:def 1; end; then A4: DOM1(0) c= {dom(F.0)}; assume A5: F is additive; A6: for m be Nat st P[m] holds P[m+1] proof let m be Nat; A7: PF.(m+1) = PF.m + F.(m+1) by Def4; A8: (PF.m)"{+infty} /\ (F.(m+1))"{-infty} = {} by A5,Th27; A9: dom(F.0) in DOM1(m+1); now let V be object; assume A10: V in meet DOM1(m) /\ dom(F.(m+1)); then A11: V in dom(F.(m+1)) by XBOOLE_0:def 4; A12: V in meet DOM1(m) by A10,XBOOLE_0:def 4; for W be set holds W in DOM1(m+1) implies V in W proof let W be set; assume W in DOM1(m+1); then consider i be Element of NAT such that A13: W = dom(F.i) and A14: i <= m+1; now assume i <= m; then W in DOM1(m) by A13; hence thesis by A12,SETFAM_1:def 1; end; hence thesis by A11,A13,A14,NAT_1:8; end; hence V in meet DOM1(m+1) by A9,SETFAM_1:def 1; end; then A15: meet DOM1(m) /\ dom(F.(m+1)) c= meet DOM1(m+1); A16: dom(F.0) in DOM1(m); now now let V be object; assume V in DOM1(m); then consider i be Element of NAT such that A17: V = dom(F.i) and A18: i <= m; i <= m+1 by A18,NAT_1:12; hence V in DOM1(m+1) by A17; end; then DOM1(m) c= DOM1(m+1); then A19: meet DOM1(m+1) c= meet DOM1(m) by A16,SETFAM_1:6; let V be object; assume A20: V in meet DOM1(m+1); dom(F.(m+1)) in DOM1(m+1); then V in dom(F.(m+1)) by A20,SETFAM_1:def 1; hence V in meet DOM1(m) /\ dom(F.(m+1)) by A20,A19,XBOOLE_0:def 4; end; then A21: meet DOM1(m+1) c= meet DOM1(m) /\ dom(F.(m+1)); (PF.m)"{-infty} /\ (F.(m+1))"{+infty} = {} by A5,Th27; then A22: dom(PF.(m+1)) = (dom(PF.m)/\dom(F.(m+1))) \ ({}\/{}) by A8,A7, MESFUNC1:def 3; assume P[m]; hence thesis by A22,A21,A15,XBOOLE_0:def 10; end; now let V be object; assume V in {dom(F.0)}; then V = dom(F.0) by TARSKI:def 1; hence V in DOM1(0); end; then {dom(F.0)} c= DOM1(0); then DOM1(0) = {dom(F.0)} by A4,XBOOLE_0:def 10; then A23: P[ 0 ] by A1,SETFAM_1:10; for k be Nat holds P[k] from NAT_1:sch 2(A23,A6); hence thesis; end; theorem Th29: F is additive & F is with_the_same_dom implies dom((Partial_Sums F).n) = dom(F.0) proof assume that A1: F is additive and A2: F is with_the_same_dom; now let D be object; A3: dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n}; assume D in meet {dom(F.k) where k is Element of NAT : k <= n}; then D in dom(F.0) by A3,SETFAM_1:def 1; hence D in meet {dom(F.0)} by SETFAM_1:10; end; then A4: meet{dom(F.k) where k is Element of NAT : k <= n} c= meet{dom(F.0)}; now let D be object; assume D in meet {dom(F.0)}; then A5: D in dom(F.0) by SETFAM_1:10; A6: for E be set holds E in {dom(F.k) where k is Element of NAT : k <= n} implies D in E proof let E be set; assume E in {dom(F.k) where k is Element of NAT : k <= n}; then ex k1 be Element of NAT st E = dom(F.k1) & k1 <= n; hence thesis by A2,A5; end; dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n}; hence D in meet {dom(F.k) where k is Element of NAT : k <= n} by A6, SETFAM_1:def 1; end; then meet{dom(F.0)} c= meet {dom(F.k) where k is Element of NAT : k <= n}; then meet{dom(F.k) where k is Element of NAT : k <= n} = meet {dom(F.0)} by A4,XBOOLE_0:def 10; then dom((Partial_Sums F).n) = meet{dom(F.0)} by A1,Th28; hence thesis by SETFAM_1:10; end; theorem Th30: (for n be Nat holds F.n is nonnegative) implies F is additive by SUPINF_2:51; theorem Th31: F is additive & (for n holds G.n = (F.n)|D) implies G is additive proof assume that A1: F is additive and A2: for n holds G.n = (F.n)|D; let n,m be Nat; A3: G.m = (F.m)|D by A2; then A4: dom(G.m) c= dom(F.m) by RELAT_1:60; assume n <> m; let x be set; assume A5: x in dom(G.n) /\ dom(G.m); then A6: x in dom(G.m) by XBOOLE_0:def 4; A7: G.n = (F.n)|D by A2; then dom(G.n) c= dom(F.n) by RELAT_1:60; then dom(G.n) /\ dom(G.m) c= dom(F.n) /\ dom(F.m) by A4,XBOOLE_1:27; then A8: (F.n).x <> +infty or (F.m).x <> -infty by A1,A5; x in dom(G.n) by A5,XBOOLE_0:def 4; hence thesis by A7,A3,A8,A6,FUNCT_1:47; end; theorem Th32: F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D implies (Partial_Sums(F#x)).n = ((Partial_Sums F)#x).n proof set PF = Partial_Sums F; set PFx = Partial_Sums(F#x); assume that A1: F is additive and A2: F is with_the_same_dom and A3: D c= dom(F.0) and A4: x in D; defpred P[Nat] means PFx.$1 = (PF#x).$1; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; PFx.(k+1) = PFx.k + (F#x).(k+1) by Def1; then PFx.(k+1) = (PF#x).k + (F.(k+1)).x by A6,MESFUNC5:def 13; then A7: PFx.(k+1) = (PF.k).x + (F.(k+1)).x by MESFUNC5:def 13; A8: PF.(k+1) = PF.k + F.(k+1) by Def4; D c= dom(PF.(k+1)) by A1,A2,A3,Th29; then PFx.(k+1) = (PF.(k+1)).x by A4,A8,A7,MESFUNC1:def 3; hence thesis by MESFUNC5:def 13; end; PFx.0 = (F#x).0 by Def1; then PFx.0 = (F.0).x by MESFUNC5:def 13; then PFx.0 = (PF.0).x by Def4; then A9: P[ 0 ] by MESFUNC5:def 13; for k being Nat holds P[k] from NAT_1:sch 2(A9,A5); hence thesis; end; theorem Th33: F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D implies ( Partial_Sums(F#x) is convergent_to_finite_number iff (Partial_Sums F) #x is convergent_to_finite_number ) & ( Partial_Sums(F#x) is convergent_to_+infty iff (Partial_Sums F)#x is convergent_to_+infty ) & ( Partial_Sums(F#x) is convergent_to_-infty iff (Partial_Sums F)#x is convergent_to_-infty ) & ( Partial_Sums(F#x) is convergent iff (Partial_Sums F) #x is convergent ) proof set PFx = Partial_Sums(F#x); set PF = Partial_Sums F; assume that A1: F is additive and A2: F is with_the_same_dom and A3: D c= dom(F.0) and A4: x in D; thus A5: now assume PFx is convergent_to_finite_number; then consider g be Real such that A6: for p be Real st 0

m; F.n is_simple_func_in S by A1; then F.n is without+infty by MESFUNC5:14; hence for x be set st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or (F.m).x <> -infty; end; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; F.(k+1) is_simple_func_in S by A1; then (Partial_Sums F).k + F.(k+1) is_simple_func_in S by A3,MESFUNC5:38; hence thesis by Def4; end; (Partial_Sums F).0 = F.0 by Def4; then A4: P[ 0 ] by A1; for k be Nat holds P[k] from NAT_1:sch 2(A4,A2); hence thesis; end; theorem Th36: (for m be Nat holds F.m is nonnegative) implies (Partial_Sums F) .n is nonnegative proof defpred P[Nat] means (Partial_Sums F).$1 is nonnegative; assume A1: for m be Nat holds F.m is nonnegative; A2: now let k be Nat; assume A3: P[k]; A4: (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4; F.(k+1) is nonnegative by A1; hence P[k+1] by A3,A4,MESFUNC5:22; end; (Partial_Sums F).0 = F.0 by Def4; then A5: P[ 0 ] by A1; for k being Nat holds P[k] from NAT_1:sch 2(A5,A2); hence thesis; end; theorem Th37: F is with_the_same_dom & x in dom(F.0) & (for k be Nat holds F.k is nonnegative) & n <= m implies ((Partial_Sums F).n).x <= ((Partial_Sums F).m) .x proof assume A1: F is with_the_same_dom; set PF = Partial_Sums F; assume A2: x in dom(F.0); defpred P[Nat] means (PF.n).x <= (PF.$1).x; assume A3: for m be Nat holds F.m is nonnegative; A4: for k be Nat holds (PF.k).x <= (PF.(k+1)).x proof let k be Nat; A5: PF.(k+1) = PF.k + F.(k+1) by Def4; F.(k+1) is nonnegative by A3; then A6: 0. <= (F.(k+1)).x by SUPINF_2:39; dom(PF.(k+1)) = dom(F.0) by A1,A3,Th29,Th30; then (PF.(k+1)).x = (PF.k).x + (F.(k+1)).x by A2,A5,MESFUNC1:def 3; hence thesis by A6,XXREAL_3:39; end; A7: for k be Nat st k >= n & (for l be Nat st l >= n & l < k holds P[l]) holds P[k] proof let k be Nat; assume that A8: k >= n and A9: for l be Nat st l >= n & l < k holds P[l]; now A10: now assume A11: k > n+1; then reconsider l = k-1 as Element of NAT by NAT_1:20; k < k+1 by NAT_1:13; then A12: k > l by XREAL_1:19; k = l+1; then A13: (PF.l).x <= (PF.k).x by A4; l >= n by A11,XREAL_1:19; then (PF.n).x <= (PF.l).x by A9,A12; hence thesis by A13,XXREAL_0:2; end; assume k > n; then k >= n + 1 by NAT_1:13; then k = n+1 or k > n+1 by XXREAL_0:1; hence thesis by A4,A10; end; hence thesis by A8,XXREAL_0:1; end; A14: for k being Nat st k >= n holds P[k] from NAT_1:sch 9(A7); assume n <= m; hence thesis by A14; end; theorem Th38: F is with_the_same_dom & x in dom(F.0) & (for m be Nat holds F.m is nonnegative) implies (Partial_Sums F)#x is non-decreasing & (Partial_Sums F) #x is convergent proof assume A1: F is with_the_same_dom; assume A2: x in dom(F.0); assume A3: for m be Nat holds F.m is nonnegative; for n,m be Nat st m<=n holds ((Partial_Sums F)#x).m <= (( Partial_Sums F)#x).n proof let n,m be Nat; assume m <= n; then ((Partial_Sums F).m).x <= ((Partial_Sums F).n).x by A1,A2,A3,Th37; then ((Partial_Sums F)#x).m <= ((Partial_Sums F).n).x by MESFUNC5:def 13; hence thesis by MESFUNC5:def 13; end; hence ((Partial_Sums F)#x) is non-decreasing by RINFSUP2:7; hence thesis by RINFSUP2:37; end; theorem Th39: (for m be Nat holds F.m is without-infty) implies (Partial_Sums F).n is without-infty proof defpred P[Nat] means (Partial_Sums F).$1 is without-infty; assume A1: for m be Nat holds F.m is without-infty; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; A4: F.(k+1) is without-infty by A1; (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4; hence thesis by A3,A4,Th3; end; (Partial_Sums F).0 = F.0 by Def4; then A5: P[ 0 ] by A1; for k being Nat holds P[k] from NAT_1:sch 2(A5,A2); hence thesis; end; theorem (for m be Nat holds F.m is without+infty) implies (Partial_Sums F).n is without+infty proof defpred P[Nat] means (Partial_Sums F).$1 is without+infty; assume A1: for m be Nat holds F.m is without+infty; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; A4: F.(k+1) is without+infty by A1; (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4; hence thesis by A3,A4,Th4; end; (Partial_Sums F).0 = F.0 by Def4; then A5: P[ 0 ] by A1; for k being Nat holds P[k] from NAT_1:sch 2(A5,A2); hence thesis; end; theorem Th41: (for n be Nat holds F.n is_measurable_on E & F.n is without-infty) implies (Partial_Sums F).m is_measurable_on E proof set PF = Partial_Sums F; defpred P[Nat] means PF.$1 is_measurable_on E; assume A1: for n be Nat holds F.n is_measurable_on E & F.n is without-infty; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; A4: F.(k+1) is_measurable_on E by A1; A5: F.(k+1) is without-infty by A1; PF.k is without-infty by A1,Th39; then PF.k + F.(k+1) is_measurable_on E by A3,A4,A5,MESFUNC5:31; hence thesis by Def4; end; PF.0 = F.0 by Def4; then A6: P[ 0 ] by A1; for k being Nat holds P[k] from NAT_1:sch 2(A6,A2); hence thesis; end; theorem Th42: F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in dom(F.0) /\ dom(G.0) & (for k be Nat, y be Element of X st y in dom(F.0) /\ dom(G.0) holds (F.k).y <= (G.k).y) implies ((Partial_Sums F).n).x <= ((Partial_Sums G).n).x proof assume that A1: F is additive and A2: F is with_the_same_dom and A3: G is additive and A4: G is with_the_same_dom and A5: x in dom(F.0) /\ dom(G.0) and A6: for k be Nat, y be Element of X st y in dom(F.0) /\ dom(G.0) holds ( F.k).y <= (G.k).y; set PG = Partial_Sums G; set PF = Partial_Sums F; defpred P[Nat] means (PF.$1).x <= (PG.$1).x; A7: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A8: P[k]; dom(PF.(k+1)) = dom(F.0) by A1,A2,Th29; then A9: x in dom(PF.(k+1)) by A5,XBOOLE_0:def 4; dom(PG.(k+1)) = dom(G.0) by A3,A4,Th29; then A10: x in dom(PG.(k+1)) by A5,XBOOLE_0:def 4; PG.(k+1) = PG.k + G.(k+1) by Def4; then A11: (PG.(k+1)).x = (PG.k).x + (G.(k+1)).x by A10,MESFUNC1:def 3; PF.(k+1) = PF.k + F.(k+1) by Def4; then A12: (PF.(k+1)).x = (PF.k).x + (F.(k+1)).x by A9,MESFUNC1:def 3; (F.(k+1)).x <= (G.(k+1)).x by A5,A6; hence thesis by A8,A12,A11,XXREAL_3:36; end; A13: (PG.0) = G.0 by Def4; (PF.0) = F.0 by Def4; then A14: P[ 0 ] by A5,A6,A13; for k being Nat holds P[k] from NAT_1:sch 2(A14,A7); hence thesis; end; theorem Th43: for X be non empty set, F be Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom holds Partial_Sums F is with_the_same_dom proof let X be non empty set, F be Functional_Sequence of X,ExtREAL; assume that A1: F is additive and A2: F is with_the_same_dom; let n,m be Nat; dom((Partial_Sums F).n) = dom(F.0) by A1,A2,Th29; hence thesis by A1,A2,Th29; end; theorem Th44: dom(F.0) = E & F is additive & F is with_the_same_dom & (for n be Nat holds (Partial_Sums F).n is_measurable_on E) & (for x be Element of X st x in E holds F#x is summable) implies lim(Partial_Sums F) is_measurable_on E proof assume that A1: dom(F.0) = E and A2: F is additive and A3: F is with_the_same_dom and A4: for n be Nat holds (Partial_Sums F).n is_measurable_on E and A5: for x be Element of X st x in E holds F#x is summable; reconsider PF = Partial_Sums F as with_the_same_dom Functional_Sequence of X ,ExtREAL by A2,A3,Th43; A6: now let x be Element of X; assume A7: x in E; then F#x is summable by A5; then Partial_Sums(F#x) is convergent; hence PF#x is convergent by A1,A2,A3,A7,Th33; end; dom((Partial_Sums F).0) = E by A1,A2,A3,Th29; hence thesis by A4,A6,MESFUNC8:25; end; theorem (for n be Nat holds F.n is_integrable_on M) implies for m be Nat holds (Partial_Sums F).m is_integrable_on M proof set PF = Partial_Sums F; defpred P1[Nat] means PF.$1 is_integrable_on M; assume A1: for n be Nat holds F.n is_integrable_on M; A2: for k be Nat st P1[k] holds P1[k+1] proof let k be Nat; assume A3: P1[k]; F.(k+1) is_integrable_on M by A1; then PF.k + F.(k+1) is_integrable_on M by A3,MESFUNC5:108; hence thesis by Def4; end; PF.0 = F.0 by Def4; then A4: P1[ 0 ] by A1; thus for m be Nat holds P1[m] from NAT_1:sch 2(A4,A2); end; theorem Th46: E = dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat holds F.n is_measurable_on E & F.n is nonnegative & I.n = Integral(M,F.n )) implies Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m proof assume that A1: E = dom(F.0) and A2: F is additive and A3: F is with_the_same_dom and A4: for n be Nat holds F.n is_measurable_on E & F.n is nonnegative & I.n = Integral(M,F.n); set PF = Partial_Sums F; A5: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12; thus Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m proof set PI = Partial_Sums I; defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1; A6: for k be Nat st P2[k] holds P2[k+1] proof let k be Nat; assume A7: P2[k]; A8: F.(k+1) is_measurable_on E by A4; A9: dom(F.(k+1)) = E by A1,A3; A10: PF.(k+1) is_measurable_on E by A4,A5,Th41; A11: PF.(k+1) is nonnegative by A4,Th36; A12: F.(k+1) is nonnegative by A4; A13: PF.k is nonnegative by A4,Th36; A14: dom(PF.k) = E by A1,A2,A3,Th29; A15: PF.k is_measurable_on E by A4,A5,Th41; then consider D be Element of S such that A16: D = dom(PF.k + F.(k+1)) and A17: integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+ (M,( F.(k+1))|D) by A14,A9,A8,A13,A12,MESFUNC5:78; A18: D = E /\ E by A14,A9,A13,A12,A16,MESFUNC5:22; then A19: (PF.k)|D = PF.k by A14; A20: (F.(k+1))|D = F.(k+1) by A9,A18; dom(PF.(k+1)) = E by A1,A2,A3,Th29; then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by A10,A11,MESFUNC5:88 .= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A17,Def4 .= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A14,A15,A13,A19, MESFUNC5:88 .= Integral(M,PF.k) + Integral(M,F.(k+1)) by A9,A8,A12,A20,MESFUNC5:88 .= PI.k + I.(k+1) by A4,A7; hence thesis by Def1; end; Integral(M,PF.0) = Integral(M,F.0) by Def4; then Integral(M,PF.0) = I.0 by A4; then A21: P2[ 0 ] by Def1; for k be Nat holds P2[k] from NAT_1:sch 2(A21,A6); hence thesis; end; end; begin :: Sequence of Measurable Functions Lm2: E c= dom f & f is_measurable_on E & E ={} & (for n be Nat holds F.n is_simple_func_in S) implies ex I be ExtREAL_sequence st (for n be Nat holds I. n = Integral(M,(F.n)|E)) & I is summable & Integral(M,f|E) = Sum(I) proof assume that A1: E c= dom f and A2: f is_measurable_on E and A3: E ={} and A4: for n be Nat holds F.n is_simple_func_in S; take I = NAT --> 0.; A5: M.E = 0 by A3,VALUED_0:def 19; thus for n be Nat holds I.n = Integral(M,(F.n)|E) proof let n be Nat; reconsider m = n as Element of NAT by ORDINAL1:def 12; reconsider D = dom(F.m) as Element of S by A4,MESFUNC5:37; F.m is_measurable_on D by A4,MESFUNC2:34; then Integral(M,(F.m)|E) = 0 by A5,MESFUNC5:94; hence thesis by FUNCOP_1:7; end; defpred P[Nat] means (Partial_Sums I).$1 = 0; A6: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A7: P[k]; A8: I.(k+1) = 0 by FUNCOP_1:7; (Partial_Sums I).(k+1) = (Partial_Sums I).k + I.(k+1) by Def1; hence thesis by A7,A8; end; (Partial_Sums I).0 = I.0 by Def1; then A9: P[ 0 ] by FUNCOP_1:7; A10: for k being Nat holds P[k] from NAT_1:sch 2(A9,A6); A11: for n be Nat holds (Partial_Sums I).n = 0 by A10; then A12: lim(Partial_Sums I) = 0 by MESFUNC5:52; Partial_Sums I is convergent_to_finite_number by A11,MESFUNC5:52; then Partial_Sums I is convergent; hence I is summable; A13: E = dom(f|E) by A1,RELAT_1:62; then E = dom f /\ E by RELAT_1:61; then Integral(M,(f|E)|E) = 0 by A2,A5,A13,MESFUNC5:42,94; hence thesis by A12; end; Lm3: E c= dom f & f is nonnegative & f is_measurable_on E & F is additive & E common_on_dom F & (for n be Nat holds F.n is_simple_func_in S & F.n is nonnegative ) & (for x be Element of X st x in E holds F#x is summable & f.x = Sum(F#x)) implies ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,f|E) = Sum(I) proof assume that A1: E c= dom f and A2: f is nonnegative and A3: f is_measurable_on E and A4: F is additive and A5: E common_on_dom F and A6: for n be Nat holds F.n is_simple_func_in S & F.n is nonnegative and A7: for x be Element of X st x in E holds F#x is summable & f.x = Sum(F# x); deffunc G1(Nat) = (F.$1)|E; consider g1 be Functional_Sequence of X,ExtREAL such that A8: for n be Nat holds g1.n = G1(n) from SEQFUNC:sch 1; A9: for n be Nat holds (F.n)|E is_simple_func_in S & (F.n)|E is nonnegative & dom((F.n)|E) = E proof let n be Nat; reconsider n9=n as Element of NAT by ORDINAL1:def 12; thus (F.n)|E is_simple_func_in S by A6,MESFUNC5:34; thus (F.n)|E is nonnegative by A6,MESFUNC5:15; E c= dom(F.n9) by A5,SEQFUNC:def 9; hence thesis by RELAT_1:62; end; for n,m be Nat holds dom(g1.n) = dom(g1.m) proof let n,m be Nat; dom(g1.m) = dom((F.m)|E) by A8; then A10: dom(g1.m) = E by A9; dom(g1.n) = dom((F.n)|E) by A8; hence thesis by A9,A10; end; then A11: g1 is with_the_same_dom; set G = Partial_Sums g1; deffunc I(Element of NAT) = Integral(M,g1.$1); consider I be ExtREAL_sequence such that A12: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4; take I; A13: dom(f|E) = E by A1,RELAT_1:62; then dom f /\ E = E by RELAT_1:61; then A14: f|E is_measurable_on E by A3,MESFUNC5:42; set L = Partial_Sums I; A15: for n be Nat holds I.n = Integral(M,(F.n)|E) proof let n be Nat; reconsider m = n as Element of NAT by ORDINAL1:def 12; I.m = Integral(M,g1.m) by A12; hence thesis by A8; end; A16: for k be Nat holds g1.k is nonnegative proof let k be Nat; (F.k)|E is nonnegative by A9; hence thesis by A8; end; A17: for n be Nat holds G.n is_simple_func_in S & G.n is nonnegative & dom(G. n)=E proof let n be Nat; A18: for n be Nat holds g1.n is_simple_func_in S proof let n be Nat; (F.n)|E is_simple_func_in S by A9; hence thesis by A8; end; hence G.n is_simple_func_in S by Th35; thus G.n is nonnegative by A16,Th36; dom(g1.0) = dom((F.0)|E) by A8; then dom(g1.0) = E by A9; hence thesis by A11,A18,Th29,Th35; end; G.0 = g1.0 by Def4; then A19: G.0 = (F.0)|E by A8; A20: for n be Nat holds integral'(M,G.n) = L.n proof defpred L[Nat] means L.$1 = integral'(M,G.$1); let n be Nat; A21: G.0 is nonnegative by A17; A22: for k be Nat st L[k] holds L[k+1] proof let k be Nat; assume A23: L[k]; L.(k+1) = (Partial_Sums I).k + I.(k+1) by Def1; then A24: L.(k+1) = integral'(M,G.k) + Integral(M,(F.(k+1))|E) by A15,A23; A25: (F.(k+1))|E is_simple_func_in S by A9; A26: dom((F.(k+1))|E) = E by A9; A27: G.k is_simple_func_in S by A17; G.(k+1) = G.k + g1.(k+1) by Def4; then A28: G.(k+1) = G.k + (F.(k+1))|E by A8; A29: (F.(k+1))|E is nonnegative by A9; A30: G.k is nonnegative by A17; A31: dom(G.k) = E by A17; then E = dom(G.k) /\ dom((F.(k+1))|E) by A26; then dom( G.k + (F.(k+1))|E ) = E by A25,A29,A27,A30,MESFUNC5:65; then A32: integral'(M,G.k + (F.(k+1))|E) = integral'(M,(G.k)|E) + integral'(M ,((F.(k+1))|E)|E) by A25,A29,A27,A30,MESFUNC5:65; (G.k)|E = G.k by A31; hence thesis by A28,A24,A25,A29,A32,MESFUNC5:89; end; L.0 = I.0 by Def1; then A33: L.0 = Integral(M,G.0) by A15,A19; G.0 is_simple_func_in S by A17; then A34: L[ 0 ] by A33,A21,MESFUNC5:89; A35: for k be Nat holds L[k] from NAT_1:sch 2(A34,A22); thus thesis by A35; end; g1.0 = (F.0)|E by A8; then A36: dom(g1.0) = E by A9; A37: for x be Element of X st x in dom(f|E) holds g1#x is summable & (f|E).x = Sum(g1#x) proof let x be Element of X; assume A38: x in dom(f|E); then A39: f.x = (f|E).x by FUNCT_1:47; A40: for n be object st n in NAT holds (F#x).n = (g1#x).n proof let n be object; assume n in NAT; then reconsider n1 = n as Nat; A41: (F#x).n = (F.n1).x by MESFUNC5:def 13; A42: dom((F.n1)|E) = E by A9; (F.n1)|E = g1.n1 by A8; then (g1.n1).x = (F.n1).x by A13,A38,A42,FUNCT_1:47; hence thesis by A41,MESFUNC5:def 13; end; A43: f.x = Sum(F#x) by A7,A13,A38; F#x is summable by A7,A13,A38; hence thesis by A43,A39,A40,FUNCT_2:12; end; A44: f|E is nonnegative by A2,MESFUNC5:15; then consider F be Functional_Sequence of X,ExtREAL, K be ExtREAL_sequence such that A45: for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom(f|E) and A46: for n be Nat holds F.n is nonnegative and A47: for n,m be Nat st n <=m holds for x be Element of X st x in dom(f| E) holds (F.n).x <= (F.m).x and A48: for x be Element of X st x in dom(f|E) holds F#x is convergent & lim(F#x) = (f|E).x and A49: for n be Nat holds K.n=integral'(M,F.n) and K is convergent and A50: integral+(M,(f|E))=lim K by A13,A14,MESFUNC5:def 15; A51: g1 is additive by A4,A8,Th31; A52: for x be Element of X st x in E holds F#x is convergent & G#x is convergent & lim(F#x) = lim(G#x) proof let x be Element of X; assume A53: x in E; hence F#x is convergent by A13,A48; g1#x is summable by A13,A37,A53; then Partial_Sums(g1#x) is convergent; hence G#x is convergent by A11,A51,A36,A53,Th33; A54: (f|E).x = Sum(g1#x) by A13,A37,A53; g1#x is summable by A13,A37,A53; then lim(G#x) = (f|E).x by A4,A13,A8,A11,A36,A53,A54,Th31,Th34; hence thesis by A13,A48,A53; end; A55: for n,m be Nat st n <=m holds for x be Element of X st x in E holds (G.n ).x <= (G.m).x by A11,A16,A36,Th37; then A56: L is convergent by A13,A17,A20,A45,A46,A47,A49,A52,MESFUNC5:76; lim L = integral+(M,(f|E)) by A13,A17,A20,A45,A46,A47,A49,A50,A55,A52, MESFUNC5:76; hence thesis by A13,A15,A14,A44,A56,MESFUNC5:88; end; theorem E c= dom f & f is nonnegative & f is_measurable_on E & F is additive & (for n holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom(F.n)) & ( for x st x in E holds F#x is summable & f.x = Sum(F#x)) implies ex I be ExtREAL_sequence st (for n holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,f|E) = Sum I proof assume that A1: E c= dom f and A2: f is nonnegative and A3: f is_measurable_on E and A4: F is additive and A5: for n holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom (F.n) and A6: for x st x in E holds F#x is summable & f.x = Sum(F#x); per cases; suppose E = {}; hence thesis by A1,A3,A5,Lm2; end; suppose A7: E <> {}; for n be Nat holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom(F.n) by A5; then E common_on_dom F by A7,SEQFUNC:def 9; hence thesis by A1,A2,A3,A4,A5,A6,Lm3; end; end; theorem E c= dom f & f is nonnegative & f is_measurable_on E implies ex g be Functional_Sequence of X,ExtREAL st g is additive & (for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n is_measurable_on E) & (for x be Element of X st x in E holds g#x is summable & f.x = Sum(g#x)) & ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,(g.n)|E)) & I is summable & Integral(M,f|E) = Sum I proof assume that A1: E c= dom f and A2: f is nonnegative and A3: f is_measurable_on E; set F = f|E; A4: dom F = E by A1,RELAT_1:62; E = dom f /\ E by A1,XBOOLE_1:28; then F is_measurable_on E by A3,MESFUNC5:42; then consider h be Functional_Sequence of X,ExtREAL such that A5: for n be Nat holds h.n is_simple_func_in S & dom(h.n) = dom F and A6: for n be Nat holds h.n is nonnegative and A7: for n,m be Nat st n <=m holds for x be Element of X st x in dom F holds (h.n).x <= (h.m).x and A8: for x be Element of X st x in dom F holds (h#x) is convergent & lim (h#x) = F.x by A2,A4,MESFUNC5:15,64; defpred P[Nat,set,set] means $3 = h.($1+1) - h.$1; A9: for n being Nat for x being set ex y being set st P[n,x,y]; consider g being Function such that A10: dom g = NAT & g.0 = h.0 & for n being Nat holds P[n,g.n, g.(n+1)] from RECDEF_1:sch 1(A9); now defpred IND[Nat] means g.$1 is PartFunc of X,ExtREAL; let f be object; assume f in rng g; then consider m be object such that A11: m in dom g and A12: f = g.m by FUNCT_1:def 3; reconsider m as Element of NAT by A10,A11; A13: for n be Nat st IND[n] holds IND[n+1] proof let n be Nat; assume IND[n]; g.(n+1) = h.(n+1) - h.n by A10; hence thesis; end; A14: IND[ 0 ] by A10; for n be Nat holds IND[n] from NAT_1:sch 2(A14,A13); then g.m is PartFunc of X,ExtREAL; hence f in PFuncs(X,ExtREAL) by A12,PARTFUN1:45; end; then rng g c= PFuncs(X,ExtREAL); then reconsider g as Functional_Sequence of X,ExtREAL by A10,FUNCT_2:def 1 ,RELSET_1:4; take g; A15: for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n is_measurable_on E & E c= dom(g.n) proof let n be Nat; per cases; suppose A16: n = 0; hence g.n is_simple_func_in S & g.n is nonnegative by A5,A6,A10; hence g.n is_measurable_on E by MESFUNC2:34; thus thesis by A4,A5,A10,A16; end; suppose n <> 0; then consider m be Nat such that A17: n = m+1 by NAT_1:6; reconsider m as Element of NAT by ORDINAL1:def 12; A18: g.n = h.n - h.m by A10,A17; then A19: g.n = h.n + (-(h.m)) by MESFUNC2:8; A20: h.n is_simple_func_in S by A5; then A21: h.n is without-infty by MESFUNC5:14; A22: dom(h.n) = dom F by A5; (-jj)(#)(h.m) is_simple_func_in S by A5,MESFUNC5:39; then A23: -(h.m) is_simple_func_in S by MESFUNC2:9; hence g.n is_simple_func_in S by A19,A20,MESFUNC5:38; A24: h.m is_simple_func_in S by A5; then h.m is without+infty by MESFUNC5:14; then A25: dom(h.n - h.m) = dom(h.n) /\ dom(h.m) by A21,MESFUNC5:17; A26: dom(h.m) = dom F by A5; then for x being object st x in dom(h.n - h.m) holds(h.m).x <= (h.n).x by A7,A17,A25,A22,NAT_1:11; hence g.n is nonnegative by A18,A20,A24,MESFUNC5:40; thus g.n is_measurable_on E by A19,A20,A23,MESFUNC2:34,MESFUNC5:38; thus thesis by A4,A10,A17,A25,A22,A26; end; end; hence A27: g is additive by Th35; thus for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n is_measurable_on E by A15; A28: now let x be Element of X; assume A29: x in E; then A30: (h#x) is convergent by A4,A8; A31: for m be Nat holds (Partial_Sums(g#x)).m = (h#x).m proof defpred P[Nat] means (Partial_Sums(g#x)).$1 = (h#x).$1; let m be Nat; A32: for k be Nat st P[k] holds P[k+1] proof set Pgx = Partial_Sums(g#x); let k be Nat; assume P[k]; then A33: Pgx.k = (h.k).x by MESFUNC5:def 13; A34: dom(h.(k+1)) = dom F by A5; A35: h.(k+1) is_simple_func_in S by A5; then A36: h.(k+1) is without-infty by MESFUNC5:14; then A37: -infty < (h.(k+1)).x; h.(k+1) is without+infty by A35,MESFUNC5:14; then A38: (h.(k+1)).x < +infty; A39: dom(h.k) = dom F by A5; A40: h.k is_simple_func_in S by A5; then A41: h.k is without+infty by MESFUNC5:14; then A42: (h.k).x < +infty; h.k is without-infty by A40,MESFUNC5:14; then A43: -infty < (h.k).x; reconsider k as Element of NAT by ORDINAL1:def 12; reconsider hk1x=(h.(k+1)).x as Element of REAL by A37,A38,XXREAL_0:14; A44: g.(k+1) = h.(k+1) - h.k by A10; reconsider hkx=(h.k).x as Element of REAL by A43,A42,XXREAL_0:14; (h.(k+1)).x - (h.k).x = hk1x - hkx by SUPINF_2:3; then A45: (h.(k+1)).x - (h.k).x + (h.k).x = hk1x - hkx + hkx by SUPINF_2:1; Pgx.(k+1) = Pgx.k + ((g#x).(k+1)) by Def1; then A46: Pgx.(k+1) = (h.k).x + (g.(k+1)).x by A33,MESFUNC5:def 13; dom(h.(k+1) - h.k) = dom(h.(k+1)) /\ dom(h.k) by A36,A41,MESFUNC5:17; then (g.(k+1)).x = (h.(k+1)).x - (h.k).x by A4,A29,A34,A39,A44, MESFUNC1:def 4; hence thesis by A46,A45,MESFUNC5:def 13; end; (Partial_Sums(g#x)).0 = (g#x).0 by Def1; then (Partial_Sums(g#x)).0 = (g.0).x by MESFUNC5:def 13; then A47: P[ 0 ] by A10,MESFUNC5:def 13; for k being Nat holds P[k] from NAT_1:sch 2(A47,A32); hence thesis; end; A48: lim(h#x) = F.x by A4,A8,A29; per cases by A30; suppose A49: h#x is convergent_to_finite_number; then A50: not h#x is convergent_to_-infty by MESFUNC5:51; not h#x is convergent_to_+infty by A49,MESFUNC5:50; then consider s be Real such that A51: lim(h#x) = s and A52: for p be Real st 0 < p ex N be Nat st for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p and h#x is convergent_to_finite_number by A30,A50,MESFUNC5:def 12; for p be Real st 0 < p ex N be Nat st for m be Nat st N <= m holds |. (Partial_Sums(g#x)).m - s .| < p proof let p be Real; assume 0 < p; then consider N be Nat such that A53: for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by A52; take N; let m be Nat; assume N <= m; then |. (h#x).m - lim(h#x) .| < p by A53; hence thesis by A31,A51; end; then A54: Partial_Sums(g#x) is convergent_to_finite_number; then A55: Partial_Sums(g#x) is convergent; hence g#x is summable; for p be Real st 0 < p ex N be Nat st for m be Nat st N <= m holds |. (Partial_Sums(g#x)).m - lim(h#x) .| < p proof let p be Real; assume 0 < p; then consider N be Nat such that A56: for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by A52; take N; let m be Nat; assume N <= m; then |. (h#x).m - lim(h#x) .| < p by A56; hence thesis by A31; end; then lim Partial_Sums(g#x) = lim(h#x) by A51,A54,A55,MESFUNC5:def 12; hence Sum(g#x) = f.x by A29,A48,FUNCT_1:49; end; suppose A57: (h#x) is convergent_to_+infty; for p be Real st 0 < p ex N be Nat st for m be Nat st N<=m holds p <= (Partial_Sums(g#x)).m proof let p be Real; assume 0 < p; then consider N be Nat such that A58: for m be Nat st N<=m holds p <= (h#x).m by A57; take N; let m be Nat; assume N <= m; then p <= (h#x).m by A58; hence thesis by A31; end; then A59: Partial_Sums(g#x) is convergent_to_+infty; then A60: Partial_Sums(g#x) is convergent; then A61: lim Partial_Sums(g#x) = +infty by A59,MESFUNC5:def 12; thus g#x is summable by A60; lim(h#x) = +infty by A30,A57,MESFUNC5:def 12; hence Sum(g#x) = f.x by A29,A48,A61,FUNCT_1:49; end; suppose A62: (h#x) is convergent_to_-infty; for p be Real st p < 0 ex N be Nat st for m be Nat st N<=m holds (Partial_Sums(g#x)).m <= p proof let p be Real; assume p < 0; then consider N be Nat such that A63: for m be Nat st N<=m holds (h#x).m <= p by A62; take N; let m be Nat; assume N <= m; then (h#x).m <= p by A63; hence thesis by A31; end; then A64: Partial_Sums(g#x) is convergent_to_-infty; then A65: Partial_Sums(g#x) is convergent; then A66: lim Partial_Sums(g#x) = -infty by A64,MESFUNC5:def 12; thus g#x is summable by A65; lim(h#x) = -infty by A30,A62,MESFUNC5:def 12; hence Sum(g#x) = f.x by A29,A48,A66,FUNCT_1:49; end; end; hence for x be Element of X st x in E holds g#x is summable & f.x = Sum(g#x); per cases; suppose E = {}; hence thesis by A1,A3,A15,Lm2; end; suppose A67: E <> {}; for m be Nat holds g.m is_simple_func_in S & g.m is nonnegative & g.m is_measurable_on E & E c= dom(g.m) by A15; then E common_on_dom g by A67,SEQFUNC:def 9; hence thesis by A1,A2,A3,A15,A27,A28,Lm3; end; end; registration let X be non empty set; cluster additive with_the_same_dom for Functional_Sequence of X,ExtREAL; existence proof deffunc f(Nat) = <:{},X,ExtREAL:>; consider F be Functional_Sequence of X,ExtREAL such that A1: for n be Nat holds F.n = f(n) from SEQFUNC:sch 1; now let n,m be Nat; F.n = <:{},X,ExtREAL:> by A1; hence dom(F.n) = dom(F.m) by A1; end; then reconsider F as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2; take F; now let n,m be Nat; assume n <> m; let x be set; assume A2: x in dom(F.n) /\ dom(F.m); F.n = <:{},X,ExtREAL:> by A1; then x in dom {} /\ dom(F.m) by A2,PARTFUN1:34; hence (F.n).x <> +infty or (F.m).x <> -infty; end; hence thesis; end; end; definition let C,D,X be non empty set, F be Function of [:C,D:],PFuncs(X,ExtREAL); let c be Element of C, d be Element of D; redefine func F.(c,d) -> PartFunc of X,ExtREAL; correctness proof thus F.(c,d) is PartFunc of X,ExtREAL by PARTFUN1:47; end; end; definition let C,D,X be non empty set; let F be Function of [:C,D:],X; let c be Element of C; func ProjMap1(F,c) -> Function of D,X means for d be Element of D holds it.d = F.(c,d); existence proof deffunc F(Element of D) = F.(c,$1); consider IT be Function such that A1: dom IT = D & for d be Element of D holds IT.d = F(d) from FUNCT_1: sch 4; now let d be object; assume A2: d in D; then A3: [c,d] in [:C,D:] by ZFMISC_1:87; IT.d = F.(c,d) by A1,A2; hence IT.d in X by A3,FUNCT_2:5; end; then reconsider IT as Function of D,X by A1,FUNCT_2:3; take IT; let d be Element of D; thus thesis by A1; end; uniqueness proof let P1,P2 be Function of D,X; assume that A4: for d be Element of D holds P1.d = F.(c,d) and A5: for d be Element of D holds P2.d = F.(c,d); now let d be object; assume d in D; then reconsider d1 = d as Element of D; P1.d1 = F.(c,d1) by A4; hence P1.d = P2.d by A5; end; hence thesis; end; end; definition let C,D,X be non empty set; let F be Function of [:C,D:],X; let d be Element of D; func ProjMap2(F,d) -> Function of C,X means for c be Element of C holds it.c = F.(c,d); existence proof deffunc F(Element of C) = F.($1,d); consider IT be Function such that A1: dom IT = C & for c be Element of C holds IT.c = F(c) from FUNCT_1: sch 4; now let c be object; assume A2: c in C; then A3: [c,d] in [:C,D:] by ZFMISC_1:87; IT.c = F.(c,d) by A1,A2 .= F.[c,d]; hence IT.c in X by A3,FUNCT_2:5; end; then reconsider IT as Function of C,X by A1,FUNCT_2:3; take IT; let c be Element of C; thus thesis by A1; end; uniqueness proof let P1,P2 be Function of C,X; assume that A4: for c be Element of C holds P1.c = F.(c,d) and A5: for c be Element of C holds P2.c = F.(c,d); now let c be object; assume c in C; then reconsider c1 = c as Element of C; P1.c1 = F.(c1,d) by A4; hence P1.c = P2.c by A5; end; hence thesis; end; end; definition let X,Y be set, F be Function of [:NAT,NAT:],PFuncs(X,Y), n be Nat; func ProjMap1(F,n) -> Functional_Sequence of X,Y means :Def8: for m be Nat holds it.m = F.(n,m); existence proof deffunc P1(Element of NAT) = F.(n,$1); consider IT be Function such that A1: dom IT = NAT & for m be Element of NAT holds IT.m = P1(m) from FUNCT_1:sch 4; now reconsider n1=n as Element of NAT by ORDINAL1:def 12; let y be object; assume y in rng IT; then consider k be object such that A2: k in dom IT and A3: y = IT.k by FUNCT_1:def 3; reconsider k as Element of NAT by A1,A2; y = F.(n1,k) by A1,A3; hence y in PFuncs(X,Y); end; then rng IT c= PFuncs(X,Y); then reconsider IT as Functional_Sequence of X,Y by A1,FUNCT_2:def 1 ,RELSET_1:4; take IT; thus for m be Nat holds IT.m = F.(n,m) proof let m be Nat; reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12; IT.m = F.(n1,m1) by A1; hence thesis; end; end; uniqueness proof let G1,G2 be Functional_Sequence of X,Y; assume that A4: for m be Nat holds G1.m = F.(n,m) and A5: for m be Nat holds G2.m = F.(n,m); for m be Element of NAT holds G1.m = G2.m proof let m be Element of NAT; reconsider m1=m as Nat; G1.m = F.(n,m1) by A4; hence thesis by A5; end; hence thesis; end; func ProjMap2(F,n) -> Functional_Sequence of X,Y means :Def9: for m be Nat holds it.m = F.(m,n); existence proof deffunc P2(Element of NAT) = F.($1,n); consider IT be Function such that A6: dom IT = NAT & for m be Element of NAT holds IT.m = P2(m) from FUNCT_1:sch 4; now reconsider n1=n as Element of NAT by ORDINAL1:def 12; let y be object; assume y in rng IT; then consider k be object such that A7: k in dom IT and A8: y = IT.k by FUNCT_1:def 3; reconsider k as Element of NAT by A6,A7; y = F.(k,n1) by A6,A8; hence y in PFuncs(X,Y); end; then rng IT c= PFuncs(X,Y); then reconsider IT as Functional_Sequence of X,Y by A6,FUNCT_2:def 1 ,RELSET_1:4; take IT; thus for m be Nat holds IT.m = F.(m,n) proof let m be Nat; reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12; IT.m = F.(m1,n1) by A6; hence thesis; end; end; uniqueness proof let G1,G2 be Functional_Sequence of X,Y; assume that A9: for m be Nat holds G1.m = F.(m,n) and A10: for m be Nat holds G2.m = F.(m,n); for m be Element of NAT holds G1.m = G2.m proof let m be Element of NAT; reconsider m1=m as Nat; G1.m = F.(m1,n) by A9; hence thesis by A10; end; hence thesis; end; end; definition let X be non empty set, F be sequence of Funcs(NAT,PFuncs(X,ExtREAL)), n be Nat; redefine func F.n -> Functional_Sequence of X,ExtREAL; correctness proof ex f be Function st F.n = f & dom f = NAT & rng f c= PFuncs(X,ExtREAL) by FUNCT_2:def 2; hence thesis by FUNCT_2:def 1,RELSET_1:4; end; end; theorem Th49: E = dom(F.0) & F is with_the_same_dom & (for n be Nat holds F.n is nonnegative & F.n is_measurable_on E ) implies ex FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) st for n be Nat holds (for m be Nat holds (FF.n).m is_simple_func_in S & dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds ((FF.n).j).x <= ((FF.n).k).x) & for x be Element of X st x in dom(F.n) holds (FF.n)#x is convergent & lim((FF.n)#x) = (F.n).x proof assume that A1: E = dom(F.0) and A2: F is with_the_same_dom and A3: for n be Nat holds F.n is nonnegative & F.n is_measurable_on E; defpred Q[Element of NAT,set] means for G be Functional_Sequence of X, ExtREAL st $2 = G holds (for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.$1)) & (for m be Nat holds G.m is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.$1) holds (G.j).x <= (G.k).x) & (for x be Element of X st x in dom(F.$1) holds G#x is convergent & lim(G#x) = ( F.$1).x); A4: for n be Element of NAT holds ex G be Functional_Sequence of X,ExtREAL st (for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n)) & (for m be Nat holds G.m is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds (G.j).x <= (G.k).x ) & for x be Element of X st x in dom(F.n) holds (G#x) is convergent & lim(G#x) = (F.n).x proof let n be Element of NAT; A5: F.n is_measurable_on E by A3; A6: F.n is nonnegative by A3; E = dom(F.n) by A1,A2; hence thesis by A5,A6,MESFUNC5:64; end; A7: for n be Element of NAT ex G be Element of Funcs(NAT,PFuncs(X,ExtREAL)) st Q[n,G] proof let n be Element of NAT; consider G be Functional_Sequence of X,ExtREAL such that A8: for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n) and A9: for m be Nat holds G.m is nonnegative and A10: for j,k be Nat st j <= k holds for x be Element of X st x in dom( F. n) holds (G.j).x <= (G.k).x and A11: for x be Element of X st x in dom(F.n) holds (G#x) is convergent & lim(G#x) = (F.n).x by A4; reconsider G as Element of Funcs(NAT,PFuncs(X,ExtREAL)) by FUNCT_2:8; take G; thus thesis by A8,A9,A10,A11; end; consider FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) such that A12: for n be Element of NAT holds Q[n,FF.n] from FUNCT_2:sch 3(A7); take FF; thus for n be Nat holds (for m be Nat holds (FF.n).m is_simple_func_in S & dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds ((FF.n) .j).x <= ((FF.n).k).x) & for x be Element of X st x in dom(F.n) holds (FF.n)#x is convergent & lim((FF.n)#x) = (F.n).x proof let n be Nat; reconsider n1 = n as Element of NAT by ORDINAL1:def 12; for G be Functional_Sequence of X,ExtREAL st FF.n1 = G holds (for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n1)) & (for m be Nat holds G.m is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n1) holds (G.j).x <= (G.k).x) & for x be Element of X st x in dom(F.n1) holds G#x is convergent & lim(G#x) = (F.n1).x by A12; hence thesis; end; end; theorem Th50: E = dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat holds F.n is_measurable_on E & F.n is nonnegative) implies ex I be ExtREAL_sequence st for n be Nat holds I.n = Integral(M,F.n) & Integral(M,( Partial_Sums F).n) = (Partial_Sums I).n proof assume that A1: E = dom(F.0) and A2: F is additive and A3: F is with_the_same_dom and A4: for n be Nat holds F.n is_measurable_on E & F.n is nonnegative; set PF = Partial_Sums F; deffunc I(Element of NAT) = Integral(M,F.$1); consider I be sequence of ExtREAL such that A5: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4; reconsider I as ExtREAL_sequence; take I; A6: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12; thus for n be Nat holds I.n = Integral(M,F.n) & Integral(M,(Partial_Sums F). n) = (Partial_Sums I).n proof set PI = Partial_Sums I; defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1; let n be Nat; reconsider n9=n as Element of NAT by ORDINAL1:def 12; I.n = Integral(M,F.n9) by A5; hence I.n = Integral(M,F.n); A7: for k be Nat st P2[k] holds P2[k+1] proof let k be Nat; assume A8: P2[k]; A9: F.(k+1) is_measurable_on E by A4; A10: dom(F.(k+1)) = E by A1,A3; A11: PF.(k+1) is_measurable_on E by A4,A6,Th41; A12: F.(k+1) is nonnegative by A4; A13: PF.k is nonnegative by A4,Th36; A14: dom(PF.k) = E by A1,A2,A3,Th29; A15: PF.k is_measurable_on E by A4,A6,Th41; then consider D be Element of S such that A16: D = dom(PF.k + F.(k+1)) and A17: integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+ (M,( F.(k+1))|D) by A14,A10,A9,A13,A12,MESFUNC5:78; A18: D = dom(PF.k) /\ dom(F.(k+1)) by A13,A12,A16,MESFUNC5:22 .= E by A14,A10; then A19: (PF.k)|D = PF.k by A14; A20: (F.(k+1))|D = F.(k+1) by A10,A18; dom(PF.(k+1)) = E by A1,A2,A3,Th29; then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by A4,A11,Th36, MESFUNC5:88 .= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A17,Def4 .= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A14,A15,A13,A19, MESFUNC5:88 .= Integral(M,PF.k) + Integral(M,F.(k+1)) by A10,A9,A12,A20,MESFUNC5:88 .= PI.k + I.(k+1) by A5,A8; hence thesis by Def1; end; Integral(M,PF.0) = Integral(M,F.0) by Def4; then Integral(M,PF.0) = I.0 by A5; then A21: P2[ 0 ] by Def1; for k be Nat holds P2[k] from NAT_1:sch 2(A21,A7); hence thesis; end; end; Lm4: E = dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat holds F.n is nonnegative & F.n is_measurable_on E ) & (for x be Element of X st x in E holds F#x is summable) implies ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,(lim(Partial_Sums F))|E) = Sum I proof assume that A1: E = dom(F.0) and A2: F is additive and A3: F is with_the_same_dom and A4: for n be Nat holds F.n is nonnegative & F.n is_measurable_on E and A5: for x be Element of X st x in E holds F#x is summable; consider FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) such that A6: for n be Nat holds (for m be Nat holds (FF.n).m is_simple_func_in S & dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m is nonnegative) & ( for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds (( FF.n).j).x <= ((FF.n).k).x) & for x be Element of X st x in dom(F.n) holds (FF. n)#x is convergent & lim((FF.n)#x) = (F.n).x by A1,A3,A4,Th49; defpred PP[Element of NAT,Element of NAT,set] means for n,m be Nat st n = $1 & m = $2 holds $3 = (FF.n).m; A7: for i1 be Element of NAT for j1 be Element of NAT ex F1 be Element of PFuncs(X,ExtREAL) st PP[i1,j1,F1] proof let i1 be Element of NAT; let j1 be Element of NAT; reconsider i = i1, j = j1 as Nat; reconsider F1 = (FF.i).j as Element of PFuncs(X,ExtREAL) by PARTFUN1:45; take F1; thus thesis; end; consider FF2 be Function of [:NAT,NAT:],PFuncs(X,ExtREAL) such that A8: for i be Element of NAT for j be Element of NAT holds PP[i,j,FF2.(i ,j)] from BINOP_1:sch 3(A7); deffunc Phi(Nat) = (Partial_Sums ProjMap2(FF2,$1)).$1; consider P be Functional_Sequence of X,ExtREAL such that A9: for k be Nat holds P.k = Phi(k) from SEQFUNC:sch 1; A10: for n be Nat holds (for m be Nat holds dom(ProjMap1(FF2,n).m) = E & dom( ProjMap2(FF2,n).m) = E & ProjMap1(FF2,n).m is_simple_func_in S & ProjMap2(FF2,n ).m is_simple_func_in S) & ProjMap1(FF2,n) is additive & ProjMap2(FF2,n) is additive & ProjMap1(FF2,n) is with_the_same_dom & ProjMap2(FF2,n) is with_the_same_dom proof let n be Nat; A11: now let m be Nat; reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12; A12: ProjMap1(FF2,n).m = FF2.(n,m) by Def8; A13: FF2.(n1,m1) = (FF.n1).m by A8; A14: dom(F.m1) = dom(F.0) by A3; A15: ProjMap2(FF2,n).m = FF2.(m,n) by Def9; A16: FF2.(m1,n1) = (FF.m1).n by A8; dom(F.n1) = dom(F.m1) by A3; hence dom(ProjMap1(FF2,n).m) = E & dom(ProjMap2(FF2,n).m) = E by A1,A6 ,A12,A15,A13,A16,A14; thus ProjMap1(FF2,n).m is_simple_func_in S & ProjMap2(FF2,n).m is_simple_func_in S by A6,A12,A15,A13,A16; end; for i1,j1 be Nat holds dom(ProjMap1(FF2,n).i1) = dom(ProjMap1(FF2,n). j1) & dom(ProjMap2(FF2,n).i1) = dom(ProjMap2(FF2,n).j1) proof let i1,j1 be Nat; A17: dom(ProjMap2(FF2,n).i1) = E by A11; dom(ProjMap1(FF2,n).i1) = E by A11; hence thesis by A11,A17; end; hence thesis by A11,Th35; end; for n,m be Nat holds dom(P.n) = dom(P.m) proof let n,m be Nat; A18: ProjMap2(FF2,n) is with_the_same_dom by A10; A19: dom(P.n) = dom((Partial_Sums ProjMap2(FF2,n)).n) by A9; ProjMap2(FF2,n) is additive by A10; then dom(P.n) = dom((ProjMap2(FF2,n)).0) by A18,A19,Th29; then dom(P.n) = E by A10; then A20: dom(P.n) = dom((ProjMap2(FF2,m)).0) by A10; A21: ProjMap2(FF2,m) is with_the_same_dom by A10; ProjMap2(FF2,m) is additive by A10; then dom(P.n) = dom((Partial_Sums ProjMap2(FF2,m)).m) by A21,A20,Th29; hence thesis by A9; end; then reconsider P as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2; dom(lim P) = dom(P.0) by MESFUNC8:def 9; then dom(lim P) = dom((Partial_Sums ProjMap2(FF2,0)).0) by A9; then dom(lim P) = dom((ProjMap2(FF2,0)).0) by Def4; then dom(lim P) = dom( FF2.(0,0) ) by Def9; then A22: dom(lim P) = dom( (FF.0).0 ) by A8; then A23: dom (lim P) = dom(F.0) by A6; A24: for k be Nat holds for m be Nat, x be Element of X st x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0) holds ((ProjMap2(FF2,k)).m).x <= (F.m).x proof let k be Nat; let m be Nat, x be Element of X; reconsider m1 = m, k1 = k as Element of NAT by ORDINAL1:def 12; assume x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0); then x in dom(F.0) by XBOOLE_0:def 4; then A25: x in dom(F.m) by A3; (FF.m1)#x is non-decreasing proof let j,k be ExtReal; assume that A26: j in dom((FF.m1)#x) and A27: k in dom((FF.m1)#x) and A28: j <= k; reconsider j,k as Element of NAT by A26,A27; A29: ((FF.m1)#x).k = ((FF.m1).k).x by MESFUNC5:def 13; ((FF.m1)#x).j = ((FF.m1).j).x by MESFUNC5:def 13; hence thesis by A6,A25,A28,A29; end; then lim((FF.m1)#x) = sup ((FF.m1)#x) by RINFSUP2:37; then ((FF.m1)#x).k1 <= lim((FF.m1)#x) by RINFSUP2:23; then A30: ((FF.m1)#x).k <= (F.m1).x by A6,A25; (ProjMap2(FF2,k)).m = FF2.(m1,k1) by Def9; then (ProjMap2(FF2,k)).m = (FF.m).k by A8; hence thesis by A30,MESFUNC5:def 13; end; A31: for x be Element of X, k be Element of NAT st x in dom(lim P) holds (P# x).k <= ((Partial_Sums F)#x).k proof let x be Element of X; let k be Element of NAT; assume A32: x in dom(lim P); dom((ProjMap2(FF2,k)).0) = E by A10; then A33: x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0) by A1,A6,A22,A32; A34: ProjMap2(FF2,k) is with_the_same_dom by A10; (P#x).k = (P.k).x by MESFUNC5:def 13; then A35: (P#x).k = ((Partial_Sums ProjMap2(FF2,k)).k).x by A9; A36: for m be Nat, x be Element of X st x in dom(F.0) /\ dom((ProjMap2( FF2, k)).0) holds ((ProjMap2(FF2,k)).m).x <= (F.m).x by A24; ProjMap2(FF2,k) is additive by A10; then ((Partial_Sums ProjMap2(FF2,k)).k).x <= ((Partial_Sums F).k).x by A2 ,A3,A33,A34,A36,Th42; hence thesis by A35,MESFUNC5:def 13; end; dom(lim(Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 9; then A37: dom(lim(Partial_Sums F)) = E by A1,Def4; A38: for n,m be Nat holds (ProjMap1(FF2,n)).m is nonnegative & (ProjMap2(FF2, n)).m is nonnegative proof let n,m be Nat; reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12; (ProjMap1(FF2,n)).m = FF2.(n1,m1) by Def8; then (ProjMap1(FF2,n)).m = (FF.n).m by A8; hence (ProjMap1(FF2,n)).m is nonnegative by A6; (ProjMap2(FF2,n)).m = FF2.(m1,n1) by Def9; then (ProjMap2(FF2,n)).m = (FF.m).n by A8; hence thesis by A6; end; A39: for n be Element of NAT holds for x be Element of X st x in E holds ( ProjMap1(FF2,n))#x is convergent & (F.n).x = lim( (ProjMap1(FF2,n))#x ) proof let n be Element of NAT; reconsider n1 = n as Nat; let x be Element of X; assume A40: x in E; for k be Nat holds ex m be Nat st k <= m & ((ProjMap1(FF2,n))#x).m > -1 proof let k be Nat; take m = k; A41: ((ProjMap1(FF2,n))#x).m = ((ProjMap1(FF2,n)).m).x by MESFUNC5:def 13; (ProjMap1(FF2,n)).m is nonnegative by A38; hence thesis by A41,SUPINF_2:39; end; then A42: not (ProjMap1(FF2,n))#x is convergent_to_-infty; A43: E = dom(F.n1) by A1,A3; (ProjMap1(FF2,n))#x is non-decreasing proof let i,j be ExtReal; assume that A44: i in dom((ProjMap1(FF2,n))#x) and A45: j in dom((ProjMap1(FF2,n))#x) and A46: i <= j; reconsider i1=i, j1=j as Element of NAT by A44,A45; A47: ((ProjMap1(FF2,n))#x).i1 = ((ProjMap1(FF2,n)).i1).x by MESFUNC5:def 13; (ProjMap1(FF2,n)).i1 = FF2.(n,i1) by Def8; then A48: (ProjMap1(FF2,n)).i1 = (FF.n1).i1 by A8; A49: ((ProjMap1(FF2,n))#x).j1 = ((ProjMap1(FF2,n)).j1).x by MESFUNC5:def 13; A50: (ProjMap1(FF2,n)).j1 = FF2.(n,j1) by Def8; ((FF.n1).i1).x <= ((FF.n1).j1).x by A6,A43,A40,A46; hence thesis by A8,A47,A49,A48,A50; end; hence A51: (ProjMap1(FF2,n))#x is convergent by RINFSUP2:37; per cases by A51,A42; suppose A52: (ProjMap1(FF2,n))#x is convergent_to_finite_number; then A53: not (ProjMap1(FF2,n))#x is convergent_to_-infty by MESFUNC5:51; not (ProjMap1(FF2,n))#x is convergent_to_+infty by A52,MESFUNC5:50; then consider lP be Real such that A54: lim( (ProjMap1(FF2,n))#x ) = lP and A55: for p be Real st 0

= 0 proof let x be object; assume A147: x in dom(lim(Partial_Sums F)); then reconsider x1=x as Element of X; A148: for n be Nat holds ((Partial_Sums F)#x1).n >= 0 proof let n be Nat; (Partial_Sums F).n is nonnegative by A4,Th36; then ((Partial_Sums F).n).x1 >= 0 by SUPINF_2:51; hence thesis by MESFUNC5:def 13; end; x in dom(F.0) by A67,A147,Def4; then (Partial_Sums F)#x1 is convergent by A3,A4,Th38; then lim((Partial_Sums F)#x1) >= 0 by A148,Th10; hence thesis by A147,MESFUNC8:def 9; end; then A149: lim(Partial_Sums F) is nonnegative by SUPINF_2:52; consider I be ExtREAL_sequence such that A150: for n be Nat holds I.n = Integral(M,F.n) & Integral(M,( Partial_Sums F).n) = (Partial_Sums I).n by A1,A2,A3,A4,Th50; for n be object st n in dom I holds 0 <= I.n proof let n be object; assume n in dom I; then reconsider n1 = n as Nat; A151: F.n1 is nonnegative by A4; A152: F.n1 is_measurable_on E by A4; E = dom(F.n1) by A1,A3; then 0 <= Integral(M,F.n1) by A151,A152,MESFUNC5:90; hence thesis by A150; end; then I is nonnegative by SUPINF_2:52; then A153: Partial_Sums I is non-decreasing by Th16; then A154: Partial_Sums I is convergent by RINFSUP2:37; deffunc J(Element of NAT) = integral'(M,P.$1); consider J be sequence of ExtREAL such that A155: for n be Element of NAT holds J.n = J(n) from FUNCT_2:sch 4; reconsider J as ExtREAL_sequence; A156: for n be Nat holds P.n is_simple_func_in S proof let n be Nat; for m be Nat holds ProjMap2(FF2,n).m is_simple_func_in S by A10; then (Partial_Sums ProjMap2(FF2,n)).n is_simple_func_in S by Th35; hence thesis by A9; end; A157: for n be Nat holds J.n = integral'(M,P.n) proof let n be Nat; reconsider n9=n as Element of NAT by ORDINAL1:def 12; J.n = integral'(M,P.n9) by A155; hence thesis; end; for n,m be Nat st m<=n holds J.m <= J.n proof let n,m be Nat; A158: P.n is nonnegative by A145; A159: P.m is_simple_func_in S by A156; A160: for n,m,l be Nat holds dom(P.n - P.m) = dom(P.l) proof let n,m,l be Nat; P.m is_simple_func_in S by A156; then A161: P.m is without+infty by MESFUNC5:14; P.n is_simple_func_in S by A156; then P.n is without-infty by MESFUNC5:14; then dom(P.n - P.m) = dom(P.n) /\ dom(P.m) by A161,MESFUNC5:17; then dom(P.n - P.m) = dom(lim(Partial_Sums F)) /\ dom(P.m) by A69; then dom(P.n - P.m) = dom(lim(Partial_Sums F)) /\ dom(lim(Partial_Sums F)) by A69; hence thesis by A69; end; then A162: dom(P.n - P.m) = dom(P.n); then A163: (P.n)|dom(P.n - P.m) = P.n; assume A164: m<=n; A165: for x be object st x in dom(P.n - P.m) holds (P.m).x <= (P.n).x proof let x be object; assume x in dom(P.n - P.m); then x in dom(lim(Partial_Sums F)) by A69,A162; hence thesis by A68,A85,A164; end; A166: P.m is nonnegative by A145; dom(P.n - P.m) = dom(P.m) by A160; then A167: (P.m)|dom(P.n - P.m) = P.m; P.n is_simple_func_in S by A156; then integral'(M,(P.m)|dom(P.n - P.m)) <= integral'(M,(P.n)|dom(P.n - P.m )) by A158,A159,A166,A165,MESFUNC5:70; then J.m <= integral'(M,P.n) by A157,A167,A163; hence thesis by A157; end; then J is non-decreasing by RINFSUP2:7; then A168: J is convergent by RINFSUP2:37; A169: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12; then A170: for n be Nat holds (Partial_Sums F).n is_measurable_on E by A4,Th41; then lim(Partial_Sums F) is_measurable_on E by A1,A2,A3,A5,Th44; then integral+(M,(lim(Partial_Sums F))) = lim J by A68,A156,A85,A157,A69,A143 ,A145,A149,A168,MESFUNC5:def 15; then A171: Integral(M,(lim(Partial_Sums F))) = lim J by A1,A2,A3,A5,A170,A37,A149 ,Th44,MESFUNC5:88; A172: for n be Nat, x be Element of X st x in dom(F.n) holds (FF.n)#x is non-decreasing proof let n be Nat, x be Element of X; assume A173: x in dom(F.n); let i,j be ExtReal; assume that A174: i in dom((FF.n)#x) and A175: j in dom((FF.n)#x) and A176: i<=j; reconsider i,j as Element of NAT by A174,A175; ((FF.n).i).x <= ((FF.n).j).x by A6,A173,A176; then ((FF.n)#x).i <= ((FF.n).j).x by MESFUNC5:def 13; hence thesis by MESFUNC5:def 13; end; A177: for n,p be Nat st p >= n holds for x be Element of X st x in E holds (( Partial_Sums ProjMap2(FF2,p)).n).x <= (P.p).x & (P.p).x = ((Partial_Sums ProjMap2(FF2,p)).p).x & ((Partial_Sums ProjMap2(FF2,p)).p).x <= ((Partial_Sums F).p).x & ((Partial_Sums F).p).x <= (lim (Partial_Sums F)).x proof let n,p be Nat; reconsider p1=p, n1=n as Element of NAT by ORDINAL1:def 12; assume A178: p >= n; let x be Element of X; A179: for i be Nat holds ProjMap2(FF2,p).i is nonnegative by A38; assume A180: x in E; then A181: x in dom((ProjMap2(FF2,p)).0) by A10; ProjMap2(FF2,p) is with_the_same_dom by A10; then (Partial_Sums ProjMap2(FF2,p))#x is non-decreasing by A181,A179,Th38; then ((Partial_Sums ProjMap2(FF2,p))#x).n1 <= ((Partial_Sums ProjMap2(FF2 ,p))#x).p1 by A178,RINFSUP2:7; then ((Partial_Sums ProjMap2(FF2,p)).n).x <= ((Partial_Sums ProjMap2(FF2, p))#x).p by MESFUNC5:def 13; then ((Partial_Sums ProjMap2(FF2,p)).n).x <= ((Partial_Sums ProjMap2(FF2, p)).p).x by MESFUNC5:def 13; hence ((Partial_Sums ProjMap2(FF2,p)).n).x <= (P.p).x by A9; thus (P.p).x = ((Partial_Sums ProjMap2(FF2,p)).p).x by A9; A182: ProjMap2(FF2,p) is additive by A10; A183: ProjMap2(FF2,p) is with_the_same_dom by A10; A184: for n be Nat, x be Element of X st x in dom(ProjMap2(FF2,p).0) /\ dom (F.0) holds (ProjMap2(FF2,p).n).x <= (F.n).x proof let n be Nat, x be Element of X; reconsider n1=n as Element of NAT by ORDINAL1:def 12; assume x in dom(ProjMap2(FF2,p).0) /\ dom(F.0); then x in dom(F.0) by XBOOLE_0:def 4; then A185: x in dom(F.n) by A3; then (FF.n)#x is non-decreasing by A172; then lim((FF.n)#x) = sup((FF.n)#x) by RINFSUP2:37; then ((FF.n)#x).p1 <= lim((FF.n)#x) by RINFSUP2:23; then A186: ((FF.n)#x).p <= (F.n).x by A6,A185; ((ProjMap2(FF2,p)).n).x = (FF2.(n1,p1)).x by Def9; then ((ProjMap2(FF2,p)).n).x = ((FF.n).p).x by A8; hence thesis by A186,MESFUNC5:def 13; end; x in dom(ProjMap2(FF2,p).0) /\ dom(F.0) by A1,A180,A181,XBOOLE_0:def 4; hence ((Partial_Sums ProjMap2(FF2,p)).p).x <= ((Partial_Sums F).p).x by A2,A3 ,A182,A183,A184,Th42; (Partial_Sums F)#x is non-decreasing by A1,A3,A4,A180,Th38; then lim((Partial_Sums F)#x) = sup((Partial_Sums F)#x) by RINFSUP2:37; then ((Partial_Sums F)#x).p1 <= lim((Partial_Sums F)#x) by RINFSUP2:23; then ((Partial_Sums F).p).x <= lim((Partial_Sums F)#x) by MESFUNC5:def 13; hence thesis by A68,A180,MESFUNC8:def 9; end; for n be Nat holds (Partial_Sums I).n <= Integral(M,(lim(Partial_Sums F))) proof let n be Nat; A187: (Partial_Sums F).n is nonnegative by A4,Th36; A188: lim(Partial_Sums F) is_measurable_on E by A1,A2,A3,A5,A170,Th44; A189: (Partial_Sums F).n is_measurable_on E by A4,A169,Th41; A190: E = dom((Partial_Sums F).n) by A1,A2,A3,Th29; then for x be Element of X st x in dom((Partial_Sums F).n) holds (( Partial_Sums F).n).x <= (lim(Partial_Sums F)).x by A177; then integral+(M,(Partial_Sums F).n) <= integral+(M,(lim(Partial_Sums F)) ) by A37,A149,A190,A189,A188,A187,MESFUNC5:85; then Integral(M,(Partial_Sums F).n) <= integral+(M,(lim(Partial_Sums F))) by A170,A190,A187,MESFUNC5:88; then Integral(M,(Partial_Sums F).n) <= Integral(M,(lim(Partial_Sums F))) by A37,A146,A188,MESFUNC5:88,SUPINF_2:52; hence thesis by A150; end; then A191: lim(Partial_Sums I) <= Integral(M,(lim(Partial_Sums F))) by A153,Th9, RINFSUP2:37; take I; thus for n be Nat holds I.n = Integral(M,(F.n)|E) proof let n be Nat; dom(F.0) = dom(F.n) by A3; then (F.n)|E = F.n by A1; hence thesis by A150; end; A192: for n be Nat holds J.n = Integral(M,P.n) proof let n be Nat; A193: P.n is nonnegative by A145; A194: J.n = integral'(M,P.n) by A157; P.n is_simple_func_in S by A156; hence thesis by A193,A194,MESFUNC5:89; end; for n be Nat holds J.n <= (Partial_Sums I).n proof let n be Nat; A195: P.n is_measurable_on E by A156,MESFUNC2:34; A196: (Partial_Sums F).n is nonnegative by A4,Th36; A197: n in NAT by ORDINAL1:def 12; A198: for x be Element of X st x in dom(P.n) holds (P.n).x <= (( Partial_Sums F).n).x proof let x be Element of X; assume x in dom(P.n); then x in dom(lim(Partial_Sums F)) by A69; then (P#x).n <= ((Partial_Sums F)#x).n by A1,A23,A37,A31,A197; then (P.n).x <= ((Partial_Sums F)#x).n by MESFUNC5:def 13; hence thesis by MESFUNC5:def 13; end; A199: P.n is nonnegative by A145; A200: dom(P.n) = E by A37,A69; A201: E = dom((Partial_Sums F).n) by A1,A2,A3,Th29; (Partial_Sums F).n is_measurable_on E by A4,A169,Th41; then integral+(M,P.n) <= integral+(M,(Partial_Sums F).n) by A201,A200,A195 ,A199,A196,A198,MESFUNC5:85; then Integral(M,P.n) <= integral+(M,(Partial_Sums F).n) by A145,A200,A195, MESFUNC5:88; then Integral(M,P.n) <= Integral(M,(Partial_Sums F).n) by A170,A201,A196, MESFUNC5:88; then J.n <= Integral(M,(Partial_Sums F).n) by A192; hence thesis by A150; end; then lim J <= lim (Partial_Sums I) by A168,A154,RINFSUP2:38; then Sum I = Integral(M,(lim(Partial_Sums F))) by A171,A191,XXREAL_0:1; hence thesis by A37,A154; end; theorem Th51: E c= dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat holds F.n is nonnegative & F.n is_measurable_on E) & (for x be Element of X st x in E holds F#x is summable) implies ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,(lim( Partial_Sums F))|E) = Sum I proof assume that A1: E c= dom(F.0) and A2: F is additive and A3: F is with_the_same_dom and A4: for n be Nat holds F.n is nonnegative & F.n is_measurable_on E and A5: for x be Element of X st x in E holds F#x is summable; deffunc F(Nat) = (F.$1)|E; consider G be Functional_Sequence of X,ExtREAL such that A6: for n be Nat holds G.n = F(n) from SEQFUNC:sch 1; reconsider G as additive with_the_same_dom Functional_Sequence of X,ExtREAL by A2,A3,A6,Th18,Th31; A7: for n be Nat holds G.n is nonnegative & G.n is_measurable_on E proof let n be Nat; (F.n)|E is nonnegative by A4,MESFUNC5:15; hence G.n is nonnegative by A6; thus thesis by A1,A3,A4,A6,Th20; end; dom((F.0)|E) = E by A1,RELAT_1:62; then A8: E = dom(G.0) by A6; A9: for x be Element of X st x in E holds F#x = G#x proof let x be Element of X; assume A10: x in E; for n9 be object st n9 in NAT holds (F#x).n9 = (G#x).n9 proof let n9 be object; assume n9 in NAT; then reconsider n = n9 as Nat; dom(G.n) = E by A8,MESFUNC8:def 2; then x in dom((F.n)|E) by A6,A10; then ((F.n)|E).x = (F.n).x by FUNCT_1:47; then A11: (G.n).x = (F.n).x by A6; (F#x).n = (F.n).x by MESFUNC5:def 13; hence thesis by A11,MESFUNC5:def 13; end; hence thesis; end; A12: (lim(Partial_Sums G))|E = (lim(Partial_Sums F))|E proof set E1 = dom(F.0); set PF = Partial_Sums F; set PG = Partial_Sums G; A13: dom(lim PG) = dom(PG.0) by MESFUNC8:def 9; dom(PF.0) = E1 by A2,A3,Th29; then A14: E c= dom(lim(PF)) by A1,MESFUNC8:def 9; A15: for x being Element of X st x in dom(lim PG) holds (lim PG).x = (lim PF).x proof let x being Element of X; set PFx = Partial_Sums(F#x); set PGx = Partial_Sums(G#x); assume A16: x in dom(lim PG); then A17: x in E by A8,A13,Th29; for n be Element of NAT holds (PG#x).n = (PF#x).n proof let n be Element of NAT; A18: PGx.n = (PG#x).n by A8,A17,Th32; PFx.n = (PF#x).n by A1,A2,A3,A17,Th32; hence thesis by A9,A17,A18; end; then A19: lim(PG#x) = lim(PF#x) by FUNCT_2:63; (lim PG).x = lim(PG#x) by A16,MESFUNC8:def 9; hence thesis by A14,A17,A19,MESFUNC8:def 9; end; A20: dom(PG.0) = dom(G.0) by Th29; then A21: dom((lim PG)|E) = dom(lim PG) by A8,A13; A22: dom((lim PF)|E) = E by A14,RELAT_1:62; then A23: dom((lim PG)|E) = dom((lim PF)|E) by A8,A20,A13; for x be Element of X st x in dom((lim PG)|E) holds ((lim PG)|E).x = ((lim PF)|E).x proof let x be Element of X; assume A24: x in dom((lim PG)|E); then A25: ((lim PF)|E).x = (lim PF).x by A23,FUNCT_1:47; (lim PG).x = (lim PF).x by A21,A15,A24; hence thesis by A24,A25,FUNCT_1:47; end; hence thesis by A8,A20,A13,A22,PARTFUN1:5; end; for x be Element of X st x in E holds G#x is summable by A1,A5,A6,Th21; then consider I be ExtREAL_sequence such that A26: for n be Nat holds I.n = Integral(M,(G.n)|E) and A27: I is summable and A28: Integral(M,(lim(Partial_Sums G))|E) = Sum I by A8,A7,Lm4; take I; now let n be Nat; ((F.n)|E)|E = (F.n)|E; then (G.n)|E = (F.n)|E by A6; hence I.n = Integral(M,(F.n)|E) by A26; end; hence thesis by A27,A28,A12; end; :: Lebesgue Monotone Convergence Theorem ::$N Lebesgue's Monotone Convergence Theorem theorem E = dom(F.0) & F.0 is nonnegative & F is with_the_same_dom & (for n be Nat holds F.n is_measurable_on E) & (for n,m be Nat st n <=m holds for x be Element of X st x in E holds (F.n).x <= (F.m).x ) & (for x be Element of X st x in E holds F#x is convergent) implies ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n)) & I is convergent & Integral(M,lim F) = lim I proof assume that A1: E = dom(F.0) and A2: F.0 is nonnegative and A3: F is with_the_same_dom and A4: for n be Nat holds F.n is_measurable_on E and A5: for n,m be Nat st n <= m holds for x be Element of X st x in E holds (F.n).x <= (F.m).x and A6: for x be Element of X st x in E holds F#x is convergent; A7: lim F is_measurable_on E by A1,A3,A4,A6,MESFUNC8:25; A8: for n be Nat holds F.n is nonnegative proof let n be Nat; for x be object st x in dom(F.n) holds 0 <= (F.n).x proof let x be object; assume x in dom(F.n); then x in E by A1,A3; then (F.0).x <= (F.n).x by A5; hence thesis by A2,SUPINF_2:51; end; hence thesis by SUPINF_2:52; end; per cases; suppose ex n be Nat st M.(E /\ eq_dom(F.n,+infty)) <> 0; then consider N be Nat such that A9: M.(E /\ eq_dom(F.N,+infty)) <> 0; A10: E = dom(F.N) by A1,A3; then reconsider EE = E /\ eq_dom(F.N,+infty) as Element of S by A4, MESFUNC1:33; A11: EE c= E by XBOOLE_1:17; then A12: F.N is_measurable_on EE by A4,MESFUNC1:30; EE c= dom(F.N) by A1,A3,A11; then A13: EE = dom((F.N)|EE) by RELAT_1:62; then EE = dom(F.N) /\ EE by RELAT_1:61; then A14: (F.N)|EE is_measurable_on EE by A12,MESFUNC5:42; now let x be object; assume A15: x in EE; then x in eq_dom(F.N,+infty) by XBOOLE_0:def 4; then (F.N).x = +infty by MESFUNC1:def 15; then ((F.N)|EE).x = +infty by A13,A15,FUNCT_1:47; hence x in eq_dom((F.N)|EE,+infty) by A13,A15,MESFUNC1:def 15; end; then A16: EE c= eq_dom((F.N)|EE,+infty); for x be object st x in eq_dom((F.N)|EE,+infty) holds x in EE by A13, MESFUNC1:def 15; then eq_dom((F.N)|EE,+infty) c= EE; then EE = eq_dom((F.N)|EE,+infty) by A16,XBOOLE_0:def 10; then A17: M.(EE /\ eq_dom((F.N)|EE,+infty)) <> 0 by A9; F.N is_measurable_on E by A4; then A18: Integral(M,(F.N)|EE) <= Integral(M,(F.N)|E) by A8,A10,A11,MESFUNC5:93; reconsider N1 = N as Element of NAT by ORDINAL1:def 12; deffunc I1(Element of NAT) = Integral(M,F.$1); consider I be sequence of ExtREAL such that A19: for n be Element of NAT holds I.n = I1(n) from FUNCT_2:sch 4; reconsider I as ExtREAL_sequence; A20: 0 < M.(E /\ eq_dom(F.N,+infty)) by A9,SUPINF_2:51; A21: for n be Nat holds I.n = Integral(M,F.n) proof let n be Nat; reconsider n1=n as Element of NAT by ORDINAL1:def 12; I.n = Integral(M,F.n1) by A19; hence thesis; end; take I; A22: dom(lim F) = dom(F.0) by MESFUNC8:def 9; for x be object st x in dom(lim F) holds (lim F).x >= 0 proof let x be object; assume A23: x in dom(lim F); then reconsider x1=x as Element of X; for n be Nat holds (F#x1).n >= 0 proof let n be Nat; A24: (F.0).x1 >= 0 by A2,SUPINF_2:51; (F.n).x1 >= (F.0).x1 by A1,A5,A22,A23; hence thesis by A24,MESFUNC5:def 13; end; then lim(F#x1) >= 0 by A1,A6,A22,A23,Th10; hence thesis by A23,MESFUNC8:def 9; end; then A25: lim F is nonnegative by SUPINF_2:52; A26: E = dom(lim F) by A1,MESFUNC8:def 9; A27: EE c= E /\ eq_dom(lim F,+infty) proof let x be object; assume A28: x in EE; then reconsider x1=x as Element of X; x in eq_dom(F.N,+infty) by A28,XBOOLE_0:def 4; then (F.N).x1 = +infty by MESFUNC1:def 15; then A29: (F#x1).N = +infty by MESFUNC5:def 13; A30: x in E by A28,XBOOLE_0:def 4; for n,m be Nat st m <= n holds (F#x1).m <= (F#x1).n proof let n,m be Nat; assume m <= n; then (F.m).x1 <= (F.n).x1 by A5,A30; then (F#x1).m <= (F.n).x1 by MESFUNC5:def 13; hence thesis by MESFUNC5:def 13; end; then A31: (F#x1) is non-decreasing by RINFSUP2:7; then A32: (F#x1)^\N1 is non-decreasing by RINFSUP2:26; ((F#x1)^\N1).0 = (F#x1).(0+N) by NAT_1:def 3; then for n be Element of NAT holds +infty <= ((F#x1)^\N1).n by A29,A32, RINFSUP2:7; then (F#x1)^\N1 is convergent_to_+infty by RINFSUP2:32; then A33: lim((F#x1)^\N1) = +infty by Th7; A34: sup(F#x1) = sup((F#x1)^\N1) by A31,RINFSUP2:26; lim(F#x1) = sup(F#x1) by A31,RINFSUP2:37; then lim(F#x1) = +infty by A32,A34,A33,RINFSUP2:37; then (lim F).x1 = +infty by A1,A22,A30,MESFUNC8:def 9; then x in eq_dom(lim F,+infty) by A26,A30,MESFUNC1:def 15; hence thesis by A30,XBOOLE_0:def 4; end; A35: for n,m be Nat st m<=n holds I.m<=I.n proof let n,m be Nat; A36: F.m is_measurable_on E by A4; assume m <= n; then A37: for x be Element of X st x in E holds (F.m).x <= (F.n).x by A5; A38: E = dom(F.m) by A1,A3; A39: E = dom(F.n) by A1,A3; A40: n in NAT by ORDINAL1:def 12; A41: m in NAT by ORDINAL1:def 12; F.n is_measurable_on E by A4; then Integral(M,(F.m)|E) <= Integral(M,(F.n)|E) by A8,A38,A39,A36,A37 ,Th15; then Integral(M,F.m) <= Integral(M,(F.n)|E) by A38; then Integral(M,F.m) <= Integral(M,F.n) by A39; then I.m <= Integral(M,F.n) by A19,A41; hence thesis by A19,A40; end; then A42: I is non-decreasing by RINFSUP2:7; then A43: I^\N1 is non-decreasing by RINFSUP2:26; F.N is nonnegative by A8; then Integral(M,(F.N)|EE) = +infty by A13,A14,A17,Th13,MESFUNC5:15; then +infty <= Integral(M,F.N) by A10,A18; then A44: Integral(M,F.N) = +infty by XXREAL_0:4; for k be Element of NAT holds +infty <= (I^\N1).k proof let k be Element of NAT; I.N1 <= I.(N1+k) by A35,NAT_1:12; then I.N1 <= (I^\N1).k by NAT_1:def 3; hence thesis by A44,A21; end; then I^\N1 is convergent_to_+infty by RINFSUP2:32; then A45: lim(I^\N1) = +infty by Th7; E /\ eq_dom(lim F,+infty) is Element of S by A7,A26,MESFUNC1:33; then A46: M.(E /\ eq_dom(lim F,+infty)) <> 0 by A27,A20,MEASURE1:31; A47: sup I = sup(I^\N1) by A42,RINFSUP2:26; lim I = sup I by A42,RINFSUP2:37; then lim I = +infty by A43,A47,A45,RINFSUP2:37; hence thesis by A7,A21,A42,A26,A25,A46,Th13,RINFSUP2:37; end; suppose A48: for n be Nat holds M.(E /\ eq_dom(F.n,+infty)) = 0; defpred L[Element of NAT,set] means $2 = E /\ eq_dom(F.$1,+infty); A49: for n be Element of NAT ex A be Element of S st L[n,A] proof let n be Element of NAT; E c= dom(F.n) by A1,A3; then reconsider A = E /\ eq_dom(F.n,+infty) as Element of S by A4, MESFUNC1:33; take A; thus thesis; end; consider L be sequence of S such that A50: for n be Element of NAT holds L[n,L.n] from FUNCT_2:sch 3(A49); A51: rng L c= S by RELAT_1:def 19; rng L is N_Sub_set_fam of X by MEASURE1:23; then reconsider E0 = rng L as N_Measure_fam of S by A51,MEASURE2:def 1; set E1 = E\(union E0); deffunc H(Nat) = (F.$1)|E1; consider H be Functional_Sequence of X,ExtREAL such that A52: for n be Nat holds H.n = H(n) from SEQFUNC:sch 1; deffunc I2(Element of NAT) = Integral(M,(F.$1)|E1); consider I be sequence of ExtREAL such that A53: for n be Element of NAT holds I.n = I2(n) from FUNCT_2:sch 4; reconsider I as ExtREAL_sequence; A54: E1 c= E by XBOOLE_1:36; then A55: for n be Nat holds F.n is_measurable_on E1 by A4,MESFUNC1:30; A56: for n be Nat holds dom(H.n) = E1 & H.n is without-infty & H.n is without+infty proof let n be Nat; A57: dom(H.n) = dom((F.n)|E1) by A52; E1 c= dom(F.n) by A1,A3,A54; hence dom(H.n) = E1 by A57,RELAT_1:62; (F.n)|E1 is nonnegative by A8,MESFUNC5:15; then H.n is nonnegative by A52; hence H.n is without-infty by MESFUNC5:12; for x be set st x in dom(H.n) holds (H.n).x < +infty proof reconsider n1 = n as Element of NAT by ORDINAL1:def 12; let x be set; A58: L.n = E /\ eq_dom(F.n1,+infty) by A50; dom L = NAT by FUNCT_2:def 1; then A59: L.n in rng L by A58,FUNCT_1:3; assume x in dom(H.n); then A60: x in dom((F.n)|E1) by A52; then A61: x in E1 by RELAT_1:57; A62: x in dom(F.n) by A60,RELAT_1:57; assume A63: (H.n).x >= +infty; (H.n).x = ((F.n)|E1).x by A52; then (H.n).x = (F.n).x by A61,FUNCT_1:49; then (F.n).x = +infty by A63,XXREAL_0:4; then x in eq_dom(F.n,+infty) by A62,MESFUNC1:def 15; then x in L.n by A54,A61,A58,XBOOLE_0:def 4; then x in union E0 by A59,TARSKI:def 4; hence contradiction by A61,XBOOLE_0:def 5; end; hence thesis by MESFUNC5:11; end; for n,m be Nat holds dom(H.n) = dom(H.m) proof let n,m be Nat; dom(H.n) = E1 by A56; hence thesis by A56; end; then reconsider H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2; defpred G[Nat,set,set] means $3 = H.($1+1) - H.($1); A64: for n being Nat for x being set ex y being set st G[n,x,y ]; consider G being Function such that A65: dom G = NAT & G.0 = H.0 & for n being Nat holds G[n,G .n,G.(n+1)] from RECDEF_1:sch 1(A64); A66: for n be Nat holds G.(n+1) = H.(n+1)-H.n by A65; now defpred IND[Nat] means G.$1 is PartFunc of X,ExtREAL; let f be object; assume f in rng G; then consider m be object such that A67: m in dom G and A68: f = G.m by FUNCT_1:def 3; reconsider m as Nat by A65,A67; A69: for n be Nat st IND[n] holds IND[n+1] proof let n be Nat; assume IND[n]; G.(n+1) = H.(n+1) - H.n by A66; hence thesis; end; A70: IND[ 0 ] by A65; for n be Nat holds IND[n] from NAT_1:sch 2(A70,A69); then G.m is PartFunc of X,ExtREAL; hence f in PFuncs(X,ExtREAL) by A68,PARTFUN1:45; end; then rng G c= PFuncs(X,ExtREAL); then reconsider G as Functional_Sequence of X,ExtREAL by A65,FUNCT_2:def 1 ,RELSET_1:4; A71: for n be Nat holds dom(G.n) = E1 proof let n be Nat; now assume n <> 0; then consider k be Nat such that A72: n = k+1 by NAT_1:6; A73: H.(k+1) is without-infty by A56; A74: H.k is without+infty by A56; G.(k+1) = H.(k+1) - H.k by A66; then dom(G.(k+1)) = dom(H.(k+1)) /\ dom(H.k) by A73,A74,MESFUNC5:17; then dom(G.(k+1)) = E1 /\ dom(H.k) by A56; then dom(G.(k+1)) = E1 /\ E1 by A56; hence thesis by A72; end; hence thesis by A56,A65; end; A75: for n,m be Nat holds dom(G.n) = dom(G.m) proof let n,m be Nat; dom(G.n) = E1 by A71; hence thesis by A71; end; A76: for n be Nat holds G.n is nonnegative proof let n be Nat; A77: n <> 0 implies G.n is nonnegative proof assume n <> 0; then consider k be Nat such that A78: n = k + 1 by NAT_1:6; A79: G.(k+1) = H.(k+1) - H.k by A66; for x be object st x in dom(G.(k+1)) holds 0 <= (G.(k+1)).x proof let x be object; assume A80: x in dom(G.(k+1)); A81: dom(G.(k+1)) = E1 by A71; (H.k).x = ((F.k)|E1).x by A52; then A82: (H.k).x = (F.k).x by A80,A81,FUNCT_1:49; (H.(k+1)).x = ((F.(k+1))|E1).x by A52; then A83: (H.(k+1)).x = (F.(k+1)).x by A80,A81,FUNCT_1:49; (F.k).x <= (F.(k+1)).x by A5,A54,A80,A81,NAT_1:11; then (H.(k+1)).x - (H.k).x >= 0 by A83,A82,XXREAL_3:40; hence thesis by A79,A80,MESFUNC1:def 4; end; hence thesis by A78,SUPINF_2:52; end; n = 0 implies G.n is nonnegative proof assume A84: n = 0; (F.n)|E1 is nonnegative by A8,MESFUNC5:15; hence thesis by A52,A65,A84; end; hence thesis by A77; end; A85: for n1 be object st n1 in NAT holds H.n1 = (Partial_Sums G).n1 proof defpred PH[Nat] means H.$1 = (Partial_Sums G).$1; let n1 be object; assume n1 in NAT; then reconsider n = n1 as Nat; A86: for k be Nat st PH[k] holds PH[k+1] proof let k be Nat; A87: H.k is without+infty by A56; A88: H.k is without-infty by A56; A89: dom(G.(k+1)) = E1 by A71; G.(k+1) is without-infty by A76,MESFUNC5:12; then dom(G.(k+1) + H.k) = dom(G.(k+1)) /\ dom(H.k) by A88,MESFUNC5:16; then dom(G.(k+1) + H.k) = E1 /\ E1 by A56,A89; then A90: dom(H.(k+1)) = dom(G.(k+1) + H.k) by A56; A91: G.(k+1) = H.(k+1) - H.k by A66; for x being Element of X st x in dom(H.(k+1)) holds (H.(k+1)).x = (G.(k+1) + H.k).x proof let x be Element of X; A92: (H.k).x <> +infty by A87; (H.k).x <> -infty by A88; then ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x - ( (H.k).x - (H.k).x ) by A92,XXREAL_3:32; then ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x - 0. by XXREAL_3:7; then A93: ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x by XXREAL_3:4; assume A94: x in dom(H.(k+1)); then x in E1 by A56; then (H.(k+1)).x = (G.(k+1)).x + (H.k).x by A91,A89,A93, MESFUNC1:def 4; hence thesis by A90,A94,MESFUNC1:def 3; end; then A95: H.(k+1) = G.(k+1) + H.k by A90,PARTFUN1:5; assume PH[k]; hence thesis by A95,Def4; end; A96: PH[ 0 ] by A65,Def4; for k be Nat holds PH[k] from NAT_1:sch 2(A96,A86); then H.n = (Partial_Sums G).n; hence thesis; end; then A97: for n be Nat holds H.n = (Partial_Sums G).n & lim H = lim( Partial_Sums G) by FUNCT_2:12; reconsider G as with_the_same_dom Functional_Sequence of X,ExtREAL by A75, MESFUNC8:def 2; reconsider G as additive with_the_same_dom Functional_Sequence of X, ExtREAL by A76,Th30; A98: for k be Nat holds H.k is real-valued proof let k be Nat; for x be Element of X st x in dom(H.k) holds |. (H.k).x .| < +infty proof let x be Element of X; assume x in dom(H.k); H.k is without+infty by A56; then A99: (H.k).x < +infty; H.k is without-infty by A56; then -infty < (H.k).x; hence thesis by A99,EXTREAL1:40,XXREAL_0:4; end; hence thesis by MESFUNC2:def 1; end; A100: for n be Nat holds G.n is_measurable_on E1 proof let n be Nat; n <> 0 implies G.n is_measurable_on E1 proof assume n <> 0; then consider k be Nat such that A101: n = k + 1 by NAT_1:6; A102: E1 = dom(H.k) by A56; A103: G.(k+1) = H.(k+1) - H.k by A66; A104: H.k is real-valued by A98; A105: H.k is_measurable_on E1 by A1,A3,A55,A52,Th20,XBOOLE_1:36; A106: H.(k+1) is real-valued by A98; H.(k+1) is_measurable_on E1 by A1,A3,A55,A52,Th20,XBOOLE_1:36; hence thesis by A101,A105,A102,A106,A104,A103,MESFUNC2:11; end; hence thesis by A1,A3,A54,A55,A52,A65,Th20; end; A107: E1 = dom(G.0) by A56,A65; for x be Element of X st x in E1 holds G#x is summable proof let x be Element of X; assume A108: x in E1; E1 c= E by XBOOLE_1:36; then F#x is convergent by A6,A108; then H#x is convergent by A52,A108,Th12; then (Partial_Sums G)#x is convergent by A85,FUNCT_2:12; then Partial_Sums (G#x) is convergent by A107,A108,Th33; hence thesis; end; then consider J be ExtREAL_sequence such that A109: for n be Nat holds J.n = Integral(M,(G.n)|E1) and J is summable and A110: Integral(M,(lim(Partial_Sums G))|E1) = Sum J by A76,A107,A100,Th51; for n be object st n in NAT holds I.n = (Partial_Sums J).n proof let n be object; assume n in NAT; then reconsider n1 = n as Element of NAT; A111: for n be Nat holds J.n = Integral(M,G.n) proof let n be Nat; dom(G.n) = E1 by A71; then (G.n)|E1 = (G.n); hence thesis by A109; end; E1 = dom(G.0) by A71; then (Partial_Sums J).n1 = Integral(M,(Partial_Sums G).n1) by A76,A100 ,A111,Th46; then (Partial_Sums J).n1 = Integral(M,H.n1) by A85; then (Partial_Sums J).n1 = Integral(M,(F.n1)|E1) by A52; hence thesis by A53; end; then A112: I = Partial_Sums J; dom(lim(Partial_Sums G)) = dom(H.0) by A97,MESFUNC8:def 9; then dom(lim(Partial_Sums G)) = E1 by A56; then A113: lim I = Integral(M,lim H) by A97,A110,A112; take I; A114: for x be Element of X st x in E1 holds F#x is convergent proof let x be Element of X; A115: E1 c= E by XBOOLE_1:36; assume x in E1; hence thesis by A6,A115; end; A116: for n be Element of NAT st 0 <= n holds (M*L).n = 0 proof let n be Element of NAT; assume 0 <= n; dom L = NAT by FUNCT_2:def 1; then (M*L).n = M.(L.n) by FUNCT_1:13; then (M*L).n = M.(E /\ eq_dom(F.n,+infty)) by A50; hence thesis by A48; end; M*L is nonnegative by MEASURE2:1; then SUM(M*L) = Ser(M*L).0 by A116,SUPINF_2:48; then SUM(M*L) = (M*L).0 by SUPINF_2:def 11; then SUM(M*L) = 0 by A116; then M.(union E0) <= 0 by MEASURE2:11; then A117: M.(union E0) = 0 by SUPINF_2:51; A118: for n be Nat holds I.n = Integral(M,F.n) proof let n be Nat; reconsider n1=n as Element of NAT by ORDINAL1:def 12; A119: I.n = Integral(M,(F.n1)|E1) by A53; dom(F.n) = E by A1,A3; hence thesis by A4,A117,A119,MESFUNC5:95; end; for n,m be Nat st m <= n holds I.m <= I.n proof let n,m be Nat; A120: F.m is nonnegative by A8; A121: dom(F.m) = E by A1,A3; assume m <= n; then A122: for x be Element of X st x in dom(F.m) holds (F.m).x <= (F.n).x by A5 ,A121; A123: dom(F.n) = E by A1,A3; A124: F.n is_measurable_on E by A4; A125: F.n is nonnegative by A8; F.m is_measurable_on E by A4; then integral+(M,F.m) <= integral+(M,F.n) by A121,A123,A122,A120,A125 ,A124,MESFUNC5:85; then Integral(M,F.m) <= integral+(M,F.n) by A4,A121,A120,MESFUNC5:88; then Integral(M,F.m) <= Integral(M,F.n) by A4,A123,A125,MESFUNC5:88; then I.m <= Integral(M,F.n) by A118; hence thesis by A118; end; then A126: I is non-decreasing by RINFSUP2:7; E = dom(lim F) by A1,MESFUNC8:def 9; then A127: Integral(M,lim F) = Integral(M,(lim F)|E1) by A7,A117,MESFUNC5:95; E1 c= dom(F.0) by A1,XBOOLE_1:36; hence thesis by A127,A52,A118,A126,A114,A113,Th19,RINFSUP2:37; end; end;