:: The Lebesgue Monotone Convergence Theorem :: by Noboru Endou , Keiko Narita and Yasunari Shidama :: :: Received March 18, 2008 :: Copyright (c) 2008 Association of Mizar Users environ vocabularies PARTFUN1, MEASURE1, RELAT_1, FUNCT_1, ORDINAL2, COMPLEX1, SEQ_1, SEQ_2, MEASURE6, BOOLE, ARYTM, ARYTM_1, MESFUNC1, TARSKI, ARYTM_3, SQUARE_1, RLVECT_1, GROUP_1, PROB_1, INTEGRA1, MESFUNC2, MESFUNC5, SUPINF_1, SUPINF_2, FUNCT_3, SEQFUNC, TDGROUP, SERIES_1, RFUNCT_3, SETFAM_1, GRCAT_1, MESFUNC8, MESFUNC9, FUNCT_2, SEQM_3, RINFSUP1, FINSET_1, MEASURE2, VALUED_0, XXREAL_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, VALUED_0, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, FUNCT_2, PARTFUN1, NAT_1, MEMBERED, PROB_1, SETFAM_1, SUPINF_1, SUPINF_2, SEQ_1, KURATO_2, XXREAL_2, MEASURE1, MEASURE2, EXTREAL1, MESFUNC1, MEASURE6, MESFUNC2, LIMFUNC1, SEQFUNC, MESFUNC5, MESFUNC8, RINFSUP2; constructors REAL_1, NAT_1, EXTREAL1, EXTREAL2, BINOP_1, SEQ_1, NEWTON, MESFUNC1, MEASURE2, MESFUNC3, MEASURE6, MESFUNC2, LIMFUNC1, KURATO_2, MESFUNC5, MESFUNC8, RINFSUP2, VALUED_0, SUPINF_1; registrations SUBSET_1, NAT_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, STRUCT_0, MEASURE1, FUNCT_2, RELAT_1, XBOOLE_0, NUMBERS, XXREAL_0, XCMPLX_0, MESFUNC8, FUNCT_1, VALUED_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions SUPINF_2, MESFUNC1, MEASURE6, MESFUNC5, XXREAL_0, BINOP_1, RINFSUP2, MESFUNC8, TARSKI; theorems TARSKI, SUPINF_1, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, EXTREAL2, MESFUNC1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, MESFUNC2, XREAL_1, XXREAL_0, MESFUNC5, PROB_1, NAT_1, RELAT_1, FUNCT_3, ZFMISC_1, FUNCT_2, MEASURE1, MESFUNC6, MEASURE6, SEQFUNC, ORDINAL1, REAL_1, SETFAM_1, MESFUNC8, RINFSUP2, KURATO_2, MESFUNC7, SEQ_4, RELSET_1, MEASURE2, XXREAL_2; schemes FUNCT_2, NAT_1, BINOP_1, RECDEF_1, SEQFUNC, FUNCT_1; begin :: Preliminaries reserve X for non empty set, S for SigmaField of X, M for sigma_Measure of S, E,E1 for Element of S, F,G for Functional_Sequence of X,ExtREAL, I for ExtREAL_sequence, f,g for PartFunc of X,ExtREAL, seq, seq1, seq2 for ExtREAL_sequence, p for ext-real number, n,m for Nat, x for Element of X, z,D for set; theorem M5th22: f is without+infty & g is without+infty implies dom(f+g)=dom f /\ dom g proof assume f is without+infty & g is without+infty; then not +infty in rng f & not +infty in rng g by MESFUNC5:def 4; then f"{+infty} = {} & g"{+infty} = {} by FUNCT_1:142; then f"{+infty} /\ g"{-infty} \/ f"{-infty} /\ g"{+infty} = {}; then dom(f+g) = (dom f /\ dom g)\{} by MESFUNC1:def 3; hence dom(f+g)=dom f /\ dom g; end; theorem M5th23: f is without+infty & g is without-infty implies dom(f-g)=dom f /\ dom g proof assume f is without+infty & g is without-infty; then not -infty in rng g & not +infty in rng f by MESFUNC5:def 3,def 4; then g"{-infty} = {} & f"{+infty} = {} by FUNCT_1:142; then g"{+infty} /\ f"{+infty} \/ g"{-infty} /\ f"{-infty} = {}; then dom(f-g) = (dom f /\ dom g)\{} by MESFUNC1:def 4; hence thesis; end; theorem ADD1a: f is without-infty & g is without-infty implies f+g is without-infty proof assume A1: f is without-infty & g is without-infty; then P2:dom(f+g)=dom f /\ dom g by MESFUNC5:22; for x be set st x in dom(f+g) holds -infty < (f+g).x proof let x be set; assume B1: x in dom(f+g); then x in dom f & x in dom g by P2,XBOOLE_0:def 3; then B2: -infty < f.x & -infty < g.x by A1,MESFUNC5:16; (f+g).x = f.x + g.x by B1,MESFUNC1:def 3; hence thesis by B2,XXREAL_0:6,SUPINF_2:9; end; hence thesis by MESFUNC5:16; end; theorem ADD1b: f is without+infty & g is without+infty implies f+g is without+infty proof assume A1: f is without+infty & g is without+infty; then P2:dom(f+g)=dom f /\ dom g by M5th22; for x be set st x in dom(f+g) holds (f+g).x < +infty proof let x be set; assume B1: x in dom(f+g); then x in dom f & x in dom g by P2,XBOOLE_0:def 3; then B2: f.x < +infty & g.x < +infty by A1,MESFUNC5:17; (f+g).x = f.x + g.x by B1,MESFUNC1:def 3; hence thesis by B2,XXREAL_0:4,SUPINF_2:8; end; hence thesis by MESFUNC5:17; end; theorem f is without-infty & g is without+infty implies f-g is without-infty proof assume A1: f is without-infty & g is without+infty; then P2:dom(f-g)=dom f /\ dom g by MESFUNC5:23; for x be set st x in dom(f-g) holds -infty < (f-g).x proof let x be set; assume B1: x in dom(f-g); then x in dom f & x in dom g by P2,XBOOLE_0:def 3; then B2: -infty < f.x & g.x < +infty by A1,MESFUNC5:16,17; (f-g).x = f.x - g.x by B1,MESFUNC1:def 4; hence thesis by B2,XXREAL_0:6,SUPINF_2:11; end; hence thesis by MESFUNC5:16; end; theorem f is without+infty & g is without-infty implies f-g is without+infty proof assume A1: f is without+infty & g is without-infty; then P2:dom(f-g)=dom f /\ dom g by M5th23; for x be set st x in dom(f-g) holds (f-g).x < +infty proof let x be set; assume B1: x in dom(f-g); then x in dom f & x in dom g by P2,XBOOLE_0:def 3; then B2: f.x < +infty & -infty < g.x by A1,MESFUNC5:16,17; (f-g).x = f.x - g.x by B1,MESFUNC1:def 4; hence thesis by B2,XXREAL_0:4,SUPINF_2:10; end; hence thesis by MESFUNC5:17; end; theorem LIM: ( seq is convergent_to_finite_number implies ex g be real number st lim seq = g & for p be real number st 0

= 0 by A1,A2,SUPINF_2:70; hence contradiction; end; theorem LIM3: seq is convergent & (for k be Nat holds seq.k <= p) implies lim seq <= p proof assume that A1: seq is convergent and A2: for k be Nat holds seq.k <= p; for y be ext-real number holds y in rng seq implies y <= p proof let y be ext-real number; assume y in rng seq; then consider x be set such that A4: x in dom seq & y = seq.x by FUNCT_1:def 5; reconsider x as Nat by A4; seq.x <= p by A2; hence y <= p by A4; end; then B1:p is UpperBound of rng seq by XXREAL_2:def 1; reconsider SUPSEQ = superior_realsequence seq as Function of NAT,ExtREAL; for n be Element of NAT holds inf SUPSEQ <= SUPSEQ.n proof let n be Element of NAT; NAT = dom SUPSEQ by FUNCT_2:def 1; then SUPSEQ.n in rng SUPSEQ by FUNCT_1:def 5; hence thesis by XXREAL_2:3; end; then B2:inf SUPSEQ <= SUPSEQ.0; consider Y be non empty Subset of ExtREAL such that A9: Y = {seq.k where k is Element of NAT: 0 <= k} & SUPSEQ.0 = sup Y by RINFSUP2:def 7; now let x be set; assume x in Y; then C1: ex k be Element of NAT st x = seq.k & 0 <= k by A9; dom seq = NAT by FUNCT_2:def 1; hence x in rng seq by C1,FUNCT_1:12; end; then C2:Y c= rng seq by TARSKI:def 3; now let x be set; assume x in rng seq; then consider k be set such that C3: k in dom seq & x = seq.k by FUNCT_1:def 5; reconsider k as Element of NAT by C3; thus x in Y by A9,C3; end; then rng seq c= Y by TARSKI:def 3; then Y = rng seq by C2,XBOOLE_0:def 10; then (superior_realsequence seq).0 <= p by B1,A9,XXREAL_2:def 3; then lim_sup seq <= p by B2,XXREAL_0:2; hence lim seq <= p by A1,RINFSUP2:41; end; theorem LIM3a: seq is convergent & (for k be Nat holds p <= seq.k) implies p <= lim seq proof assume that A1: seq is convergent and A2: for k be Nat holds p <= seq.k; for y be ext-real number holds y in rng seq implies p <= y proof let y be ext-real number; assume y in rng seq; then consider x be set such that A4: x in dom seq & y = seq.x by FUNCT_1:def 5; reconsider x as Nat by A4; seq.x >= p by A2; hence y >= p by A4; end; then B1:p is LowerBound of rng seq by XXREAL_2:def 2; reconsider INFSEQ = inferior_realsequence seq as Function of NAT,ExtREAL; 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 5; hence thesis by XXREAL_2:4; end; then B2:sup INFSEQ >= INFSEQ.0; consider Y be non empty Subset of ExtREAL such that A9: Y = {seq.k where k is Element of NAT: 0 <= k} & INFSEQ.0 = inf Y by RINFSUP2:def 6; now let x be set; assume x in Y; then C1: ex k be Element of NAT st x = seq.k & 0 <= k by A9; dom seq = NAT by FUNCT_2:def 1; hence x in rng seq by C1,FUNCT_1:12; end; then C2:Y c= rng seq by TARSKI:def 3; now let x be set; assume x in rng seq; then consider k be set such that C3: k in dom seq & x = seq.k by FUNCT_1:def 5; reconsider k as Element of NAT by C3; thus x in Y by A9,C3; end; then rng seq c= Y by TARSKI:def 3; then Y = rng seq by C2,XBOOLE_0:def 10; then (inferior_realsequence seq).0 >= p by B1,A9,XXREAL_2:def 4; then lim_inf seq >= p by B2,XXREAL_0:2; hence lim seq >= p by A1,RINFSUP2:41; end; theorem LIM2: 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 & seq2 is convergent and A2: seq1 is nonnegative & seq2 is nonnegative and A3: for k be Nat holds seq.k = seq1.k + seq2.k; A4:not seq1 is convergent_to_-infty & not seq2 is convergent_to_-infty by A2,LIM2a; for n be set st n in dom seq holds 0. <= seq.n proof let n be set; assume n in dom seq; then reconsider n1=n as Nat; C1: 0 <= seq1.n1 & 0 <= seq2.n1 by A2,SUPINF_2:70; seq.n1 = seq1.n1 + seq2.n1 by A3; hence thesis by C1,SUPINF_2:20; end; hence seq is nonnegative by SUPINF_2:71; for n be Nat holds 0 <= seq2.n by A2,SUPINF_2:70; then B2:lim seq2 <> -infty by A1,LIM3a; per cases by A4,A1,MESFUNC5:def 11; suppose A5: seq1 is convergent_to_+infty; for g be real number st 0 < g ex n be Nat st for m be Nat st n<=m holds g <= seq.m proof let g be real number; assume 0 < g; then consider n be Nat such that A7: for m be Nat st n <= m holds g <= seq1.m by A5,MESFUNC5:def 9; take n; let m be Nat; assume n<=m; then g <= seq1.m & 0 <= seq2.m by A2,A7,SUPINF_2:70; then R_EAL g + 0. <= seq1.m + seq2.m by SUPINF_2:14; then g <= seq1.m + seq2.m by SUPINF_2:18; hence g <= seq.m by A3; end; then A9: seq is convergent_to_+infty by MESFUNC5:def 9; hence seq is convergent by MESFUNC5:def 11; then lim seq = +infty & lim seq1 = +infty by A1,A5,A9,MESFUNC5:def 12; hence lim seq = lim seq1 + lim seq2 by B2,SUPINF_2:def 2; end; suppose seq1 is convergent_to_finite_number; then not seq1 is convergent_to_+infty & not seq1 is convergent_to_-infty by MESFUNC5:56,57; then consider g be real number such that B3: lim seq1 = g & (for p be real number st 0

-infty & seq1.m - R_EAL g <> -infty by SUPINF_2:11; R_EAL(g+h) = g+h & R_EAL g = g' & R_EAL h = h'; then R_EAL(g+h) = R_EAL g + R_EAL h by SUPINF_2:1; then seq.m - R_EAL(g+h) = seq.m - R_EAL h - R_EAL g by EXTREAL2:40 .= seq1.m + seq2.m - R_EAL h - R_EAL g by A3 .= seq1.m + (seq2.m - R_EAL h) - R_EAL g by D3,EXTREAL1:11 .= (seq2.m - R_EAL h) + (seq1.m - R_EAL g) by D3,D4,EXTREAL1:11; then E0: |. seq.m - R_EAL(g+h) .| <= |. seq2.m - R_EAL h .| + |. seq1.m - R_EAL g .| by D4,EXTREAL2:61; E1: |. seq1.m - lim seq1 .| < p/2 & |. seq2.m - lim seq2 .| < p/2 by D0,C5,C6; then |. seq1.m - lim seq1 .| < +infty & |. seq2.m - lim seq2 .| < +infty by XXREAL_0:2,9; then seq1.m - R_EAL g in REAL & seq2.m - R_EAL h in REAL by B3,C3,EXTREAL2:102; then consider e1,e2 be Real such that E2: e1 = seq1.m - R_EAL g & e2 = seq2.m - R_EAL h; E3: |. seq1.m - R_EAL g .| = |.e1.| & |. seq2.m - R_EAL h .| = |.e2.| by E2,EXTREAL2:49; then E4: |. seq2.m - R_EAL h .| + |. seq1.m - R_EAL g .| = |.e1.| + |.e2.| by SUPINF_2:1; |.e1.| + |.e2.| < p/2 + p/2 by E1,B3,C3,E3,XREAL_1:10; hence |. seq.m - R_EAL(g+h) .| < p by E0,E4,XXREAL_0:2; end; then E5: seq is convergent_to_finite_number by MESFUNC5:def 8; hence seq is convergent by MESFUNC5:def 11; then lim seq = g'+h' by E5,C9,MESFUNC5:def 12; hence lim seq = lim seq1 + lim seq2 by B3,C3,SUPINF_2:1; end; end; end; theorem Lm16: (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 A2: for n be Nat holds G.n = (F.n)|D and A3: x in D; thus V1: F#x is convergent_to_+infty implies G#x is convergent_to_+infty proof assume B1: F#x is convergent_to_+infty; let g be real number; assume 0 < g; then consider n be Nat such that B2: for m be Nat st n <= m holds g <= (F#x).m by B1,MESFUNC5:def 9; take n; let m be Nat; assume n <= m; then g <= (F#x).m by B2; then g <= (F.m).x by MESFUNC5:def 13; then g <= ((F.m)|D).x by A3,FUNCT_1:72; then g <= (G.m).x by A2; hence g <= (G#x).m by MESFUNC5:def 13; end; thus V2: F#x is convergent_to_-infty implies G#x is convergent_to_-infty proof assume C1: F#x is convergent_to_-infty; let g be real number; assume g < 0; then consider n be Nat such that C2: for m be Nat st n <= m holds (F#x).m <= g by C1,MESFUNC5:def 10; take n; let m be Nat; assume n <= m; then (F#x).m <= g by C2; then (F.m).x <= g by MESFUNC5:def 13; then ((F.m)|D).x <= g by A3,FUNCT_1:72; then (G.m).x <= g by A2; hence (G#x).m <= g by MESFUNC5:def 13; end; thus V3: 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 number such that D1: lim(F#x) = g & for p be real number st 0

0 implies Integral(M,f) = +infty proof assume that A1: E = dom f & f is_measurable_on E & f is nonnegative and A2: M.(E /\ eq_dom(f,+infty)) <> 0; reconsider EE = E /\ eq_dom(f,+infty) as Element of S by A1,MESFUNC1:37; A3:f|EE is nonnegative & f|E is nonnegative by A1,MESFUNC5:21; E = dom f /\ E by A1; then A4:f|E is_measurable_on E by A1,MESFUNC5:48; A5:dom(f|E) = E by A1,RELAT_1:91; integral+(M,f|EE) <= integral+(M,f|E) by A1,XBOOLE_1:17,MESFUNC5:89; then A6:integral+(M,f|EE) <= Integral(M,f|E) by A1,A4,A5,MESFUNC5:21,94; A8:f is_measurable_on EE by A1,XBOOLE_1:17,MESFUNC1:34; A9:dom(f|EE) = EE by A1,XBOOLE_1:17,RELAT_1:91; EE = dom f /\ EE by A1,XBOOLE_1:17,XBOOLE_1:28; then A10: f|EE is_measurable_on EE by A8,MESFUNC5:48; deffunc G(Element of NAT) = $1(#)((chi(EE,X))|EE); consider G be Function such that B1: dom G = NAT & for n be Element of NAT holds G.n = G(n) from FUNCT_1:sch 4; now let g be set; assume g in rng G; then consider m be set such that B2: m in dom G & g = G.m by FUNCT_1:def 5; reconsider m as Element of NAT by B1,B2; g = m(#)((chi(EE,X))|EE) by B1,B2; hence g in PFuncs(X,ExtREAL) by PARTFUN1:119; end; then rng G c= PFuncs(X,ExtREAL) by TARSKI:def 3; then reconsider G as Functional_Sequence of X,ExtREAL by B1,SEQFUNC:def 1; B8: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 13; B3: G.n = n1(#)((chi(EE,X))|EE) by B1; EE c= X; then EE c= dom(chi(EE,X)) by FUNCT_3:def 3; then B6: dom((chi(EE,X))|EE) = EE by RELAT_1:91; hence B4: dom(G.n) = EE by B3,MESFUNC1:def 6; let x be set; assume B5:x in dom(G.n); then reconsider x1=x as Element of X; chi(EE,X).x1 = 1. by B4,B5,FUNCT_3:def 3; then ((chi(EE,X))|EE).x1 = 1. by B5,B4,B6,FUNCT_1:70; then (G.n).x = (R_EAL n1) * 1. by B3,B5,MESFUNC1:def 6; hence (G.n).x = n by EXTREAL2:4; end; C1:for n be Nat holds dom(G.n) = dom(f|EE) & G.n is_simple_func_in S proof let n be Nat; thus C2: dom(G.n) = dom(f|EE) by A9,B8; reconsider n1 = n as Element of NAT by ORDINAL1:def 13; for x be set st x in dom(G.n) holds (G.n).x = n1 by B8; hence G.n is_simple_func_in S by C2,A9,MESFUNC6:2; end; H1:for n be Nat holds G.n is nonnegative proof let n be Nat; for x be set st x in dom(G.n) holds 0 <= (G.n).x by B8; hence G.n is nonnegative by SUPINF_2:71; end; D1: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 D3: n <= m; let x be Element of X; assume x in dom(f|EE); then x in dom(G.n) & x in dom(G.m) by B8,A9; then (G.n).x = n & (G.m).x = m by B8; hence (G.n).x <= (G.m).x by D3; end; E1: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 E2: x in dom(f|EE); then E3: x in EE by A1,XBOOLE_1:17,RELAT_1:91; for n,m be Element of NAT st m<=n holds (G#x).m <= (G#x).n proof let n,m be Element of NAT; dom(G.n) = EE & dom(G.m) = EE by B8; then (G.m).x = m & (G.n).x = n by A9,E2,B8; then E4: (G#x).m = m & (G#x).n = n by MESFUNC5:def 13; assume m <= n; hence (G#x).m <= (G#x).n by E4; end; then E5: G#x is non-decreasing by RINFSUP2:7; E6: not rng(G#x) is bounded_above proof assume rng(G#x) is bounded_above; then consider UB be UpperBound of rng(G#x) such that E61: UB in REAL by SUPINF_1:def 11; reconsider r = UB as Real by E61; consider n be Element of NAT such that E62: r < n by SEQ_4:10; dom(G#x) = NAT by FUNCT_2:def 1; then E63: (G#x).n in rng(G#x) by FUNCT_1:12; x in dom(G.n) by B8,E3; then (G.n).x = n by B8; then UB < (G#x).n by E62,MESFUNC5:def 13; hence contradiction by E63,XXREAL_2:def 1; end; sup rng(G#x) is UpperBound of rng(G#x) by XXREAL_2:def 3; then E7: sup(G#x) = +infty by E6,XXREAL_2:53; x in eq_dom(f,+infty) by E3,XBOOLE_0:def 3; then x in dom f & f.x = +infty by MESFUNC1:def 16; then (f|EE).x = +infty by E3,FUNCT_1:72; hence thesis by E5,E7,RINFSUP2:37; end; deffunc K(Element of NAT) = integral'(M,G.$1); consider K be Function of NAT,ExtREAL such that F0: for n be Element of NAT holds K.n = K(n) from FUNCT_2:sch 4; reconsider K as ExtREAL_sequence; F1: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 13; K.n = integral'(M,G.n1) by F0; hence thesis; end; G2:for i be Element of NAT holds K.i = (R_EAL i)*(M.(dom(G.i))) proof let i be Element of NAT; G4: G.i is_simple_func_in S by C1; for x be set st x in dom(G.i) holds (G.i).x = R_EAL i by B8; then integral'(M,G.i) = (R_EAL i)*(M.(dom(G.i))) by G4,MESFUNC5:77; hence thesis by F1; end; reconsider ES = {} as Element of S by PROB_1:42; M.ES <= M.EE by MEASURE1:62,XBOOLE_1:2; then L1:0 < M.EE by A2,MEASURE1:def 11; for n,m be Element of NAT st m <= n holds K.m <= K.n proof let n,m be Element of NAT; assume G5: m <= n; dom(G.m) = EE & dom(G.n) = EE by B8; then K.m = (R_EAL m)*M.EE & K.n = (R_EAL n)*M.EE by G2; hence thesis by G5,L1,EXTREAL1:42; end; then K is non-decreasing by RINFSUP2:7; then G1:K is convergent & lim K = sup K by RINFSUP2:37; G7:not rng K is bounded_above proof assume rng K is bounded_above; then consider UB be UpperBound of rng K such that G71: UB in REAL by SUPINF_1:def 11; reconsider r = UB as Real by G71; per cases by L1,XXREAL_0:10; suppose G73: M.EE = +infty; K.1 = (R_EAL 1) * (M.(dom(G.1))) by G2; then K.1 = (R_EAL 1) * (M.EE) by B8; then G74: K.1 = +infty by G73,EXTREAL1:def 1; dom K = NAT by FUNCT_2:def 1; then K.1 in rng K by FUNCT_1:12; then K.1 <= UB by XXREAL_2:def 1; then UB = +infty by G74,XXREAL_0:4; hence contradiction by G71; end; suppose M.EE in REAL; then reconsider ee = M.EE as Real; reconsider UB as R_eal by XXREAL_0:def 1; consider n be Element of NAT such that G75: r/ee < n by SEQ_4:10; dom K = NAT by FUNCT_2:def 1; then G77: K.n in rng K by FUNCT_1:12; K.n = (R_EAL n) * (M.(dom(G.n))) by G2; then K.n = (R_EAL n) * (M.EE) by B8; then G76: K.n = n * ee by EXTREAL1:13; (r/ee) * ee < n * ee by L1,G75,XREAL_1:70; then r / (ee/ee) < K.n by G76,XCMPLX_1:83; then r < K.n by A2,XCMPLX_1:51; hence contradiction by G77,XXREAL_2:def 1; end; end; sup rng K is UpperBound of rng K by XXREAL_2:def 3; then sup K = +infty by G7,XXREAL_2:53; then integral+(M,f|EE) = +infty by A3,A9,A10,C1,D1,E1,F1,G1,H1,MESFUNC5:def 15; then Integral(M,f|E) = +infty by A6,XXREAL_0:4; hence Integral(M,f) = +infty by A1,RELAT_1:97; end; theorem :: MESFUNC7:24 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:21; A2:XX = dom chi(E,X) & chi(E,X) is_measurable_on XX by FUNCT_3:def 3,MESFUNC2:32; then A3:XX = dom(max+(chi(E,X))) & max+(chi(E,X)) is_measurable_on XX by MESFUNC7:23; set F = XX \ E; for x be set st x in dom max+(chi(E,X)) holds 0. <= (max+(chi(E,X))).x by MESFUNC2:14; then P1:max+(chi(E,X)) is nonnegative by SUPINF_2:71; then P2:(max+(chi(E,X)))|E is nonnegative by MESFUNC5:21; X1:integral+(M,(max+ chi(E,X))|(E\/F)) = integral+(M,(max+ chi(E,X))|E) + integral+(M,(max+ chi(E,X))|F) by A3,P1,MESFUNC5:87,XBOOLE_1:79; A6:XX /\ F = F & XX /\ E = E by XBOOLE_1:28; then A5:dom((max+(chi(E,X)))|F) = F & dom((max+(chi(E,X)))|E) = E by A3,FUNCT_1:68; max+(chi(E,X)) is_measurable_on E & max+(chi(E,X)) is_measurable_on F by A3,MESFUNC1:34; then A8:(max+(chi(E,X)))|E is_measurable_on E & (max+(chi(E,X)))|F is_measurable_on F by A3,A6,MESFUNC5:48; E \/ F = XX by A6,XBOOLE_1:51; then C1:(max+ chi(E,X))|(E\/F) = max+ chi(E,X) by A3,RELAT_1:98; now let x be Element of X; assume B1:x in dom((max+(chi(E,X)))|F); then chi(E,X).x = 0 by A5,FUNCT_3:43; then (max+(chi(E,X))).x = 0 by MESFUNC7:23; hence ((max+(chi(E,X)))|F).x = 0 by B1,FUNCT_1:70; end; then integral+(M,(max+ chi(E,X))|F) = 0 by A5,A8,MESFUNC5:93; then X2:integral+(M,max+ chi(E,X)) = integral+(M,(max+ chi(E,X))|E) by X1,C1,SUPINF_2:18; P3:now let x be set; assume B1:x in dom((max+(chi(E,X)))|E); then chi(E,X).x = 1 by A5,FUNCT_3:def 3; then (max+(chi(E,X))).x = 1 by MESFUNC7:23; hence ((max+(chi(E,X)))|E).x = 1 by B1,FUNCT_1:70; end; then (max+(chi(E,X)))|E is_simple_func_in S by A5,MESFUNC6:2; then integral+(M,max+ chi(E,X)) = integral'(M,(max+ chi(E,X))|E) by X2,P1,MESFUNC5:21,83; then P8:integral+(M,max+ chi(E,X)) = R_EAL 1 * M.(dom((max+(chi(E,X)))|E)) by A5,P3,MESFUNC5:110; P5:XX = dom(max- chi(E,X)) & max- chi(E,X) is_measurable_on XX by A2,MESFUNC2:def 3,28; now let x be Element of X; assume B1:x in dom(max- chi(E,X)); per cases; suppose x in E; then L2: chi(E,X).x = 1 by FUNCT_3:def 3; then ex c be Real st c = chi(E,X).x & -(chi(E,X).x) = -c by SUPINF_2:def 3; then max(-(chi(E,X).x),0.) = 0. by L2,XXREAL_0:def 9; hence (max-(chi(E,X))).x = 0 by B1,MESFUNC2:def 3; end; suppose not x in E; then chi(E,X).x = 0. by FUNCT_3:def 3; then max(-(chi(E,X).x),0.) = 0. by EXTREAL1:24; hence (max-(chi(E,X))).x = 0 by B1,MESFUNC2:def 3; end; end; then QQ:integral+(M,max- chi(E,X)) = 0 by P5,MESFUNC5:93; Integral(M,chi(E,X)) = R_EAL 1 * M.E by P8,A5,QQ,MEASURE6:21; hence Integral(M,chi(E,X)) = M.E by EXTREAL2:4; Q1:E = dom((chi(E,X))|E) & (chi(E,X))|E is_measurable_on E by A5,A8,MESFUNC7:23; Q2:(chi(E,X))|E is nonnegative by P2,MESFUNC7:23; Q3:(chi(E,X))|E = (max+ chi(E,X))|E by MESFUNC7:23; Integral(M,(chi(E,X))|E) =integral+(M,(chi(E,X))|E) by Q1,Q2,MESFUNC5:94; hence Integral(M,(chi(E,X))|E) = M.E by X2,Q3,P8,A5,EXTREAL2:4; end; theorem Prop3: 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 A0: E c= dom f & E c= dom g and A2: f is_measurable_on E & g is_measurable_on E and A3: f is nonnegative and A4: for x be Element of X st x in E holds f.x <= g.x; set F1 = f|E; set F2 = g|E; A5:F1 is nonnegative by A3,MESFUNC5:21; A6:E = dom(f|E) & E = dom(g|E) by A0,RELAT_1:91; A7:for x be Element of X st x in dom F1 holds F1.x <= F2.x proof let x be Element of X; assume E4: x in dom F1; then F1.x = f.x & F2.x = g.x by A6,FUNCT_1:68; hence thesis by E4,A4,A6; end; for x be set st x in dom F2 holds 0 <= F2.x proof let x be set; assume x in dom F2; then 0 <= F1.x & F1.x <= F2.x by A6,A5,A7,SUPINF_2:70; hence 0 <= F2.x; end; then A8:F2 is nonnegative by SUPINF_2:71; A9:dom f /\ E = E & dom g /\ E = E by A0,XBOOLE_1:28; then F1 is_measurable_on E & F2 is_measurable_on E by A2,MESFUNC5:48; then integral+(M,F1) <= integral+(M,F2) by A5,A7,A8,A6,MESFUNC5:91; then Integral(M,F1) <= integral+(M,F2) by A5,A6,A9,A2,MESFUNC5:48,94; hence thesis by A8,A6,A2,A9,MESFUNC5:48,94; end; begin :: Selected Properties of Extended Real Sequence definition :: to be removed in next MML version let f be ext-real-valued Function; let f be ext-real-valued Function, x be set; redefine func f.x -> Element of ExtREAL; coherence by XXREAL_0:def 1; end; 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 Function of NAT,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 & for n be Nat holds s1.(n+1)=s1.n + s.(n+1) and A3: s2.0=s.0 & for n be Nat holds s2.(n+1)=s2.n + s.(n+1); defpred X[Element of NAT] means s1.$1 = s2.$1; A4: X[0] by A2,A3; A5: for k be Element of NAT st X[k] holds X[k+1] proof let k be Element of NAT; assume s1.k =s2.k; hence s1.(k+1) = s2.k + s.(k+1) by A2 .= s2.(k+1) by A3; end; for n be Element of NAT holds X[n] from NAT_1:sch 1(A4,A5); hence s1 = s2 by FUNCT_2:113; end; end; definition let s be ext-real-valued Function; attr s is summable means :Def2: 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 ADD3a: seq is nonnegative implies Partial_Sums seq is nonnegative & Partial_Sums seq is non-decreasing proof set PS = Partial_Sums seq; assume A1: seq is nonnegative; defpred P[Nat] means 0 <= PS.$1; PS.0 = seq.0 by Def1; then A2:P[0] by A1,SUPINF_2:70; A3:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: seq.(k+1) >= 0 by A1,SUPINF_2:70; PS.(k+1) = PS.k + seq.(k+1) by Def1; hence PS.(k+1) >= 0 by A4,A5,SUPINF_2:20; end; A6:for m be Nat holds P[m] from NAT_1:sch 2(A2,A3); for k be set st k in dom PS holds 0 <= PS.k by A6; hence PS is nonnegative by SUPINF_2:71; for n,m be Element of NAT st m <= n holds (Partial_Sums seq).m <= (Partial_Sums seq).n proof let n,m be Element of NAT; reconsider n1=n, m1=m as Nat; assume A7: m <= n; defpred Q[Nat] means PS.m1 <= PS.$1; A8: for k be Nat holds PS.k <= PS.(k+1) proof let k be Nat; A9: PS.(k+1) = PS.k + seq.(k+1) by Def1; 0 <= seq.(k+1) & 0 <= PS.k by A1,A6,SUPINF_2:70; hence thesis by A9,SUPINF_2:20; end; A10: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 A11: k >= m1 and A12: for l be Nat st l >= m1 & l < k holds Q[l]; now assume k > m1; then A13: k >= m1 + 1 by NAT_1:13; per cases by A13,REAL_1:def 5; suppose k = m1 + 1; hence Q[k] by A8; end; suppose A14: k > m1 + 1; then reconsider l = k-1 as Element of NAT by NAT_1:20; k < k+1 by NAT_1:13; then k > l & l >= m1 by A14,XREAL_1:21; then A15: PS.m1 <= PS.l by A12; k = l+1; then PS.l <= PS.k by A8; hence Q[k] by A15,XXREAL_0:2; end; end; hence thesis by A11,REAL_1:def 5; end; for k be Nat st k >= m1 holds Q[k] from NAT_1:sch 9(A10); hence thesis by A7; 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 assume A1: for n be Nat holds 0 < seq.n; defpred P[Nat] means 0 < (Partial_Sums seq).$1; (Partial_Sums seq).0 = seq.0 by Def1; then A2:P[0] by A1; A3:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4:P[k]; A5: seq.(k+1) > 0 by A1; (Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1) by Def1; hence (Partial_Sums seq).(k+1) > 0 by A4,A5,SUPINF_2:20; end; thus for m be Nat holds P[m] from NAT_1:sch 2(A2,A3); end; theorem Lm17: 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.n = (F.n)|D & G.m = (F.m)|D by A2; then dom(G.n) = dom(F.n) /\ D & dom(G.m) = dom(F.m) /\ D by RELAT_1:90; hence dom(G.n) = dom(G.m) by A1,MESFUNC8:def 2; end; theorem Lm15: 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 A4: 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 L2:dom(G.0) = D by A4,RELAT_1:91; L43: dom((lim F)|D) = dom(lim F) /\ D by RELAT_1:90; then dom((lim F)|D) = dom(F.0) /\ D by MESFUNC8:def 10; then dom((lim F)|D) = D by A4,XBOOLE_1:28; then L41: dom((lim F)|D) = dom(lim G) by L2,MESFUNC8:def 10; now let x be Element of X; assume L42: x in dom((lim F)|D); then L44:x in dom(lim F) by L43,XBOOLE_0:def 3; ((lim F)|D).x = (lim F).x by L42,FUNCT_1:70; then L47:((lim F)|D).x = lim(F#x) by L44,MESFUNC8:def 10; L46:x in D by L42,RELAT_1:86; then L45:F#x is convergent by A3; per cases by L45,MESFUNC5:def 11; suppose B0: F#x is convergent_to_+infty; then G#x is convergent_to_+infty by A2,L46,Lm16; then lim(G#x) = +infty by LIM; then (lim G).x = +infty by L41,L42,MESFUNC8:def 10; hence (lim G).x = ((lim F)|D).x by L47,B0,LIM; end; suppose B0: F#x is convergent_to_-infty; then G#x is convergent_to_-infty by A2,L46,Lm16; then lim(G#x) = -infty by LIM; then (lim G).x = -infty by L41,L42,MESFUNC8:def 10; hence (lim G).x = ((lim F)|D).x by L47,B0,LIM; end; suppose B0: F#x is convergent_to_finite_number; then consider g be real number such that B4: lim(F#x) = g & for p be real number st 0

Functional_Sequence of X,ExtREAL means :Def0: it.0 = F.0 & for n be Nat holds it.(n+1) = it.n + F.(n+1); existence proof defpred P[Element of 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)); P1:for n being Element of NAT for x being set ex y being set st P[n,x,y] proof let n be Element of NAT; let x be set; thus ex y be set st P[n,x,y] proof per cases; suppose P11: 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 P11; 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; P2:for n being Element of NAT for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1=y2 proof let n be Element of NAT; let x,y1,y2 be set; assume P20: P[n,x,y1] & P[n,x,y2]; per cases; suppose not x is PartFunc of X,ExtREAL; hence y1 = y2 by P20; end; suppose x is PartFunc of X,ExtREAL; then reconsider F2 = x as PartFunc of X,ExtREAL; y1 = F2 + F.(n+1) & y2 = F2 + F.(n+1) by P20; hence y1 = y2; end; end; consider IT being Function such that P3: dom IT = NAT & IT.0 = F.0 & for n being Element of NAT holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(P1,P2); now let f be set; assume f in rng IT; then consider m be set such that P41: m in dom IT & f = IT.m by FUNCT_1:def 5; reconsider m as Element of NAT by P41,P3; defpred IND[Element of NAT] means IT.$1 is PartFunc of X,ExtREAL; P42:IND[0] by P3; P43:for n be Element of NAT st IND[n] holds IND[n+1] proof let n be Element of NAT; assume IND[n]; then reconsider F2 = IT.n as PartFunc of X,ExtREAL; IT.(n+1) = F2 + F.(n+1) by P3; hence IND[n+1]; end; for n be Element of NAT holds IND[n] from NAT_1:sch 1(P42,P43); then IT.m is PartFunc of X,ExtREAL; hence f in PFuncs(X,ExtREAL) by P41,PARTFUN1:119; end; then rng IT c= PFuncs(X,ExtREAL) by TARSKI:def 3; then reconsider IT as Functional_Sequence of X,ExtREAL by P3,SEQFUNC:def 1; take IT; for n be Nat holds IT.(n+1) = IT.n + F.(n+1) proof let n be Nat; reconsider m = n as Element of NAT by ORDINAL1:def 13; IT.(m+1) = IT.m + F.(m+1) by P3; hence IT.(n+1) = IT.n + F.(n+1); end; hence thesis by P3; end; uniqueness proof let PS1,PS2 be Functional_Sequence of X,ExtREAL; assume that A1: PS1.0 = F.0 & for n be Nat holds PS1.(n+1) = PS1.n + F.(n+1) and A2: PS2.0 = F.0 & for n be Nat holds PS2.(n+1) = PS2.n + F.(n+1); defpred IND[Nat] means PS1.$1 = PS2.$1; P1:IND[0] by A1,A2; P2:for n be Nat st IND[n] holds IND[n+1] proof let n be Nat; assume P21: IND[n]; PS1.(n+1) = PS1.n + F.(n+1) by A1; hence PS1.(n+1) = PS2.(n+1) by A2,P21; end; for n be Nat holds IND[n] from NAT_1:sch 2(P1,P2); then for m be Element of NAT holds PS1.m = PS2.m; hence thesis by SEQFUNC:2; end; end; definition let X be set, F be Functional_Sequence of X,ExtREAL; attr F is additive means :Def1a: 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; Lem01: z in dom((Partial_Sums F).n) & m <= n implies z in dom((Partial_Sums F).m) proof set PF = Partial_Sums F; assume A1: z in dom(PF.n) & m <= n; assume A2: not z in dom(PF.m); defpred P[Nat] means m <= $1 & $1 <= n implies not z in dom(PF.$1); A3:P[0] by A2; A4:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A5: P[k]; assume A6:m <= k+1 & k+1 <= n; per cases by A6,NAT_1:8; suppose m <= k; then A7: not z in dom(PF.k) /\ dom(F.(k+1)) by A5,A6,NAT_1:13,XBOOLE_0:def 3; PF.(k+1) = PF.k + F.(k+1) by Def0; then 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; hence not z in dom(PF.(k+1)) by A7,XBOOLE_0:def 4; end; suppose m = k+1; hence not z in dom(PF.(k+1)) by A2; end; end; for k be Nat holds P[k] from NAT_1:sch 2(A3,A4); hence contradiction by A1; end; theorem Lem02: 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 A1: z in dom(PF.n) & m <= n; hence A2: z in dom(PF.m) by Lem01; per cases; suppose m = 0; then PF.m = F.m by Def0; hence z in dom(F.m) by A1,Lem01; end; suppose m <> 0; then consider k be Nat such that A5: m = k + 1 by NAT_1:6; PF.m = PF.k + F.m by A5,Def0; 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 A2,XBOOLE_0:def 4; hence z in dom(F.m) by XBOOLE_0:def 3; end; end; theorem Lem03: 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 A2: z in dom(PF.n) & (PF.n).z = +infty; now assume A4:for m be Element of NAT st m <= n holds (F.m).z <> +infty; defpred P[Nat] means $1 <= n implies (PF.$1).z <> +infty; PF.0 = F.0 by Def0; then A5: P[0] by A4; A6: for k being Nat st P[k] holds P[k + 1] proof let k be Nat; assume B1: P[k]; assume B2: k+1 <= n; then k <= n by NAT_1:13; then z in dom(PF.k) & z in dom(F.(k+1)) by A2,B2,Lem02; then B3: z in dom(PF.k) /\ dom(F.(k+1)) by XBOOLE_0:def 3; B4: (PF.k).z <> +infty & (F.(k+1)).z <> +infty by A4,B1,B2,NAT_1:13; then not( (PF.k).z in {+infty} ) & not( (F.(k+1)).z in {+infty} ) by TARSKI:def 1; then not z in (PF.k)"{+infty} & not z in (F.(k+1))"{+infty} by FUNCT_1:def 13; then not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} & not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} by XBOOLE_0:def 3; then not z in ((PF.k)"{+infty} /\ (F.(k+1))"{-infty}) \/ ((PF.k)"{-infty} /\ (F.(k+1))"{+infty}) by XBOOLE_0:def 2; then B5: z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{+infty} /\ (F.(k+1))"{-infty}) \/ ((PF.k)"{-infty} /\ (F.(k+1))"{+infty})) by B3,XBOOLE_0:def 4; B6: PF.(k+1) = PF.k + F.(k+1) by Def0; then z in dom(PF.(k+1)) by B5,MESFUNC1:def 3; then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by B6,MESFUNC1:def 3; hence (PF.(k+1)).z <> +infty by B4,SUPINF_2:8; end; for k being Nat holds P[k] from NAT_1:sch 2(A5,A6); hence contradiction by A2; end; hence ex m be Nat st m <= n & (F.m).z = +infty; 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) & ((Partial_Sums F).n).z = +infty and A3: m <= n; consider k be Nat such that A4: k <= n & (F.k).z = +infty by A2,Lem03; z in dom(F.k) & z in dom(F.m) by A2,A3,A4,Lem02; then z in dom(F.m) /\ dom(F.k) by XBOOLE_0:def 3; hence (F.m).z <> -infty by A4,A1,Def1a; end; theorem Lem05: 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 A2: z in dom(PF.n) & (PF.n).z = -infty; now assume A4:for m be Nat st m <= n holds (F.m).z <> -infty; defpred P[Nat] means $1 <= n implies (PF.$1).z <> -infty; PF.0 = F.0 by Def0; then A5: P[0] by A4; A6: for k being Nat st P[k] holds P[k + 1] proof let k be Nat; assume B1: P[k]; assume B2: k+1 <= n; then k <= n by NAT_1:13; then z in dom(PF.k) & z in dom(F.(k+1)) by A2,B2,Lem02; then B3: z in dom(PF.k) /\ dom(F.(k+1)) by XBOOLE_0:def 3; B4: (PF.k).z <> -infty & (F.(k+1)).z <> -infty by A4,B1,B2,NAT_1:13; then not( (PF.k).z in {-infty} ) & not( (F.(k+1)).z in {-infty} ) by TARSKI:def 1; then not z in (PF.k)"{-infty} & not z in (F.(k+1))"{-infty} by FUNCT_1:def 13; then not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} & not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} by XBOOLE_0:def 3; then not z in ((PF.k)"{-infty} /\ (F.(k+1))"{+infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty}) by XBOOLE_0:def 2; then B5: z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{-infty} /\ (F.(k+1))"{+infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty})) by B3,XBOOLE_0:def 4; B6: PF.(k+1) = PF.k + F.(k+1) by Def0; then z in dom(PF.(k+1)) by B5,MESFUNC1:def 3; then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by B6,MESFUNC1:def 3; hence (PF.(k+1)).z <> -infty by B4,SUPINF_2:9; end; for k being Nat holds P[k] from NAT_1:sch 2(A5,A6); hence contradiction by A2; end; hence ex m be Nat st m <= n & (F.m).z = -infty; 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 A2: z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = -infty; consider k be Nat such that A3: k <= n & (F.k).z = -infty by A2,Lem05; A4:z in dom(F.k) by A2,A3,Lem02; assume m <= n; then z in dom(F.m) by A2,Lem02; then z in dom(F.m) /\ dom(F.k) by A4,XBOOLE_0:def 3; hence (F.m).z <> +infty by A3,A1,Def1a; end; theorem Lem07b: F is additive implies ((Partial_Sums F).n)"{-infty} /\ (F.(n+1))"{+infty} = {} & ((Partial_Sums F).n)"{+infty} /\ (F.(n+1))"{-infty} = {} proof assume A1: F is additive; set PF = Partial_Sums F; now assume ex x be set st x in (PF.n)"{-infty} & x in (F.(n+1))"{+infty}; then consider z be set such that Z1: z in (PF.n)"{-infty} & z in (F.(n+1))"{+infty}; Z2: z in dom(PF.n) & (PF.n).z in {-infty} & z in dom(F.(n+1)) & (F.(n+1)).z in {+infty} by Z1,FUNCT_1:def 13; then Z6: (PF.n).z = -infty & (F.(n+1)).z = +infty by TARSKI:def 1; then consider k be Nat such that Z3: k <= n & (F.k).z = -infty by Z2,Lem05; z in dom(F.k) by Z2,Z3,Lem02; then z in dom(F.k) /\ dom(F.(n+1)) by Z2,XBOOLE_0:def 3; hence contradiction by A1,Def1a,Z3,Z6; 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 assume ex x be set st x in (PF.n)"{+infty} & x in (F.(n+1))"{-infty}; then consider z be set such that Z1: z in (PF.n)"{+infty} & z in (F.(n+1))"{-infty}; Z2: z in dom(PF.n) & (PF.n).z in {+infty} & z in dom(F.(n+1)) & (F.(n+1)).z in {-infty} by Z1,FUNCT_1:def 13; then Z6: (PF.n).z = +infty & (F.(n+1)).z = -infty by TARSKI:def 1; then consider k be Nat such that Z3: k <= n & (F.k).z = +infty by Z2,Lem03; z in dom(F.k) by Z2,Z3,Lem02; then z in dom(F.k) /\ dom(F.(n+1)) by Z2,XBOOLE_0:def 3; hence contradiction by A1,Def1a,Z3,Z6; 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; end; theorem Lem07: F is additive implies dom((Partial_Sums F).n) = meet{dom(F.k) where k is Element of NAT : k <= n} proof deffunc DOM(Nat) = {dom(F.k) where k is Element of NAT : k <= $1}; set PF = Partial_Sums F; assume A1: F is additive; defpred P[Nat] means dom(PF.$1) = meet {dom(F.k) where k is Element of NAT : k <= $1}; A2:dom(PF.0) = dom(F.0) by Def0; now let V be set; assume V in {dom(F.0)}; then V = dom(F.0) by TARSKI:def 1; hence V in DOM(0); end; then A3:{dom(F.0)} c= DOM(0) by TARSKI:def 3; now let V be set; assume V in DOM(0); then consider k be Element of NAT such that A4: V = dom(F.k) & k <= 0; k = 0 by A4; hence V in {dom(F.0)} by A4,TARSKI:def 1; end; then DOM(0) c= {dom(F.0)} by TARSKI:def 3; then DOM(0) = {dom(F.0)} by A3,XBOOLE_0:def 10; then P0:P[0] by A2,SETFAM_1:11; P1:for m be Nat st P[m] holds P[m+1] proof let m be Nat; assume L0: P[m]; L3: (PF.m)"{-infty} /\ (F.(m+1))"{+infty} = {} & (PF.m)"{+infty} /\ (F.(m+1))"{-infty} = {} by A1,Lem07b; PF.(m+1) = PF.m + F.(m+1) by Def0; then L5: dom(PF.(m+1)) = (dom(PF.m)/\dom(F.(m+1))) \ ({}\/{}) by L3,MESFUNC1:def 3; L41:dom(F.0) in DOM(m+1) & dom(F.0) in DOM(m); now let V be set; assume L40:V in meet DOM(m+1); dom(F.(m+1)) in DOM(m+1); then L43: V in dom(F.(m+1)) by L40,SETFAM_1:def 1; now let V be set; assume V in DOM(m); then consider i be Element of NAT such that L44: V = dom(F.i) & i <= m; i <= m+1 by L44,NAT_1:12; hence V in DOM(m+1) by L44; end; then DOM(m) c= DOM(m+1) by TARSKI:def 3; then meet DOM(m+1) c= meet DOM(m) by L41,SETFAM_1:7; hence V in meet DOM(m) /\ dom(F.(m+1)) by L40,L43,XBOOLE_0:def 3; end; then L45:meet DOM(m+1) c= meet DOM(m) /\ dom(F.(m+1)) by TARSKI:def 3; now let V be set; assume V in meet DOM(m) /\ dom(F.(m+1)); then L46: V in meet DOM(m) & V in dom(F.(m+1)) by XBOOLE_0:def 3; for W be set holds W in DOM(m+1) implies V in W proof let W be set; assume W in DOM(m+1); then consider i be Element of NAT such that L48: W = dom(F.i) & i <= m+1; now assume i <= m; then W in DOM(m) by L48; hence V in W by L46,SETFAM_1:def 1; end; hence thesis by L48,NAT_1:8,L46; end; hence V in meet DOM(m+1) by L41,SETFAM_1:def 1; end; then meet DOM(m) /\ dom(F.(m+1)) c= meet DOM(m+1) by TARSKI:def 3; hence thesis by L0,L5,L45,XBOOLE_0:def 10; end; for k be Nat holds P[k] from NAT_1:sch 2(P0,P1); hence thesis; end; theorem ADD0: F is additive & F is with_the_same_dom implies dom((Partial_Sums F).n) = dom(F.0) proof assume A0: F is additive & F is with_the_same_dom; now let D be set; assume B1: D in meet {dom(F.k) where k is Element of NAT : k <= n}; dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n}; then D in dom(F.0) by B1,SETFAM_1:def 1; hence D in meet {dom(F.0)} by SETFAM_1:11; end; then B2:meet{dom(F.k) where k is Element of NAT : k <= n} c= meet{dom(F.0)} by TARSKI:def 3; now let D be set; assume D in meet {dom(F.0)}; then B5: D in dom(F.0) by SETFAM_1:11; B3: dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n}; 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 B5,A0,MESFUNC8:def 2; end; hence D in meet {dom(F.k) where k is Element of NAT : k <= n} by B3,SETFAM_1:def 1; end; then meet{dom(F.0)} c= meet {dom(F.k) where k is Element of NAT : k <= n} by TARSKI:def 3; then meet{dom(F.k) where k is Element of NAT : k <= n} = meet {dom(F.0)} by B2,XBOOLE_0:def 10; then dom((Partial_Sums F).n) = meet{dom(F.0)} by A0,Lem07; hence thesis by SETFAM_1:11; end; theorem LIM4: (for n be Nat holds F.n is nonnegative) implies F is additive proof assume A1: for n be Nat holds F.n is nonnegative; let n,m be Nat; assume n <> m; F.n is nonnegative & F.m is nonnegative by A1; hence for x be set st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or (F.m).x <> -infty by SUPINF_2:70; end; theorem Lem09: 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; assume n <> m; let x be set; assume A4: x in dom(G.n) /\ dom(G.m); A5:G.n = (F.n)|D & G.m = (F.m)|D by A2; then dom(G.n) c= dom(F.n) & dom(G.m) c= dom(F.m) by RELAT_1:89; then dom(G.n) /\ dom(G.m) c= dom(F.n) /\ dom(F.m) by XBOOLE_1:27; then A6:(F.n).x <> +infty or (F.m).x <> -infty by A1,A4,Def1a; x in dom(G.n) & x in dom(G.m) by A4,XBOOLE_0:def 3; hence (G.n).x <> +infty or (G.m).x <> -infty by A6,A5,FUNCT_1:70; end; theorem Cor00: 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 AS1: F is additive & F is with_the_same_dom & D c= dom(F.0) and AS2: x in D; defpred P[Nat] means PFx.$1 = (PF#x).$1; PFx.0 = (F#x).0 by Def1; then PFx.0 = (F.0).x by MESFUNC5:def 13; then PFx.0 = (PF.0).x by Def0; then A1:P[0] by MESFUNC5:def 13; A2:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; A4: PF.(k+1) = PF.k + F.(k+1) by Def0; A5: D c= dom(PF.(k+1)) by AS1,ADD0; PFx.(k+1) = PFx.k + (F#x).(k+1) by Def1; then PFx.(k+1) = (PF#x).k + (F.(k+1)).x by A3,MESFUNC5:def 13; then PFx.(k+1) = (PF.k).x + (F.(k+1)).x by MESFUNC5:def 13; then PFx.(k+1) = (PF.(k+1)).x by AS2,A4,A5,MESFUNC1:def 3; hence thesis by MESFUNC5:def 13; end; for k being Nat holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Cor01: 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 &D c= dom(F.0) and A3: x in D; thus P1:now assume PFx is convergent_to_finite_number; then consider g be real number such that A4: for p be real number st 0

m; F.n is_simple_func_in S & F.m is_simple_func_in S by A1; then F.n is without+infty & F.m is without+infty by MESFUNC5:20; hence for x be set st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or (F.m).x <> -infty by MESFUNC5:def 6; end; defpred P[Nat] means (Partial_Sums F).$1 is_simple_func_in S; (Partial_Sums F).0 = F.0 by Def0; then A2:P[0] by A1; A3:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: 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 A4,MESFUNC5:44; hence P[k+1] by Def0; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); hence (Partial_Sums F).n is_simple_func_in S; end; theorem ADD3C: (for m be Nat holds F.m is nonnegative) implies (Partial_Sums F).n is nonnegative proof assume A1: for m be Nat holds F.m is nonnegative; defpred P[Nat] means (Partial_Sums F).$1 is nonnegative; (Partial_Sums F).0 = F.0 by Def0; then B1:P[0] by A1; B2:now let k be Nat; assume P[k]; then B01:(Partial_Sums F).k is nonnegative & F.(k+1) is nonnegative by A1; (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def0; hence P[k+1] by B01,MESFUNC5:28; end; for k being Nat holds P[k] from NAT_1:sch 2(B1,B2); hence thesis; end; theorem ADD3D: 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 A0: F is with_the_same_dom; assume A81: x in dom(F.0); assume A1: for m be Nat holds F.m is nonnegative; assume C1: n <= m; A2:F is additive by A1,LIM4; set PF = Partial_Sums F; defpred P[Nat] means (PF.n).x <= (PF.$1).x; Q1:for k be Nat holds (PF.k).x <= (PF.(k+1)).x proof let k be Nat; Q11:PF.(k+1) = PF.k + F.(k+1) by Def0; dom(PF.(k+1)) = dom(F.0) by A0,A2,ADD0; then Q12:(PF.(k+1)).x = (PF.k).x + (F.(k+1)).x by A81,Q11,MESFUNC1:def 3; F.(k+1) is nonnegative & PF.k is nonnegative by A1,ADD3C; then 0. <= (F.(k+1)).x & 0. <= (PF.k).x by SUPINF_2:58; hence thesis by Q12,SUPINF_2:20; end; Q2: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 Q21: k >= n & for l be Nat st l >= n & l < k holds P[l]; now assume k > n; then k >= n + 1 by NAT_1:13; then Q22: k = n+1 or k > n+1 by REAL_1:def 5; now assume Q23: k > n+1; then reconsider l = k-1 as Element of NAT by NAT_1:20; k < k+1 by NAT_1:13; then k > l & l >= n by Q23,XREAL_1:21; then Q24: (PF.n).x <= (PF.l).x by Q21; k = l+1; then (PF.l).x <= (PF.k).x by Q1; hence P[k] by Q24,XXREAL_0:2; end; hence P[k] by Q22,Q1; end; hence thesis by Q21,REAL_1:def 5; end; for k being Nat st k >= n holds P[k] from NAT_1:sch 9(Q2); hence thesis by C1; end; theorem ADD3: 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 A0: F is with_the_same_dom; assume A81: x in dom(F.0); assume A1: for m be Nat holds F.m is nonnegative; for n,m be Element of NAT st m<=n holds ((Partial_Sums F)#x).m <= ((Partial_Sums F)#x).n proof let n,m be Element of NAT; assume m <= n; then ((Partial_Sums F).m).x <= ((Partial_Sums F).n).x by A0,A1,A81,ADD3D; then ((Partial_Sums F)#x).m <= ((Partial_Sums F).n).x by MESFUNC5:def 13; hence ((Partial_Sums F)#x).m <= ((Partial_Sums F)#x).n by MESFUNC5:def 13; end; hence ((Partial_Sums F)#x) is non-decreasing by RINFSUP2:7; hence ((Partial_Sums F)#x) is convergent by RINFSUP2:37; end; theorem ADD1e: (for m be Nat holds F.m is without-infty) implies (Partial_Sums F).n is without-infty proof assume P1: for m be Nat holds F.m is without-infty; defpred P[Nat] means (Partial_Sums F).$1 is without-infty; (Partial_Sums F).0 = F.0 by Def0; then B1:P[0] by P1; B2:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume B01: P[k]; B02:(Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def0; F.(k+1) is without-infty by P1; hence thesis by B02,B01,ADD1a; end; for k being Nat holds P[k] from NAT_1:sch 2(B1,B2); hence thesis; end; theorem (for m be Nat holds F.m is without+infty) implies (Partial_Sums F).n is without+infty proof assume P1: for m be Nat holds F.m is without+infty; defpred P[Nat] means (Partial_Sums F).$1 is without+infty; (Partial_Sums F).0 = F.0 by Def0; then B1:P[0] by P1; B2:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume B01: P[k]; B02:(Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def0; F.(k+1) is without+infty by P1; hence thesis by B02,B01,ADD1b; end; for k being Nat holds P[k] from NAT_1:sch 2(B1,B2); hence thesis; end; theorem ADD1: (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; PF.0 = F.0 by Def0; then C1:P[0] by A1; C2:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then C03:PF.k is_measurable_on E & PF.k is without-infty by A1,ADD1e; F.(k+1) is_measurable_on E & F.(k+1) is without-infty by A1; then PF.k + F.(k+1) is_measurable_on E by C03,MESFUNC5:37; hence thesis by Def0; end; for k being Nat holds P[k] from NAT_1:sch 2(C1,C2); hence (Partial_Sums F).m is_measurable_on E; end; theorem ADD4: 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 A6: x in dom(F.0) /\ dom(G.0) and A5: (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 PF = Partial_Sums F; set PG = Partial_Sums G; defpred P[Nat] means (PF.$1).x <= (PG.$1).x; (PF.0) = F.0 & (PG.0) = G.0 by Def0; then B1:P[0] by A5,A6; B2:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume B20: P[k]; R1: (F.(k+1)).x <= (G.(k+1)).x by A5,A6; B22:PF.(k+1) = PF.k + F.(k+1) & PG.(k+1) = PG.k + G.(k+1) by Def0; dom(PF.(k+1)) = dom(F.0) & dom(PG.(k+1)) = dom(G.0) by A1,A2,A3,A4,ADD0; then x in dom(PF.(k+1)) & x in dom(PG.(k+1)) by A6,XBOOLE_0:def 3; then B25:(PF.(k+1)).x = (PF.k).x + (F.(k+1)).x & (PG.(k+1)).x = (PG.k).x + (G.(k+1)).x by B22,MESFUNC1:def 3; thus thesis by B25,R1,B20,SUPINF_2:14; end; for k being Nat holds P[k] from NAT_1:sch 2(B1,B2); hence thesis; end; theorem ADD5: 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,ADD0; hence dom((Partial_Sums F).n) = dom((Partial_Sums F).m) by A1,A2,ADD0; end; theorem ADD2: 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 A4: F is additive and A5: F is with_the_same_dom and A2: for n be Nat holds (Partial_Sums F).n is_measurable_on E and A3: for x be Element of X st x in E holds F#x is summable; P1:dom((Partial_Sums F).0) = E by ADD0,A1,A4,A5; reconsider PF = Partial_Sums F as with_the_same_dom Functional_Sequence of X,ExtREAL by A4,A5,ADD5; now let x be Element of X; assume Q1: x in E; then F#x is summable by A3; then Partial_Sums(F#x) is convergent by Def2; hence PF#x is convergent by A1,A4,A5,Q1,Cor01; end; hence thesis by P1,A2,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 assume A2: for n be Nat holds F.n is_integrable_on M; set PF = Partial_Sums F; defpred P1[Nat] means PF.$1 is_integrable_on M; PF.0 = F.0 by Def0; then A3:P1[0] by A2; A4:for k be Nat st P1[k] holds P1[k+1] proof let k be Nat; assume P1[k]; then PF.k is_integrable_on M & F.(k+1) is_integrable_on M by A2; then PF.k + F.(k+1) is_integrable_on M by MESFUNC5:114; hence P1[k+1] by Def0; end; thus for m be Nat holds P1[m] from NAT_1:sch 2(A3,A4); end; theorem FSUM3: 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 A4: F is additive and A5: F is with_the_same_dom and A2: for n be Nat holds F.n is_measurable_on E & F.n is nonnegative & I.n = Integral(M,F.n); G3:for n be Nat holds F.n is without-infty by A2,MESFUNC5:18; set PF = Partial_Sums F; thus Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m proof defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1; set PI = Partial_Sums I; Integral(M,PF.0) = Integral(M,F.0) by Def0; then Integral(M,PF.0) = I.0 by A2; then A8: P2[0] by Def1; B1: for k be Nat st P2[k] holds P2[k+1] proof let k be Nat; assume B2: P2[k]; A12: dom(PF.k) = E & dom(F.(k+1)) = E by A1,A4,A5,ADD0,MESFUNC8:def 2; A9: PF.k is_measurable_on E & F.(k+1) is_measurable_on E & PF.k is nonnegative & F.(k+1) is nonnegative by A2,G3,ADD1,ADD3C; then consider D be Element of S such that A11: D = dom(PF.k + F.(k+1)) & integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A12,MESFUNC5:84; D = E /\ E by A12,A9,A11,MESFUNC5:28; then A14: (PF.k)|D = PF.k & (F.(k+1))|D = F.(k+1) by A12,RELAT_1:97; dom(PF.(k+1)) = E & PF.(k+1) is_measurable_on E & PF.(k+1) is nonnegative by A1,G3,A2,A4,A5,ADD1,ADD3C,ADD0; then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by MESFUNC5:94 .= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A11,Def0 .= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A9,A12,A14,MESFUNC5:94 .= Integral(M,PF.k) + Integral(M,F.(k+1)) by A9,A12,A14,MESFUNC5:94 .= PI.k + I.(k+1) by A2,B2; hence PI.(k+1) = Integral(M,PF.(k+1)) by Def1; end; for k be Nat holds P2[k] from NAT_1:sch 2(A8,B1); hence Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m; end; end; begin :: Sequence of Measurable Functions Cor131a: 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 A0: E c= dom f and B2: f is_measurable_on E and A1: E ={} and A2: for n be Nat holds F.n is_simple_func_in S; deffunc I(Element of NAT) = 0.; consider I be ExtREAL_sequence such that A3: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4; take I; A5:M.E = 0 by A1,MEASURE1:def 11; 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 13; reconsider D = dom(F.m) as Element of S by A2,MESFUNC5:43; F.m is_measurable_on D by A2,MESFUNC2:37; then Integral(M,(F.m)|E) = 0 by A5,MESFUNC5:100; hence thesis by A3; end; defpred P[Element of NAT] means (Partial_Sums I).$1 = 0; (Partial_Sums I).0 = I.0 by Def1; then P1:P[0] by A3; P2:for k be Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT; assume P21: P[k]; P22:I.(k+1) = 0 by A3; (Partial_Sums I).(k+1) = (Partial_Sums I).k + I.(k+1) by Def1; then (Partial_Sums I).(k+1) = 0 + 0 by P21,P22,SUPINF_2:1; hence thesis; end; P3:for k being Element of NAT holds P[k] from NAT_1:sch 1(P1,P2); for n be Nat holds (Partial_Sums I).n = 0 proof let n be Nat; n is Element of NAT by ORDINAL1:def 13; hence thesis by P3; end; then A6:Partial_Sums I is convergent_to_finite_number & lim(Partial_Sums I) = 0 by MESFUNC5:58; then Partial_Sums I is convergent by MESFUNC5:def 11; hence I is summable by Def2; A7:E = dom(f|E) by A0,RELAT_1:91; then E = dom f /\ E by FUNCT_1:68; then Integral(M,(f|E)|E) = 0 by A7,A5,B2,MESFUNC5:48,100; hence Integral(M,f|E) = Sum I by A6,FUNCT_1:82; end; Cor131b: 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 & F is additive and NE: E common_on_dom F and A4: for n be Nat holds F.n is_simple_func_in S & F.n is nonnegative and A5: for x be Element of X st x in E holds F#x is summable & f.x = Sum(F#x); B1:dom(f|E) = E by A1,RELAT_1:91; P0: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 n'=n as Element of NAT by ORDINAL1:def 13; P01:F.n is_simple_func_in S & F.n is nonnegative & E c= dom(F.n') by A4,NE,SEQFUNC:def 10; hence (F.n)|E is_simple_func_in S by MESFUNC5:40; thus (F.n)|E is nonnegative by P01,MESFUNC5:21; thus dom((F.n)|E) = E by P01,RELAT_1:91; end; deffunc G1(Nat) = (F.$1)|E; consider g1 be Functional_Sequence of X,ExtREAL such that G1: for n be Nat holds g1.n = G1(n) from SEQFUNC:sch 1; set G = Partial_Sums g1; deffunc I(Element of NAT) = Integral(M,g1.$1); consider I be ExtREAL_sequence such that A6: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4; take I; G2: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 13; I.m = Integral(M,g1.m) by A6; hence thesis by G1; end; G.0 = g1.0 by Def0; then P10:G.0 = (F.0)|E by G1; for n,m be Nat holds dom(g1.n) = dom(g1.m) proof let n,m be Nat; R12:dom(g1.n) = dom((F.n)|E) by G1; dom(g1.m) = dom((F.m)|E) by G1; then dom(g1.m) = E by P0; hence dom(g1.n) = dom(g1.m) by P0,R12; end; then XX:g1 is with_the_same_dom by MESFUNC8:def 2; T1:for k be Nat holds g1.k is nonnegative proof let k be Nat; (F.k)|E is nonnegative by P0; hence g1.k is nonnegative by G1; end; R1: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; R10: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 P0; hence thesis by G1; end; hence G.n is_simple_func_in S by Lem10; thus G.n is nonnegative by T1,ADD3C; R11:g1 is additive by R10,Lem10; dom(g1.0) = dom((F.0)|E) by G1; then dom(g1.0) = E by P0; hence dom(G.n) = E by R11,XX,ADD0; end; set L = Partial_Sums I; L3:for n be Nat holds integral'(M,G.n) = L.n proof let n be Nat; reconsider m = n as Element of NAT by ORDINAL1:def 13; defpred L[Element of NAT] means L.$1 = integral'(M,G.$1); L.0 = I.0 by Def1; then L31:L.0 = Integral(M,G.0) by P10,G2; G.0 is_simple_func_in S & G.0 is nonnegative by R1; then L32:L[0] by L31,MESFUNC5:95; L33:for k be Element of NAT st L[k] holds L[k+1] proof let k be Element of NAT; assume L4: L[k]; G.(k+1) = G.k + g1.(k+1) by Def0; then P15: G.(k+1) = G.k + (F.(k+1))|E by G1; L.(k+1) = (Partial_Sums I).k + I.(k+1) by Def1; then L5: L.(k+1) = integral'(M,G.k) + Integral(M,(F.(k+1))|E) by G2,L4; L7: (F.(k+1))|E is_simple_func_in S & (F.(k+1))|E is nonnegative by P0; L8: G.k is_simple_func_in S & G.k is nonnegative & G.(k+1) is_simple_func_in S & G.(k+1) is nonnegative by R1; L9: dom(G.k) = E & dom((F.(k+1))|E) = E by P0,R1; then E = dom(G.k) /\ dom((F.(k+1))|E); then dom( G.k + (F.(k+1))|E ) = E by L7,L8,MESFUNC5:71; then L10: integral'(M,G.k + (F.(k+1))|E) = integral'(M,(G.k)|E) + integral'(M,((F.(k+1))|E)|E) by L7,L8,MESFUNC5:71; (G.k)|E = G.k & ((F.(k+1))|E)|E = (F.(k+1))|E by L9,RELAT_1:97; hence thesis by P15,L7,L10,L5,MESFUNC5:95; end; L34:for k be Element of NAT holds L[k] from NAT_1:sch 1(L32,L33); n is Element of NAT by ORDINAL1:def 13; hence thesis by L34; end; C1: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 C11: x in dom(f|E); then C12:F#x is summable & f.x = Sum(F#x) by A5,B1; C14:f.x = (f|E).x by C11,FUNCT_1:70; for n be set st n in NAT holds (F#x).n = (g1#x).n proof let n be set; assume n in NAT; then reconsider n1 = n as Nat; C16: (F.n1)|E = g1.n1 by G1; dom((F.n1)|E) = E by P0; then C13: (g1.n1).x = (F.n1).x by C11,C16,B1,FUNCT_1:70; (F#x).n = (F.n1).x by MESFUNC5:def 13; hence thesis by C13,MESFUNC5:def 13; end; hence thesis by C12,C14,FUNCT_2:18; end; X0:g1 is additive by A3,G1,Lem09; g1.0 = (F.0)|E by G1; then Y1:dom(g1.0) = E by P0; dom f /\ E = E by B1,FUNCT_1:68; then A7:f|E is_measurable_on E & f|E is nonnegative by A2,A3,MESFUNC5:21,48; then consider F be Functional_Sequence of X,ExtREAL, K be ExtREAL_sequence such that A8: (for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom(f|E)) & (for n be Nat holds F.n is nonnegative) & (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 ) & (for x be Element of X st x in dom(f|E) holds F#x is convergent & lim(F#x) = (f|E).x) & (for n be Nat holds K.n=integral'(M,F.n)) & K is convergent & integral+(M,(f|E))=lim K by B1,MESFUNC5:def 15; R2: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 XX,T1,Y1,ADD3D; 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 R31: x in E; hence F#x is convergent by B1,A8; g1#x is summable by R31,B1,C1; then Partial_Sums(g1#x) is convergent by Def2; hence G#x is convergent by R31,Y1,X0,XX,Cor01; g1#x is summable & (f|E).x = Sum(g1#x) by R31,B1,C1; then lim(G#x) = (f|E).x by B1,R31,Y1,X0,XX,Cor02; hence lim(F#x) = lim(G#x) by B1,A8,R31; end; then L is convergent & lim L = integral+(M,(f|E)) by R1,R2,B1,A8,L3,MESFUNC5:82; hence thesis by A7,B1,G2,Def2,MESFUNC5:94; 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 & 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)); per cases; suppose E = {}; hence thesis by A1,Cor131a; end; suppose A2: E <> {}; for n be Element of NAT holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom(F.n) by A1; then E common_on_dom F by A2,SEQFUNC:def 10; hence thesis by A1,Cor131b; 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; R1:dom F = E by A1,RELAT_1:91; E = dom f /\ E by A1,XBOOLE_1:28; then F is_measurable_on E & F is nonnegative by A2,A3,MESFUNC5:48,21; then consider h be Functional_Sequence of X,ExtREAL such that A4: (for n be Nat holds h.n is_simple_func_in S & dom(h.n) = dom F) & (for n be Nat holds h.n is nonnegative) & (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 ) & (for x be Element of X st x in dom F holds (h#x) is convergent & lim(h#x) = F.x) by R1,MESFUNC5:70; defpred P[Element of NAT,set,set] means $3 = h.($1+1) - h.$1; K1:for n being Element of NAT for x being set ex y being set st P[n,x,y]; K2:for n being Element of NAT for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1=y2; consider g being Function such that K3: dom g = NAT & g.0 = h.0 & for n being Element of NAT holds P[n,g.n,g.(n+1)] from RECDEF_1:sch 1(K1,K2); now let f be set; assume f in rng g; then consider m be set such that K41: m in dom g & f = g.m by FUNCT_1:def 5; reconsider m as Element of NAT by K41,K3; defpred IND[Element of NAT] means g.$1 is PartFunc of X,ExtREAL; K42:IND[0] by K3; K43:for n be Element of NAT st IND[n] holds IND[n+1] proof let n be Element of NAT; assume IND[n]; then reconsider F2 = g.n as PartFunc of X,ExtREAL; g.(n+1) = h.(n+1) - h.n by K3; hence IND[n+1]; end; for n be Element of NAT holds IND[n] from NAT_1:sch 1(K42,K43); then g.m is PartFunc of X,ExtREAL; hence f in PFuncs(X,ExtREAL) by K41,PARTFUN1:119; end; then rng g c= PFuncs(X,ExtREAL) by TARSKI:def 3; then reconsider g as Functional_Sequence of X,ExtREAL by K3,SEQFUNC:def 1; take g; Q1: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 Q01: n = 0; hence g.n is_simple_func_in S & g.n is nonnegative by A4,K3; hence g.n is_measurable_on E by MESFUNC2:37; thus E c= dom(g.n) by R1,Q01,K3,A4; end; suppose n <> 0; then consider m be Nat such that P2: n = m+1 by NAT_1:6; reconsider m as Element of NAT by ORDINAL1:def 13; P5: g.n = h.n - h.m by K3,P2; then P3: g.n = h.n + (-(h.m)) by MESFUNC2:9; P4: h.n is_simple_func_in S & h.m is_simple_func_in S by A4; then (-1)(#)(h.m) is_simple_func_in S by MESFUNC5:45; then P11: -(h.m) is_simple_func_in S by MESFUNC2:11; hence g.n is_simple_func_in S by P3,P4,MESFUNC5:44; h.n is without-infty & h.m is without+infty by P4,MESFUNC5:20; then P7: dom(h.n - h.m) = dom(h.n) /\ dom(h.m) by MESFUNC5:23; P10: dom(h.n) = dom F & dom(h.m) = dom F by A4; now let x be set; assume P9: x in dom(h.n - h.m); m <= m+1 by NAT_1:11; hence (h.m).x <= (h.n).x by P9,P10,P7,A4,P2; end; hence g.n is nonnegative by P4,P5,MESFUNC5:46; thus g.n is_measurable_on E by P11,P3,P4,MESFUNC5:44,MESFUNC2:37; thus E c= dom(g.n) by R1,K3,P2,P10,P7; end; end; hence Q2:g is additive by Lem10; thus for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n is_measurable_on E by Q1; Q3:now let x be Element of X; assume L0: x in E; then L1: (h#x) is convergent & lim(h#x) = F.x by A4,R1; L5: for m be Nat holds (Partial_Sums(g#x)).m = (h#x).m proof let m be Nat; defpred P[Nat] means (Partial_Sums(g#x)).$1 = (h#x).$1; (Partial_Sums(g#x)).0 = (g#x).0 by Def1; then (Partial_Sums(g#x)).0 = (g.0).x by MESFUNC5:def 13; then B1: P[0] by K3,MESFUNC5:def 13; B2: for k be Nat st P[k] holds P[k+1] proof let k be Nat; set Pgx = Partial_Sums(g#x); assume P[k]; then B3: Pgx.k = (h.k).x by MESFUNC5:def 13; h.(k+1) is_simple_func_in S & h.k is_simple_func_in S by A4; then B4: (h.(k+1) is without+infty & h.(k+1) is without-infty) & (h.k is without+infty & h.k is without-infty) by MESFUNC5:20; B5: dom(h.(k+1)) = dom F & dom(h.k) = dom F by A4; then C0: ( -infty < (h.(k+1)).x & (h.(k+1)).x < +infty ) & ( -infty < (h.k).x & (h.k).x < +infty) by L0,R1,B4,MESFUNC5:16,17; reconsider k as Element of NAT by ORDINAL1:def 13; B6: g.(k+1) = h.(k+1) - h.k by K3; B7: dom(h.(k+1) - h.k) = dom(h.(k+1)) /\ dom(h.k) by B4,MESFUNC5:23; Pgx.(k+1) = Pgx.k + ((g#x).(k+1)) by Def1; then B9: Pgx.(k+1) = (h.k).x + (g.(k+1)).x by B3,MESFUNC5:def 13; reconsider hk1x=(h.(k+1)).x as Real by C0,EXTREAL1:1; reconsider hkx=(h.k).x as Real by C0,EXTREAL1:1; (h.(k+1)).x - (h.k).x = hk1x - hkx by SUPINF_2:5; then D2: (h.(k+1)).x - (h.k).x + (h.k).x = hk1x - hkx + hkx by SUPINF_2:1; (g.(k+1)).x = (h.(k+1)).x - (h.k).x by B6,B7,L0,R1,B5,MESFUNC1:def 4; hence thesis by B9,D2,MESFUNC5:def 13; end; for k being Nat holds P[k] from NAT_1:sch 2(B1,B2); hence thesis; end; per cases by L1,MESFUNC5:def 11; suppose h#x is convergent_to_finite_number; then not h#x is convergent_to_+infty & not h#x is convergent_to_-infty by MESFUNC5:56,57; then consider s be real number such that L3: lim(h#x) = s & (for p be real number st 0 < p ex N be Nat st for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p) & h#x is convergent_to_finite_number by L1,MESFUNC5:def 12; for p be real number st 0 < p ex N be Nat st for m be Nat st N <= m holds |. (Partial_Sums(g#x)).m - R_EAL s .| < p proof let p be real number; assume 0 < p; then consider N be Nat such that L4: for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by L3; take N; let m be Nat; assume N <= m; then |. (h#x).m - lim(h#x) .| < p by L4; hence |. (Partial_Sums(g#x)).m - R_EAL s .| < p by L5,L3; end; then L7: Partial_Sums(g#x) is convergent_to_finite_number by MESFUNC5:def 8; then L8: Partial_Sums(g#x) is convergent by MESFUNC5:def 11; hence g#x is summable by Def2; for p be real number 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 number; assume 0 < p; then consider N be Nat such that S1: for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by L3; take N; let m be Nat; assume N <= m; then |. (h#x).m - lim(h#x) .| < p by S1; hence |. (Partial_Sums(g#x)).m - lim(h#x) .| < p by L5; end; then lim Partial_Sums(g#x) = lim(h#x) by L3,L7,L8,MESFUNC5:def 12; hence Sum(g#x) = f.x by L0,L1,FUNCT_1:72; end; suppose T1: (h#x) is convergent_to_+infty; for p be real number 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 number; assume 0 < p; then consider N be Nat such that T3: for m be Nat st N<=m holds p <= (h#x).m by T1,MESFUNC5:def 9; take N; let m be Nat; assume N <= m; then p <= (h#x).m by T3; hence p <= (Partial_Sums(g#x)).m by L5; end; then T4: Partial_Sums(g#x) is convergent_to_+infty by MESFUNC5:def 9; then T5: Partial_Sums(g#x) is convergent by MESFUNC5:def 11; hence g#x is summable by Def2; T6: lim(h#x) = +infty by T1,L1,MESFUNC5:def 12; lim Partial_Sums(g#x) = +infty by T4,T5,MESFUNC5:def 12; hence Sum(g#x) = f.x by L0,L1,T6,FUNCT_1:72; end; suppose U1: (h#x) is convergent_to_-infty; for p be real number 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 number; assume p < 0; then consider N be Nat such that U3: for m be Nat st N<=m holds (h#x).m <= p by U1,MESFUNC5:def 10; take N; let m be Nat; assume N <= m; then (h#x).m <= p by U3; hence (Partial_Sums(g#x)).m <= p by L5; end; then U4: Partial_Sums(g#x) is convergent_to_-infty by MESFUNC5:def 10; then U5: Partial_Sums(g#x) is convergent by MESFUNC5:def 11; hence g#x is summable by Def2; U6: lim(h#x) = -infty by U1,L1,MESFUNC5:def 12; lim Partial_Sums(g#x) = -infty by U4,U5,MESFUNC5:def 12; hence Sum(g#x) = f.x by L0,L1,U6,FUNCT_1:72; 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 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 by A1,A3,Q1,Cor131a; end; suppose V1: E <> {}; for m be Element of 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 Q1; then E common_on_dom g by V1,SEQFUNC:def 10; hence 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 by A1,A2,A3,Q1,Q2,Q3,Cor131b; end; end; registration let X be non empty set; cluster additive with_the_same_dom 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:> & F.m = <:{},X,ExtREAL:> by A1; hence dom(F.n) = dom(F.m); end; then reconsider F as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2; A3:now let n,m be Nat; A2: F.n = <:{},X,ExtREAL:> by A1; assume n <> m; let x be set; assume x in dom(F.n) /\ dom(F.m); then x in dom {} /\ dom(F.m) by A2,PARTFUN1:91; hence (F.n).x <> +infty or (F.m).x <> -infty; end; take F; thus thesis by A3,Def1a; 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:121; 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 set; assume A2: d in D; then A3: IT.d = F.(c,d) by A1; [c,d] in [:C,D:] by A2,ZFMISC_1:106; hence IT.d in X by A3,FUNCT_2:7; end; then reconsider IT as Function of D,X by A1,FUNCT_2:5; take IT; let d be Element of D; thus IT.d = F.(c,d) by A1; end; uniqueness proof let P1,P2 be Function of D,X; assume that A1: for d be Element of D holds P1.d = F.(c,d) and A2: for d be Element of D holds P2.d = F.(c,d); now let d be set; assume d in D; then reconsider d1 = d as Element of D; P1.d1 = F.(c,d1) & P2.d1 = F.(c,d1) by A1,A2; hence P1.d = P2.d; end; hence thesis by FUNCT_2:18; 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 set; assume A2: c in C; then A3: IT.c = F.(c,d) by A1 .= F.[c,d]; [c,d] in [:C,D:] by A2,ZFMISC_1:106; hence IT.c in X by A3,FUNCT_2:7; end; then reconsider IT as Function of C,X by A1,FUNCT_2:5; take IT; let c be Element of C; thus IT.c = F.(c,d) by A1; end; uniqueness proof let P1,P2 be Function of C,X; assume that A1: for c be Element of C holds P1.c = F.(c,d) and A2: for c be Element of C holds P2.c = F.(c,d); now let c be set; assume c in C; then reconsider c1 = c as Element of C; P1.c1 = F.(c1,d) & P2.c1 = F.(c1,d) by A1,A2; hence P1.c = P2.c; end; hence thesis by FUNCT_2:18; 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 :defproj1: 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 let y be set; assume y in rng IT; then consider k be set such that A2: k in dom IT & y = IT.k by FUNCT_1:def 5; reconsider k as Element of NAT by A1,A2; reconsider n1=n as Element of NAT by ORDINAL1:def 13; y = F.(n1,k) by A1,A2; hence y in PFuncs(X,Y); end; then rng IT c= PFuncs(X,Y) by TARSKI:def 3; then reconsider IT as Functional_Sequence of X,Y by A1,SEQFUNC:def 1; 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 13; IT.m = F.(n1,m1) by A1; hence thesis; end; end; uniqueness proof let G1,G2 be Functional_Sequence of X,Y; assume that A1: for m be Nat holds G1.m = F.(n,m) and A2: 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 A1; hence G1.m = G2.m by A2; end; hence thesis by SEQFUNC:2; end; func ProjMap2(F,n) -> Functional_Sequence of X,Y means :defproj2: 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 A1: dom IT = NAT & for m be Element of NAT holds IT.m = P2(m) from FUNCT_1:sch 4; now let y be set; assume y in rng IT; then consider k be set such that A2: k in dom IT & y = IT.k by FUNCT_1:def 5; reconsider k as Element of NAT by A1,A2; reconsider n1=n as Element of NAT by ORDINAL1:def 13; y = F.(k,n1) by A1,A2; hence y in PFuncs(X,Y); end; then rng IT c= PFuncs(X,Y) by TARSKI:def 3; then reconsider IT as Functional_Sequence of X,Y by A1,SEQFUNC:def 1; 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 13; IT.m = F.(m1,n1) by A1; hence thesis; end; end; uniqueness proof let G1,G2 be Functional_Sequence of X,Y; assume that A1: for m be Nat holds G1.m = F.(m,n) and A2: 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 A1; hence G1.m = G2.m by A2; end; hence thesis by SEQFUNC:2; end; end; definition let X be non empty set, F be Function of NAT,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 SEQFUNC:def 1; end; end; theorem Th131z: 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 Function of NAT,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 A3: F is with_the_same_dom and A2: for n be Nat holds F.n is nonnegative & F.n is_measurable_on E; X1: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; E = dom(F.n) & F.n is_measurable_on E & F.n is nonnegative by A1,A2,A3,MESFUNC8:def 2; hence thesis by MESFUNC5:70; end; 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); X2: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 X21: (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) by X1; reconsider G as Element of Funcs(NAT,PFuncs(X,ExtREAL)) by FUNCT_2:11; take G; thus thesis by X21; end; consider FF be Function of NAT,Funcs(NAT,PFuncs(X,ExtREAL)) such that XX: for n be Element of NAT holds Q[n,FF.n] from FUNCT_2:sch 3(X2); 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 13; 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 XX; hence thesis; end; end; theorem FSUM2: 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 A3: F is additive and A4: F is with_the_same_dom and A2: for n be Nat holds F.n is_measurable_on E & F.n is nonnegative; G3:for n be Nat holds F.n is without-infty by A2,MESFUNC5:18; deffunc I(Element of NAT) = Integral(M,F.$1); consider I be Function of NAT,ExtREAL such that A6: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4; reconsider I as ExtREAL_sequence; take I; set PF = Partial_Sums F; thus for n be Nat holds I.n = Integral(M,F.n) & Integral(M,(Partial_Sums F).n) = (Partial_Sums I).n proof let n be Nat; reconsider n'=n as Element of NAT by ORDINAL1:def 13; I.n = Integral(M,F.n') by A6; hence I.n = Integral(M,F.n); defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1; set PI = Partial_Sums I; Integral(M,PF.0) = Integral(M,F.0) by Def0; then Integral(M,PF.0) = I.0 by A6; then A8: P2[0] by Def1; B1: for k be Nat st P2[k] holds P2[k+1] proof let k be Nat; assume B2: P2[k]; reconsider k1=k+1 as Nat; A12: dom(PF.k) = E & dom(F.(k+1)) = E by A1,A3,A4,ADD0,MESFUNC8:def 2; A9: PF.k is_measurable_on E & F.(k+1) is_measurable_on E & PF.k is nonnegative & F.(k+1) is nonnegative by A2,G3,ADD1,ADD3C; then consider D be Element of S such that A11: D = dom(PF.k + F.(k+1)) & integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A12,MESFUNC5:84; D = dom(PF.k) /\ dom(F.(k+1)) by A9,A11,MESFUNC5:28 .= E by A12; then A14: (PF.k)|D = PF.k & (F.(k+1))|D = F.(k+1) by A12,RELAT_1:97; dom(PF.(k+1)) = E & PF.(k+1) is_measurable_on E & PF.(k+1) is nonnegative by A1,A3,A4,G3,A2,ADD3C,ADD1,ADD0; then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by MESFUNC5:94 .= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A11,Def0 .= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A9,A12,A14,MESFUNC5:94 .= Integral(M,PF.k) + Integral(M,F.(k+1)) by A9,A12,A14,MESFUNC5:94 .= PI.k + I.(k+1) by A6,B2; hence PI.(k+1) = Integral(M,PF.(k+1)) by Def1; end; for k be Nat holds P2[k] from NAT_1:sch 2(A8,B1); hence Integral(M,(Partial_Sums F).n) = (Partial_Sums I).n; end; end; Th131x: 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 S1: F is additive and S2: F is with_the_same_dom and A2: for n be Nat holds F.n is nonnegative & F.n is_measurable_on E and A3: for x be Element of X st x in E holds F#x is summable; G2:for n be Nat holds F.n is without-infty by A2,MESFUNC5:18; then G3:for n be Nat holds (Partial_Sums F).n is_measurable_on E by A2,ADD1; then A4:lim(Partial_Sums F) is_measurable_on E by A1,S1,S2,A3,ADD2; :: F.1 + F.2 + ... is measurable_on E consider FF be Function of NAT,Funcs(NAT,PFuncs(X,ExtREAL)) such that A5: 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,S2,A2,Th131z; A6: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 A61: x in dom(F.n); let i,j be Element of NAT; assume i in dom((FF.n)#x) & j in dom((FF.n)#x) & i<=j; then ((FF.n).i).x <= ((FF.n).j).x by A5,A61; then ((FF.n)#x).i <= ((FF.n).j).x by MESFUNC5:def 13; hence ((FF.n)#x).i <= ((FF.n)#x).j by MESFUNC5:def 13; end; A7:dom(lim(Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 10; then A72:dom(lim(Partial_Sums F)) = E by A1,Def0; 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; Z1: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:119; take F1; thus for n,m be Nat st n = i1 & m = j1 holds F1 = (FF.n).m; end; consider FF2 be Function of [:NAT,NAT:],PFuncs(X,ExtREAL) such that Z2: for i be Element of NAT for j be Element of NAT holds PP[i,j,FF2.(i,j)] from BINOP_1:sch 3(Z1); :: :: for n,m be Nat st n=i & m=j holds FF2.(i,j)=(FF.n).m :: Q1: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; T0: now let m be Nat; reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13; T1: ProjMap1(FF2,n).m = FF2.(n,m) & ProjMap2(FF2,n).m = FF2.(m,n) by defproj1,defproj2; T2: FF2.(n1,m1) = (FF.n1).m & FF2.(m1,n1) = (FF.m1).n by Z2; dom(F.n1) = dom(F.m1) & dom(F.m1) = dom(F.0) by S2,MESFUNC8:def 2; hence dom(ProjMap1(FF2,n).m) = E & dom(ProjMap2(FF2,n).m) = E by A1,T1,T2,A5; thus ProjMap1(FF2,n).m is_simple_func_in S & ProjMap2(FF2,n).m is_simple_func_in S by A5,T1,T2; 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; dom(ProjMap1(FF2,n).i1) = E & dom(ProjMap1(FF2,n).j1) = E & dom(ProjMap2(FF2,n).i1) = E & dom(ProjMap2(FF2,n).j1) = E by T0; hence dom(ProjMap1(FF2,n).i1) = dom(ProjMap1(FF2,n).j1) & dom(ProjMap2(FF2,n).i1) = dom(ProjMap2(FF2,n).j1); end; hence thesis by Lem10,T0,MESFUNC8:def 2; end; K2: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 13; (ProjMap1(FF2,n)).m = FF2.(n1,m1) by defproj1; then (ProjMap1(FF2,n)).m = (FF.n).m by Z2; hence (ProjMap1(FF2,n)).m is nonnegative by A5; (ProjMap2(FF2,n)).m = FF2.(m1,n1) by defproj2; then (ProjMap2(FF2,n)).m = (FF.m).n by Z2; hence (ProjMap2(FF2,n)).m is nonnegative by A5; end; K3: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; KL0:E = dom(F.n1) by A1,S2,MESFUNC8:def 2; let x be Element of X; assume KK0: x in E; for i,j be Element of NAT st i in dom ((ProjMap1(FF2,n))#x) & j in dom ((ProjMap1(FF2,n))#x) & i<=j holds ((ProjMap1(FF2,n))#x).i <= ((ProjMap1(FF2,n))#x).j proof let i,j be Element of NAT; assume KK5: i in dom((ProjMap1(FF2,n))#x) & j in dom((ProjMap1(FF2,n))#x) & i <= j; reconsider i1=i, j1=j as Nat; KK3: ((FF.n1).i1).x <= ((FF.n1).j1).x by A5,KK0,KL0,KK5; KK1: ((ProjMap1(FF2,n))#x).i = ((ProjMap1(FF2,n)).i).x & ((ProjMap1(FF2,n))#x).j = ((ProjMap1(FF2,n)).j).x by MESFUNC5:def 13; (ProjMap1(FF2,n)).i = FF2.(n,i) by defproj1; then KK2: (ProjMap1(FF2,n)).i = (FF.n1).i1 by Z2; (ProjMap1(FF2,n)).j = FF2.(n,j) by defproj1; hence ((ProjMap1(FF2,n))#x).i <= ((ProjMap1(FF2,n))#x).j by Z2,KK1,KK2,KK3; end; then (ProjMap1(FF2,n))#x is non-decreasing by RINFSUP2:def 10; hence K31: (ProjMap1(FF2,n))#x is convergent by RINFSUP2:37; 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; K321:((ProjMap1(FF2,n))#x).m = ((ProjMap1(FF2,n)).m).x by MESFUNC5:def 13; (ProjMap1(FF2,n)).m is nonnegative by K2; hence k <= m & -1 < ((ProjMap1(FF2,n))#x).m by K321,SUPINF_2:58; end; then K33:not (ProjMap1(FF2,n))#x is convergent_to_-infty by MESFUNC5:def 10; per cases by K31,K33,MESFUNC5:def 11; suppose (ProjMap1(FF2,n))#x is convergent_to_finite_number; then not (ProjMap1(FF2,n))#x is convergent_to_+infty & not (ProjMap1(FF2,n))#x is convergent_to_-infty by MESFUNC5:56,57; then consider lP be real number such that T2: lim( (ProjMap1(FF2,n))#x ) = lP & (for p be real number st 0

= 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 13; assume BB1: p >= n; let x be Element of X; assume BB0: x in E; then BB2:x in dom((ProjMap2(FF2,p)).0) by Q1; ProjMap2(FF2,p) is additive & ProjMap2(FF2,p) is with_the_same_dom & for i be Nat holds ProjMap2(FF2,p).i is nonnegative by Q1,K2; then (Partial_Sums ProjMap2(FF2,p))#x is non-decreasing by BB2,ADD3; then ((Partial_Sums ProjMap2(FF2,p))#x).n1 <= ((Partial_Sums ProjMap2(FF2,p))#x).p1 by BB1,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 K5; thus (P.p).x = ((Partial_Sums ProjMap2(FF2,p)).p).x by K5; ND31:ProjMap2(FF2,p) is additive & ProjMap2(FF2,p) is with_the_same_dom by Q1; ND32: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 13; assume x in dom(ProjMap2(FF2,p).0) /\ dom(F.0); then x in dom(F.0) by XBOOLE_0:def 3; then N322:x in dom(F.n) by S2,MESFUNC8:def 2; ((ProjMap2(FF2,p)).n).x = (FF2.(n1,p1)).x by defproj2; then N323:((ProjMap2(FF2,p)).n).x = ((FF.n).p).x by Z2; (FF.n)#x is non-decreasing by N322,A6; 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 ((FF.n)#x).p <= (F.n).x by N322,A5; hence thesis by N323,MESFUNC5:def 13; end; x in dom(ProjMap2(FF2,p).0) /\ dom(F.0) by BB0,A1,BB2,XBOOLE_0:def 3; hence ((Partial_Sums ProjMap2(FF2,p)).p).x <= ((Partial_Sums F).p).x by S1,S2,ND31,ND32,ADD4; (Partial_Sums F)#x is non-decreasing by BB0,A1,S2,A2,ADD3; 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 ((Partial_Sums F).p).x <= (lim (Partial_Sums F)).x by BB0,A72,MESFUNC8:def 10; end; dom(lim P) = dom(P.0) by MESFUNC8:def 10; then dom(lim P) = dom((Partial_Sums ProjMap2(FF2,0)).0) by K5; then dom(lim P) = dom((ProjMap2(FF2,0)).0) by Def0; then dom(lim P) = dom( FF2.(0,0) ) by defproj2; then N1:dom(lim P) = dom( (FF.0).0 ) by Z2; reconsider FF0 = FF.0 as Functional_Sequence of X,ExtREAL; N21:dom (lim P) = dom(F.0) by A5,N1; dom(lim(Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 10; then N5:dom(lim(Partial_Sums F)) = E by A1,Def0; N8:for x be Element of X st x in dom(lim P) holds P#x is convergent proof let x be Element of X; assume N4: x in dom(lim P); for n,m be Element of NAT st m<=n holds (P#x).m <= (P#x).n proof let n,m be Element of NAT; assume m <= n; then (P.m).x <= (P.n).x by K9,N4,N21,A1; then (P#x).m <= (P.n).x by MESFUNC5:def 13; hence (P#x).m <= (P#x).n by MESFUNC5:def 13; end; then P#x is non-decreasing by RINFSUP2:7; hence P#x is convergent by RINFSUP2:37; end; HHH: 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; assume x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0); then x in dom(F.0) by XBOOLE_0:def 3; then H1: x in dom(F.m) by S2,MESFUNC8:def 2; reconsider m1 = m, k1 = k as Element of NAT by ORDINAL1:def 13; (ProjMap2(FF2,k)).m = FF2.(m1,k1) by defproj2; then H2: (ProjMap2(FF2,k)).m = (FF.m).k by Z2; for j,k be Element of NAT st j in dom((FF.m1)#x) & k in dom((FF.m1)#x) & j <= k holds ((FF.m1)#x).j <= ((FF.m1)#x).k proof let j,k be Element of NAT; assume H3: j in dom((FF.m1)#x) & k in dom((FF.m1)#x) & j <= k; ((FF.m1)#x).j = ((FF.m1).j).x & ((FF.m1)#x).k = ((FF.m1).k).x by MESFUNC5:def 13; hence ((FF.m1)#x).j <= ((FF.m1)#x).k by H1,H3,A5; end; then (FF.m1)#x is non-decreasing by RINFSUP2:def 10; 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 ((FF.m1)#x).k <= (F.m1).x by H1,A5; hence ((ProjMap2(FF2,k)).m).x <= (F.m).x by H2,MESFUNC5:def 13; end; U0: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 N4: x in dom(lim P); (P#x).k = (P.k).x by MESFUNC5:def 13; then U1: (P#x).k = ((Partial_Sums ProjMap2(FF2,k)).k).x by K5; dom((ProjMap2(FF2,k)).0) = E by Q1; then N73:x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0) by N4,A5,N1,A1; ProjMap2(FF2,k) is additive & ProjMap2(FF2,k) is with_the_same_dom & 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 Q1,HHH; then ((Partial_Sums ProjMap2(FF2,k)).k).x <= ((Partial_Sums F).k).x by S1,S2,N73,ADD4; hence (P#x).k <= ((Partial_Sums F)#x).k by U1,MESFUNC5:def 13; end; LL7:for x be Element of X st x in dom(lim P) holds lim(P#x) = lim((Partial_Sums F)#x) proof let x be Element of X; assume N4: x in dom(lim P); then NN8:P#x is convergent by N8; N9: (Partial_Sums F)#x is convergent by N4,N21,S2,A2,ADD3; for k be Element of NAT holds (P#x).k <= ((Partial_Sums F)#x).k by N4,U0; then N10:lim(P#x) <= lim((Partial_Sums F)#x) by NN8,N9,RINFSUP2:38; defpred PP2[Element of NAT,Element of NAT,set] means for n,m be Nat st n = $1 & m = $2 holds $3 = (Partial_Sums ProjMap2(FF2,n)).m; ZZ1:for i1 be Element of NAT for j1 be Element of NAT ex PP2 be Element of PFuncs(X,ExtREAL) st PP2[i1,j1,PP2] proof let i1 be Element of NAT; let j1 be Element of NAT; reconsider i = i1, j = j1 as Nat; reconsider F1 = (Partial_Sums ProjMap2(FF2,i)).j as Element of PFuncs(X,ExtREAL) by PARTFUN1:119; take F1; thus for n,m be Nat st n = i1 & m = j1 holds F1 = (Partial_Sums ProjMap2(FF2,n)).m; end; consider PP2 be Function of [:NAT,NAT:],PFuncs(X,ExtREAL) such that ZZ2: for i be Element of NAT for j be Element of NAT holds PP2[i,j,PP2.(i,j)] from BINOP_1:sch 3(ZZ1); ZZ3:for p,n be Element of NAT holds (ProjMap2(PP2,n)).p = (Partial_Sums ProjMap2(FF2,p)).n proof let p,n be Element of NAT; reconsider p1 = p, n1 = n as Nat; (ProjMap2(PP2,n)).p = PP2.(p,n) by defproj2; hence thesis by ZZ2; end; J2: for n be Element of NAT holds ((ProjMap2(PP2,n))#x) is convergent & ((ProjMap2(PP2,n))#x)^\n is convergent & lim ((ProjMap2(PP2,n))#x) = lim (((ProjMap2(PP2,n))#x)^\n) proof let n be Element of NAT; now let j,k be Element of NAT; assume J21: j in dom((ProjMap2(PP2,n))#x) & k in dom((ProjMap2(PP2,n))#x) & j <= k; :: ((ProjMap2(PP2,n))#x).k = f_1,k(x) + f_2,k(x) + ... + f_n,k(x) ((ProjMap2(PP2,n))#x).j = ((ProjMap2(PP2,n)).j).x & ((ProjMap2(PP2,n))#x).k = ((ProjMap2(PP2,n)).k).x by MESFUNC5:def 13; then J22: ((ProjMap2(PP2,n))#x).j = ((Partial_Sums ProjMap2(FF2,j)).n).x & ((ProjMap2(PP2,n))#x).k = ((Partial_Sums ProjMap2(FF2,k)).n).x by ZZ3; J23: ProjMap2(FF2,j) is additive & ProjMap2(FF2,j) is with_the_same_dom & ProjMap2(FF2,k) is additive & ProjMap2(FF2,k) is with_the_same_dom by Q1; N73: dom((ProjMap2(FF2,j)).0) = E & dom((ProjMap2(FF2,k)).0) = E by Q1; then for i be Nat, z be Element of X st z in dom((ProjMap2(FF2,j)).0) /\ dom((ProjMap2(FF2,k)).0) holds ((ProjMap2(FF2,j)).i).z <= ((ProjMap2(FF2,k)).i).z by J21,K7; hence ((ProjMap2(PP2,n))#x).j <= ((ProjMap2(PP2,n))#x).k by J22,J23,ADD4,N73,N21,A1,N4; end; then (ProjMap2(PP2,n))#x is non-decreasing by RINFSUP2:def 10; hence (ProjMap2(PP2,n))#x is convergent by RINFSUP2:37; hence ((ProjMap2(PP2,n))#x)^\n is convergent & lim ((ProjMap2(PP2,n))#x) = lim (((ProjMap2(PP2,n))#x)^\n) by RINFSUP2:21; end; lim((Partial_Sums F)#x) <= lim(P#x) proof F#x is summable by A3,N21,A1,N4; then R00: Partial_Sums(F#x) is convergent by Def2; R0: (Partial_Sums F)#x is convergent proof per cases by R00,MESFUNC5:def 11; suppose Partial_Sums(F#x) is convergent_to_finite_number; then (Partial_Sums F)#x is convergent_to_finite_number by S1,S2,N21,N4,Cor01; hence (Partial_Sums F)#x is convergent by MESFUNC5:def 11; end; suppose Partial_Sums(F#x) is convergent_to_+infty; then (Partial_Sums F)#x is convergent_to_+infty by S1,S2,N21,N4,Cor01; hence (Partial_Sums F)#x is convergent by MESFUNC5:def 11; end; suppose Partial_Sums(F#x) is convergent_to_-infty; then (Partial_Sums F)#x is convergent_to_-infty by S1,S2,N21,N4,Cor01; hence (Partial_Sums F)#x is convergent by MESFUNC5:def 11; end; end; for n be Nat holds ((Partial_Sums F)#x).n <= lim(P#x) proof let n be Nat; reconsider n'=n as Element of NAT by ORDINAL1:def 13; R1: (P#x)^\n' is convergent & lim((P#x)^\n') = lim(P#x) by NN8,RINFSUP2:21; R2: ((ProjMap2(PP2,n))#x)^\n' is convergent by J2; for p be Element of NAT holds (((ProjMap2(PP2,n))#x)^\n').p <= ((P#x)^\n').p proof let p be Element of NAT; (((ProjMap2(PP2,n))#x)^\n').p = ((ProjMap2(PP2,n))#x).(n+p) by KURATO_2:def 2; then (((ProjMap2(PP2,n))#x)^\n').p = ((ProjMap2(PP2,n)).(n+p)).x by MESFUNC5:def 13; then R3: (((ProjMap2(PP2,n))#x)^\n').p = ((Partial_Sums ProjMap2(FF2,n+p)).n).x by ZZ3; ((P#x)^\n').p = (P#x).(n+p) by KURATO_2:def 2; then ((P#x)^\n').p = (P.(n+p)).x by MESFUNC5:def 13; then R4: ((P#x)^\n').p = ((Partial_Sums ProjMap2(FF2,n+p)).(n+p)).x by K5; R51: n <= n+p by NAT_1:11; R52: x in dom((ProjMap2(FF2,n+p)).0) by Q1,N21,A1,N4; ProjMap2(FF2,n+p) is additive & ProjMap2(FF2,n+p) is with_the_same_dom & for i be Nat holds ProjMap2(FF2,n+p).i is nonnegative by Q1,K2; then (Partial_Sums ProjMap2(FF2,n+p))#x is non-decreasing by R52,ADD3; then ((Partial_Sums ProjMap2(FF2,n+p))#x).n' <= ((Partial_Sums ProjMap2(FF2,n+p))#x).(n'+p) by R51,RINFSUP2:7; then ((Partial_Sums ProjMap2(FF2,n+p))#x).n' <= ((Partial_Sums ProjMap2(FF2,n+p)).(n+p)).x by MESFUNC5:def 13; hence (((ProjMap2(PP2,n))#x)^\n').p <= ((P#x)^\n').p by R3,R4,MESFUNC5:def 13; end; then lim(((ProjMap2(PP2,n))#x)^\n') <= lim((P#x)^\n') by R1,R2,RINFSUP2:38; then J3: lim((ProjMap2(PP2,n))#x) <= lim (P#x) by R1,J2; defpred C[Nat] means lim((ProjMap2(PP2,$1))#x) = ((Partial_Sums F)#x).$1; V1: lim((ProjMap2(PP2,0))#x) = (F.0).x proof for p be set st p in NAT holds ((ProjMap2(PP2,0))#x).p = ((ProjMap1(FF2,0))#x).p proof let p be set; assume p in NAT; then reconsider p'=p as Element of NAT; V74: ((ProjMap2(PP2,0))#x).p = ((ProjMap2(PP2,0)).p').x by MESFUNC5:def 13; (ProjMap2(PP2,0)).p' = (Partial_Sums ProjMap2(FF2,p')).0 by ZZ3; then (ProjMap2(PP2,0)).p' = (ProjMap2(FF2,p')).0 by Def0; then (ProjMap2(PP2,0)).p' = FF2.(0,p') by defproj2; then (ProjMap2(PP2,0)).p' = (ProjMap1(FF2,0)).p' by defproj1; hence thesis by V74,MESFUNC5:def 13; end; then (ProjMap2(PP2,0))#x = (ProjMap1(FF2,0))#x by FUNCT_2:18; hence lim((ProjMap2(PP2,0))#x) = (F.0).x by K3,N4,N21,A1; end; ((Partial_Sums F)#x).0 = ((Partial_Sums F).0).x by MESFUNC5:def 13; then V2: C[0] by V1,Def0; V3: for k be Nat st C[k] holds C[k+1] proof let k be Nat; reconsider k'=k as Element of NAT by ORDINAL1:def 13; assume V31: C[k]; (ProjMap2(PP2,k'))#x is convergent by J2; then V41: (ProjMap2(PP2,k))#x is convergent & (ProjMap1(FF2,k+1))#x is convergent by K3,N4,N21,A1; now let m be set; assume m in dom((ProjMap2(PP2,k))#x); then reconsider m1=m as Element of NAT; V413: for l be Nat holds (ProjMap2(FF2,m1)).l is nonnegative by K2;