:: The Lebesgue Monotone Convergence Theorem
::  by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received March 18, 2008
:: Copyright (c) 2008-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, SUBSET_1, SEQFUNC, MESFUNC5,
      PARTFUN1, XXREAL_0, NAT_1, RELAT_1, ARYTM_3, ARYTM_1, FUNCT_1, ORDINAL2,
      CARD_1, COMPLEX1, SEQ_2, SUPINF_2, XXREAL_2, RINFSUP1, TARSKI, REAL_1,
      PBOOLE, MESFUNC1, VALUED_1, FUNCT_3, MESFUNC2, SUPINF_1, VALUED_0,
      RFUNCT_3, SERIES_1, CARD_3, MESFUNC8, MSSUBFAM, SETFAM_1, INTEGRA5,
      FUNCOP_1, ZFMISC_1, FUNCT_2, MEASURE2, MESFUNC9, FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3,
      XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, VALUED_0, RELAT_1,
      FUNCT_1, RELSET_1, BINOP_1, FUNCT_2, PARTFUN1, NAT_1, PROB_1, SETFAM_1,
      SUPINF_1, SUPINF_2, XXREAL_2, MEASURE1, MEASURE2, EXTREAL1, MESFUNC1,
      MEASURE6, MESFUNC2, SEQFUNC, MESFUNC5, MESFUNC8, RINFSUP2, FUNCOP_1;
 constructors REAL_1, EXTREAL1, BINOP_1, NEWTON, MESFUNC1, MEASURE2, MEASURE6,
      MESFUNC2, MESFUNC5, MESFUNC8, RINFSUP2, SUPINF_1, SEQFUNC, RELSET_1,
      BINOP_2, NUMBERS;
 registrations SUBSET_1, NAT_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1,
      MEASURE1, FUNCT_2, RELAT_1, XBOOLE_0, NUMBERS, XXREAL_0, XCMPLX_0,
      MESFUNC8, FUNCT_1, VALUED_0, XXREAL_3, RELSET_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions MESFUNC5, MESFUNC8, TARSKI, VALUED_0;
 equalities MESFUNC1, MESFUNC5, BINOP_1, RINFSUP2, XXREAL_3, SUPINF_2;
 expansions MESFUNC5, MESFUNC8, TARSKI, FUNCT_2;
 theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, 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,
      SEQFUNC, ORDINAL1, SETFAM_1, MESFUNC8, RINFSUP2, MESFUNC7, SEQ_4,
      RELSET_1, MEASURE2, XXREAL_2, VALUED_0, FUNCOP_1, XXREAL_3;
 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 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 ExtReal,
  n,m for Nat,
  x for Element of X,
  z,D for set;

theorem
  f is without+infty & g is without+infty implies dom(f+g)=dom f /\ dom g
proof
  assume that
A1: f is without+infty and
A2: g is without+infty;
  not +infty in rng g by A2;
  then
A3: g"{+infty} = {} by FUNCT_1:72;
  not +infty in rng f by A1;
  then f"{+infty} = {} by FUNCT_1:72;
  then f"{+infty} /\ g"{-infty} \/ f"{-infty} /\ g"{+infty} = {} by A3;
  then dom(f+g) = (dom f /\ dom g)\{} by MESFUNC1:def 3;
  hence thesis;
end;

theorem
  f is without+infty & g is without-infty implies dom(f-g)=dom f /\ dom g
proof
  assume that
A1: f is without+infty and
A2: g is without-infty;
  not +infty in rng f by A1;
  then
A3: f"{+infty} = {} by FUNCT_1:72;
  not -infty in rng g by A2;
  then g"{-infty} = {} by FUNCT_1:72;
  then g"{+infty} /\ f"{+infty} \/ g"{-infty} /\ f"{-infty} = {} by A3;
  then dom(f-g) = (dom f /\ dom g)\{} by MESFUNC1:def 4;
  hence thesis;
end;

theorem Th3:
  f is without-infty & g is without-infty implies f+g is without-infty
proof
  assume that
A1: f is without-infty and
A2: g is without-infty;
  for x be set st x in dom(f+g) holds -infty < (f+g).x
  proof
    let x be set;
    assume
A3: x in dom(f+g);
A4: -infty < f.x by A1;
A5: -infty < g.x by A2;
    (f+g).x = f.x + g.x by A3,MESFUNC1:def 3;
    hence thesis by A4,A5,XXREAL_0:6,XXREAL_3:17;
  end;
  hence thesis by MESFUNC5:10;
end;

theorem Th4:
  f is without+infty & g is without+infty implies f+g is without+infty
proof
  assume that
A1: f is without+infty and
A2: g is without+infty;
  for x be set st x in dom(f+g) holds (f+g).x < +infty
  proof
    let x be set;
    assume
A3: x in dom(f+g);
A4: f.x < +infty by A1;
A5: g.x < +infty by A2;
    (f+g).x = f.x + g.x by A3,MESFUNC1:def 3;
    hence thesis by A4,A5,XXREAL_0:4,XXREAL_3:16;
  end;
  hence thesis by MESFUNC5:11;
end;

theorem
  f is without-infty & g is without+infty implies f-g is without-infty
proof
  assume that
A1: f is without-infty and
A2: g is without+infty;
  for x be set st x in dom(f-g) holds -infty < (f-g).x
  proof
    let x be set;
    assume
A3: x in dom(f-g);
A4: -infty < f.x by A1;
A5: g.x < +infty by A2;
    (f-g).x = f.x - g.x by A3,MESFUNC1:def 4;
    hence thesis by A4,A5,XXREAL_0:6,XXREAL_3:19;
  end;
  hence thesis by MESFUNC5:10;
end;

theorem
  f is without+infty & g is without-infty implies f-g is without+infty
proof
  assume that
A1: f is without+infty and
A2: g is without-infty;
  for x be set st x in dom(f-g) holds (f-g).x < +infty
  proof
    let x be set;
    assume
A3: x in dom(f-g);
A4: f.x < +infty by A1;
A5: -infty < g.x by A2;
    (f-g).x = f.x - g.x by A3,MESFUNC1:def 4;
    hence thesis by A4,A5,XXREAL_0:4,XXREAL_3:18;
  end;
  hence thesis by MESFUNC5:11;
end;

theorem Th7:
  ( seq is convergent_to_finite_number implies ex g be Real
st lim seq = g & for p be Real st 0<p ex n be Nat st for m be Nat st n<=
m holds |. seq.m - lim seq .| < p ) & ( seq is convergent_to_+infty implies lim
  seq = +infty ) & ( seq is convergent_to_-infty implies lim seq = -infty )
proof
A1: now
    assume
A2: seq is convergent_to_finite_number;
    then
A3: not seq is convergent_to_+infty by MESFUNC5:50;
A4: not seq is convergent_to_-infty by A2,MESFUNC5:51;
    seq is convergent by A2;
    then consider g be Real such that
A5: lim seq = g and
A6: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
    holds |.seq.m - lim seq.| < p and
    seq is convergent_to_finite_number by A3,A4,MESFUNC5:def 12;
    take g;
    thus ex g be Real st lim seq = g & for p be Real st 0<p ex n
    be Nat st for m be Nat st n<=m holds |. seq.m - lim seq .| < p by A5,A6;
  end;
A7: now
    assume
A8: seq is convergent_to_-infty;
    then seq is convergent;
    hence lim seq = -infty by A8,MESFUNC5:def 12;
  end;
  now
    assume
A9: seq is convergent_to_+infty;
    then seq is convergent;
    hence lim seq = +infty by A9,MESFUNC5:def 12;
  end;
  hence thesis by A1,A7;
end;

theorem Th8:
  seq is nonnegative implies not seq is convergent_to_-infty
proof
  assume
A1: seq is nonnegative;
  assume seq is convergent_to_-infty;
  then consider n be Nat such that
A2: for m be Nat st n<=m holds seq.m <= -1;
  seq.n <= -1 by A2;
  hence contradiction by A1,SUPINF_2:51;
end;

theorem Th9:
  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 ExtReal holds y in rng seq implies y <= p
  proof
    let y be ExtReal;
    assume y in rng seq;
    then consider x be object such that
A3: x in dom seq and
A4: y = seq.x by FUNCT_1:def 3;
    reconsider x as Nat by A3;
    seq.x <= p by A2;
    hence thesis by A4;
  end;
  then
A5: p is UpperBound of rng seq by XXREAL_2:def 1;
  reconsider SUPSEQ = superior_realsequence seq as sequence of ExtREAL;
  consider Y be non empty Subset of ExtREAL such that
A6: Y = {seq.k where k is Nat: 0 <= k} and
A7: SUPSEQ.0 = sup Y by RINFSUP2:def 7;
  now
    let x be object;
    assume x in rng seq;
    then consider k be object such that
A8: k in dom seq and
A9: x = seq.k by FUNCT_1:def 3;
    thus x in Y by A6,A8,A9;
  end;
  then
A10: rng seq c= Y;
  for n be Element of NAT holds 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 3;
    hence thesis by XXREAL_2:3;
  end;
  then
A11: inf SUPSEQ <= SUPSEQ.0;
  now
    let x be object;
    assume x in Y;
    then consider k be Nat such that
A12:   x = seq.k & 0 <= k by A6;
A13: k in NAT by ORDINAL1:def 12;
    dom seq = NAT by FUNCT_2:def 1;
    hence x in rng seq by A12,FUNCT_1:3,A13;
  end;
  then Y c= rng seq;
  then Y = rng seq by A10,XBOOLE_0:def 10;
  then (superior_realsequence seq).0 <= p by A5,A7,XXREAL_2:def 3;
  then lim_sup seq <= p by A11,XXREAL_0:2;
  hence thesis by A1,RINFSUP2:41;
end;

theorem Th10:
  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 ExtReal holds y in rng seq implies p <= y
  proof
    let y be ExtReal;
    assume y in rng seq;
    then consider x be object such that
A3: x in dom seq and
A4: y = seq.x by FUNCT_1:def 3;
    reconsider x as Nat by A3;
    seq.x >= p by A2;
    hence thesis by A4;
  end;
  then
A5: p is LowerBound of rng seq by XXREAL_2:def 2;
  reconsider INFSEQ = inferior_realsequence seq as sequence of ExtREAL;
  consider Y be non empty Subset of ExtREAL such that
A6: Y = {seq.k where k is Nat: 0 <= k} and
A7: INFSEQ.0 = inf Y by RINFSUP2:def 6;
  now
    let x be object;
    assume x in rng seq;
    then consider k be object such that
A8: k in dom seq and
A9: x = seq.k by FUNCT_1:def 3;
    thus x in Y by A6,A8,A9;
  end;
  then
A10: rng seq c= Y;
  for n be Element of NAT holds sup INFSEQ >= INFSEQ.n
  proof
    let n be Element of NAT;
    NAT = dom INFSEQ by FUNCT_2:def 1;
    then INFSEQ.n in rng INFSEQ by FUNCT_1:def 3;
    hence thesis by XXREAL_2:4;
  end;
  then
A11: sup INFSEQ >= INFSEQ.0;
  now
    let x be object;
    assume x in Y;
    then consider k be Nat such that
A12: x = seq.k & 0 <= k by A6;
A13: k in NAT by ORDINAL1:def 12;
    dom seq = NAT by FUNCT_2:def 1;
    hence x in rng seq by A12,FUNCT_1:3,A13;
  end;
  then Y c= rng seq;
  then Y = rng seq by A10,XBOOLE_0:def 10;
  then (inferior_realsequence seq).0 >= p by A5,A7,XXREAL_2:def 4;
  then lim_inf seq >= p by A11,XXREAL_0:2;
  hence thesis by A1,RINFSUP2:41;
end;

reconsider zz=0 as ExtReal;

theorem Th11:
 seq1 is convergent & seq2 is convergent & seq1 is nonnegative &
seq2 is nonnegative & (for k be Nat holds seq.k = seq1.k + seq2.k) implies seq
  is nonnegative & seq is convergent & lim seq = lim seq1 + lim seq2
proof
  assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: seq1 is nonnegative and
A4: seq2 is nonnegative and
A5: for k be Nat holds seq.k = seq1.k + seq2.k;
A6: not seq2 is convergent_to_-infty by A4,Th8;
  for n be object st n in dom seq holds 0. <= seq.n
  proof
    let n be object;
    assume n in dom seq;
    then reconsider n1=n as Nat;
A7: 0 <= seq2.n1 by A4,SUPINF_2:51;
A8: seq.n1 = seq1.n1 + seq2.n1 by A5;
    0 <= seq1.n1 by A3,SUPINF_2:51;
    hence thesis by A7,A8;
  end;
  hence seq is nonnegative by SUPINF_2:52;
A9: not seq1 is convergent_to_-infty by A3,Th8;
  for n be Nat holds 0 <= seq2.n by A4,SUPINF_2:51;
  then
A10: lim seq2 <> -infty by A2,Th10;
  per cases by A1,A9;
  suppose
A11: seq1 is convergent_to_+infty;
    for g be Real st 0 < g ex n be Nat st for m be Nat st n<=m
    holds g <= seq.m
    proof
      let g be Real;
      assume 0 < g;
      then consider n be Nat such that
A12:  for m be Nat st n <= m holds g <= seq1.m by A11;
      take n;
      let m be Nat;
      assume n<=m;
      then
A13:  g <= seq1.m by A12;
      0 <= seq2.m by A4,SUPINF_2:51;
      then  g + zz <= seq1.m + seq2.m by A13,XXREAL_3:36;
      then g <= seq1.m + seq2.m by XXREAL_3:4;
      hence thesis by A5;
    end;
    then
A14: seq is convergent_to_+infty;
    hence seq is convergent;
    then
A15: lim seq = +infty by A14,MESFUNC5:def 12;
    lim seq1 = +infty by A1,A11,MESFUNC5:def 12;
    hence thesis by A10,A15,XXREAL_3:def 2;
  end;
  suppose
A16: seq1 is convergent_to_finite_number;
    then
A17: not seq1 is convergent_to_-infty by MESFUNC5:51;
    not seq1 is convergent_to_+infty by A16,MESFUNC5:50;
    then consider g be Real such that
A18: lim seq1 = g and
A19: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
    holds |. seq1.m - lim seq1 .| < p and
    seq1 is convergent_to_finite_number by A1,A17,MESFUNC5:def 12;
    per cases by A2,A6;
    suppose
A20:  seq2 is convergent_to_+infty;
      for g be Real st 0 < g ex n be Nat st for m be Nat st n<=m
      holds g <= seq.m
      proof
        let g be Real;
        assume 0 < g;
        then consider n be Nat such that
A21:    for m be Nat st n <= m holds g <= seq2.m by A20;
        take n;
        let m be Nat;
        assume n<=m;
        then
A22:    g <= seq2.m by A21;
        0 <= seq1.m by A3,SUPINF_2:51;
        then  g + zz <= seq1.m + seq2.m by A22,XXREAL_3:36;
        then g <= seq1.m + seq2.m by XXREAL_3:4;
        hence thesis by A5;
      end;
      then
A23:  seq is convergent_to_+infty;
      hence seq is convergent;
      then
A24:  lim seq = +infty by A23,MESFUNC5:def 12;
      lim seq2 = +infty by A2,A20,MESFUNC5:def 12;
      hence thesis by A18,A24,XXREAL_3:def 2;
    end;
    suppose
A25:  seq2 is convergent_to_finite_number;
      then
A26:  seq2 is not convergent_to_-infty by MESFUNC5:51;
      seq2 is not convergent_to_+infty by A25,MESFUNC5:50;
      then consider h be Real such that
A27:  lim seq2 = h and
A28:  for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
      holds |. seq2.m - lim seq2 .| < p and
      seq2 is convergent_to_finite_number by A2,A26,MESFUNC5:def 12;
      reconsider h9=h, g9=g as Real;
      reconsider gh = g+h as R_eal by XXREAL_0:def 1;
A29:  for p be Real st 0<p ex n be Nat st for m be Nat st n <= m
      holds |. seq.m - (g+h).| < p
      proof
       let p be Real;
        reconsider pp= p as Element of REAL by XREAL_0:def 1;
        assume
A30:    0 < p;
        then consider n1 be Nat such that
A31:    for m be Nat st n1 <= m holds |. seq1.m - lim seq1 .| < p/2 by A19;
        consider n2 be Nat such that
A32:    for m be Nat st n2 <= m holds |. seq2.m - lim seq2 .| < p/2 by A28,A30;
        reconsider n19=n1, n29=n2 as Element of NAT by ORDINAL1:def 12;
        reconsider n = max(n19,n29) as Nat;
        take n;
        let m be Nat;
        assume
A33:    n <= m;
A34:     pp/2 in REAL by XREAL_0:def 1;
        n2 <= n by XXREAL_0:25;
        then n2 <= m by A33,XXREAL_0:2;
        then
A35:    |. seq2.m - lim seq2 .| < pp/2 by A32;
        then |. seq2.m - lim seq2 .| < +infty by XXREAL_0:2,9,A34;
        then
A36:    seq2.m -  h in REAL by A27,EXTREAL1:41;
        n1 <= n by XXREAL_0:25;
        then n1 <= m by A33,XXREAL_0:2;
        then
A37:    |. seq1.m - lim seq1 .| < pp/2 by A31;
        then |. seq1.m - lim seq1 .| < +infty by XXREAL_0:2,9,A34;
        then seq1.m -  g in REAL by A18,EXTREAL1:41;
        then consider e1,e2 be Real such that
A38:    e1 = seq1.m -  g and
A39:    e2 = seq2.m -  h by A36;
A40:    |. seq2.m -  h .| = |.e2 qua Complex.| by A39,EXTREAL1:12;
A41:    0 <= seq2.m by A4,SUPINF_2:51;
        then
A42:    seq2.m -  h <> -infty by XXREAL_3:19;
A43:    0 <= seq1.m by A3,SUPINF_2:51;
A44:    |. seq1.m -  g .| = |.e1 qua Complex.| by A38,EXTREAL1:12;
        then
A45:    |. seq2.m -  h .| + |. seq1.m -  g .|
             = |.e1 qua Complex.| + |.e2 qua Complex.|
        by A40,SUPINF_2:1;
        (g+h) =  g +  (h qua ExtReal);
        then seq.m - (g+h) = seq.m -  h -  g by XXREAL_3:31
          .= seq1.m + seq2.m -  h -  g by A5
          .= seq1.m + (seq2.m -  h) -  g by A43,A41,XXREAL_3:30
          .= (seq2.m -  h) + (seq1.m -  g) by A43,A42,XXREAL_3:30;
        then
A46:    |. seq.m - (g+h) .| <= |. seq2.m -  h .| + |. seq1.m - g .|
                by EXTREAL1:24;
        |.e1 qua Complex.| + |.e2 qua Complex.| < p/2 + p/2
          by A18,A27,A37,A35,A44,A40,XREAL_1:8;
        hence thesis by A46,A45,XXREAL_0:2;
      end;
      then
A47:  seq is convergent_to_finite_number;
      hence seq is convergent;
      then lim seq = gh by A29,A47,MESFUNC5:def 12;
      hence thesis by A18,A27,SUPINF_2:1;
    end;
  end;
end;

theorem Th12:
  (for n be Nat holds G.n = (F.n)|D) & x in D implies (F#x is
  convergent_to_+infty implies G#x is convergent_to_+infty) & (F#x is
  convergent_to_-infty implies G#x is convergent_to_-infty) & (F#x is
convergent_to_finite_number implies G#x is convergent_to_finite_number) & (F#x
  is convergent implies G#x is convergent)
proof
  assume that
A1: for n be Nat holds G.n = (F.n)|D and
A2: x in D;
  thus
A3: F#x is convergent_to_+infty implies G#x is convergent_to_+infty
  proof
    assume
A4: F#x is convergent_to_+infty;
    let g be Real;
    assume 0 < g;
    then consider n be Nat such that
A5: for m be Nat st n <= m holds g <= (F#x).m by A4;
    take n;
    let m be Nat;
    assume n <= m;
    then g <= (F#x).m by A5;
    then g <= (F.m).x by MESFUNC5:def 13;
    then g <= ((F.m)|D).x by A2,FUNCT_1:49;
    then g <= (G.m).x by A1;
    hence g <= (G#x).m by MESFUNC5:def 13;
  end;
  thus
A6: F#x is convergent_to_-infty implies G#x is convergent_to_-infty
  proof
    assume
A7: F#x is convergent_to_-infty;
    let g be Real;
    assume g < 0;
    then consider n be Nat such that
A8: for m be Nat st n <= m holds (F#x).m <= g by A7;
    take n;
    let m be Nat;
    assume n <= m;
    then (F#x).m <= g by A8;
    then (F.m).x <= g by MESFUNC5:def 13;
    then ((F.m)|D).x <= g by A2,FUNCT_1:49;
    then (G.m).x <= g by A1;
    hence (G#x).m <= g by MESFUNC5:def 13;
  end;
  thus
A9: F#x is convergent_to_finite_number implies G#x is
  convergent_to_finite_number
  proof
    assume F#x is convergent_to_finite_number;
    then consider g be Real such that
A10: lim(F#x) = g and
A11: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
    holds |. (F#x).m - lim(F#x) .| < p by Th7;
    for p be Real st 0 < p ex n be Nat st for m be Nat st n <= m
    holds |. (G#x).m - (g) .| < p
    proof
      let p be Real;
      assume 0 < p;
      then consider n be Nat such that
A12:  for m be Nat st n <= m holds |. (F#x).m - lim(F#x) .| < p by A11;
      take n;
      let m be Nat;
      (F#x).m = (F.m).x by MESFUNC5:def 13;
      then (F#x).m = ((F.m)|D).x by A2,FUNCT_1:49;
      then
A13:  (F#x).m = (G.m).x by A1;
      assume n <= m;
      then |. (F#x).m - lim(F#x) .| < p by A12;
      hence thesis by A10,A13,MESFUNC5:def 13;
    end;
    hence thesis;
  end;
  assume
A14: F#x is convergent;
  per cases by A14;
  suppose
    F#x is convergent_to_+infty;
    hence thesis by A3;
  end;
  suppose
    F#x is convergent_to_-infty;
    hence thesis by A6;
  end;
  suppose
    F#x is convergent_to_finite_number;
    hence thesis by A9;
  end;
end;

theorem Th13:
  E = dom f & f is E-measurable & f is nonnegative & M.(E /\
  eq_dom(f,+infty)) <> 0 implies Integral(M,f) = +infty
proof
  assume that
A1: E = dom f and
A2: f is E-measurable and
A3: f is nonnegative and
A4: M.(E /\ eq_dom(f,+infty)) <> 0;
  reconsider EE = E /\ eq_dom(f,+infty) as Element of S by A1,A2,MESFUNC1:33;
A5: dom(f|E) = E by A1;
  E = dom f /\ E by A1;
  then
A6: f|E is E-measurable by A2,MESFUNC5:42;
  integral+(M,f|EE) <= integral+(M,f|E) by A1,A2,A3,MESFUNC5:83,XBOOLE_1:17;
  then
A7: integral+(M,f|EE) <= Integral(M,f|E) by A3,A6,A5,MESFUNC5:15,88;
A8: EE = dom f /\ EE by A1,XBOOLE_1:17,28;
  f is EE-measurable by A2,MESFUNC1:30,XBOOLE_1:17;
  then
A9: f|EE is EE-measurable by A8,MESFUNC5:42;
A10: f|EE is nonnegative by A3,MESFUNC5:15;
  reconsider ES = {} as Element of S by PROB_1:4;
  deffunc G(Element of NAT) = $1(#)((chi(EE,X))|EE);
  consider G be Function such that
A11: dom G = NAT & for n be Element of NAT holds G.n = G(n) from FUNCT_1
  :sch 4;
  now
    let g be object;
    assume g in rng G;
    then consider m be object such that
A12: m in dom G and
A13: g = G.m by FUNCT_1:def 3;
    reconsider m as Element of NAT by A11,A12;
    g = m(#)((chi(EE,X))|EE) by A11,A13;
    hence g in PFuncs(X,ExtREAL) by PARTFUN1:45;
  end;
  then rng G c= PFuncs(X,ExtREAL);
  then reconsider G as Functional_Sequence of X,ExtREAL by A11,FUNCT_2:def 1
,RELSET_1:4;
A14: for n be Nat holds dom(G.n) = EE & for x be set st x in dom(G.n) holds (
  G.n).x = n
  proof
    let n be Nat;
    reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
    EE c= X;
    then EE c= dom(chi(EE,X)) by FUNCT_3:def 3;
    then
A15: dom((chi(EE,X))|EE) = EE by RELAT_1:62;
A16: G.n = n1(#)((chi(EE,X))|EE) by A11;
    hence
A17: dom(G.n) = EE by A15,MESFUNC1:def 6;
    let x be set;
    assume
A18: x in dom(G.n);
    then reconsider x1=x as Element of X;
    chi(EE,X).x1 = 1. by A17,A18,FUNCT_3:def 3;
    then ((chi(EE,X))|EE).x1 = 1. by A15,A17,A18,FUNCT_1:47;
    then (G.n).x = ( n1) * 1. by A16,A18,MESFUNC1:def 6;
    hence thesis by XXREAL_3:81;
  end;
A19: for n be Nat holds G.n is nonnegative
  proof
    let n be Nat;
    for x be object st x in dom(G.n) holds 0 <= (G.n).x by A14;
    hence thesis by SUPINF_2:52;
  end;
  deffunc K(Element of NAT) = integral'(M,G.$1);
  consider K be sequence of ExtREAL such that
A20: for n be Element of NAT holds K.n = K(n) from FUNCT_2:sch 4;
  reconsider K as ExtREAL_sequence;
A21: for n be Nat holds K.n=integral'(M,G.n)
  proof
    let n be Nat;
    reconsider n1=n as Element of NAT by ORDINAL1:def 12;
    K.n = integral'(M,G.n1) by A20;
    hence thesis;
  end;
A22: dom(f|EE) = EE by A1,RELAT_1:62,XBOOLE_1:17;
A23: for n,m be Nat st n <=m holds for x be Element of X st x in dom(f|EE)
  holds (G.n).x <= (G.m).x
  proof
    let n,m be Nat such that
A24: n <= m;
    let x be Element of X;
    assume
A25: x in dom(f|EE);
    then x in dom(G.n) by A22,A14;
    then
A26: (G.n).x = n by A14;
    x in dom(G.m) by A22,A14,A25;
    hence thesis by A14,A24,A26;
  end;
A27: for n be Nat holds dom(G.n) = dom(f|EE) & G.n is_simple_func_in S
  proof
    let n be Nat;
    reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
    thus
A28: dom(G.n) = dom(f|EE) by A22,A14;
    for x be object st x in dom(G.n) holds (G.n).x = n1 by A14;
    hence thesis by A22,A28,MESFUNC6:2;
  end;
A29: for i be Element of NAT holds K.i = ( i)*(M.(dom(G.i)))
  proof
    let i be Element of NAT;
     reconsider ii=i as R_eal by XXREAL_0:def 1;
    for x be object st x in dom(G.i) holds (G.ii).x =  ii by A14;
    then integral'(M,G.i) = (ii)*(M.(dom(G.ii)))
            by A27,MESFUNC5:71;
    hence thesis by A21;
  end;
  M.ES <= M.EE by MEASURE1:31,XBOOLE_1:2;
  then
A30: In(0,REAL) < M.EE by A4,VALUED_0:def 19;
A31: not rng K is bounded_above
  proof
    assume rng K is bounded_above;
    then consider UB be Real such that
A32: UB is UpperBound of rng K by XXREAL_2:def 10;
    reconsider r = UB as Real;
    per cases by A30,XXREAL_0:10;
    suppose
A33:  M.EE = +infty;
      K.1 = ( 1) * (M.(dom(G.1))) by A29;
      then K.1 = ( 1) * (M.EE) by A14;
      then
A34:  K.1 = +infty by A33,XXREAL_3:def 5;
      dom K = NAT by FUNCT_2:def 1;
      then K.1 in rng K by FUNCT_1:3;
      then K.1 <= UB by A32,XXREAL_2:def 1;
      hence contradiction by A34,XXREAL_0:4;
    end;
    suppose
      M.EE in REAL;
      then reconsider ee = M.EE as Real;
      consider n be Nat such that
A35:  r/ee < n by SEQ_4:3;
A36:   n in NAT by ORDINAL1:def 12;
      K.n = ( n) * (M.(dom(G.n))) by A29,A36;
      then K.n = ( n) * (M.EE) by A14;
      then
A37:  K.n = n * ee by EXTREAL1:1;
      (r/ee) * ee < n * ee by A30,A35,XREAL_1:68;
      then r / (ee/ee) < K.n by A37,XCMPLX_1:82;
      then
A38:  r < K.n by A4,XCMPLX_1:51;
      dom K = NAT by FUNCT_2:def 1;
      then K.n in rng K by FUNCT_1:3,A36;
      then K.n <= r by A32,XXREAL_2:def 1;
      hence contradiction by A38;
    end;
  end;
  for n,m be Nat st m <= n holds K.m <= K.n
  proof
    let n,m be Nat;
A39: n in NAT by ORDINAL1:def 12;
A40: m in NAT by ORDINAL1:def 12;
    dom(G.m) = EE by A14;
    then
A41: K.m = ( m)*M.EE by A29,A40;
    dom(G.n) = EE by A14;
    then
A42: K.n = ( n)*M.EE by A29,A39;
    assume m <= n;
    hence thesis by A30,A41,A42,XXREAL_3:71;
  end;
  then
A43: K is non-decreasing by RINFSUP2:7;
  then
A44: lim K = sup K by RINFSUP2:37;
A45: for x be Element of X st x in dom(f|EE) holds G#x is convergent & lim(G#
  x) = (f|EE).x
  proof
    let x be Element of X;
    assume
A46: x in dom(f|EE);
    then
A47: x in EE by A1,RELAT_1:62,XBOOLE_1:17;
    then x in eq_dom(f,+infty) by XBOOLE_0:def 4;
    then f.x = +infty by MESFUNC1:def 15;
    then
A48: (f|EE).x = +infty by A47,FUNCT_1:49;
A49: rng(G#x) is not bounded_above
    proof
      assume rng(G#x) is bounded_above;
      then consider UB be Real such that
A50:  UB is UpperBound of rng(G#x) by XXREAL_2:def 10;
      reconsider r = UB as Real;
      consider n be Nat such that
A51:  r < n by SEQ_4:3;
      x in dom(G.n) by A14,A47;
      then (G.n).x = n by A14;
      then
A52:  UB < (G#x).n by A51,MESFUNC5:def 13;
A53:   n in NAT by ORDINAL1:def 12;
      dom(G#x) = NAT by FUNCT_2:def 1;
      then (G#x).n in rng(G#x) by FUNCT_1:3,A53;
      hence contradiction by A52,A50,XXREAL_2:def 1;
    end;
    for n,m be Nat st m<=n holds (G#x).m <= (G#x).n
    proof
      let n,m be Nat;
      dom(G.n) = EE by A14;
      then
A54:  (G.n).x = n by A22,A14,A46;
      dom(G.m) = EE by A14;
      then (G.m).x = m by A22,A14,A46;
      then
A55:  (G#x).m = m by MESFUNC5:def 13;
      assume m <= n;
      hence thesis by A54,A55,MESFUNC5:def 13;
    end;
    then
A56: G#x is non-decreasing by RINFSUP2:7;
    sup rng(G#x) is UpperBound of rng(G#x) by XXREAL_2:def 3;
    then sup(G#x) = +infty by A49,XXREAL_2:53;
    hence thesis by A56,A48,RINFSUP2:37;
  end;
  sup rng K is UpperBound of rng K by XXREAL_2:def 3;
  then
A57: sup K = +infty by A31,XXREAL_2:53;
  K is convergent by A43,RINFSUP2:37;
  then integral+(M,f|EE) = +infty by A10,A22,A9,A27,A19,A23,A45,A21,A44,A57,
MESFUNC5:def 15;
  then Integral(M,f|E) = +infty by A7,XXREAL_0:4;
  hence thesis by A1;
end;

reconsider jj=1 as Real;

theorem
  Integral(M,chi(E,X)) = M.E & Integral(M,(chi(E,X))|E) = M.E
proof
  reconsider XX = X as Element of S by MEASURE1:7;
  set F = XX \ E;
A1: now
    let x be Element of X;
    assume
A2: x in dom(max- chi(E,X));
    per cases;
    suppose
      x in E;
      then chi(E,X).x = 1 by FUNCT_3:def 3;
      then max(-(chi(E,X).x),0.) = 0. by XXREAL_0:def 10;
      hence (max-(chi(E,X))).x = 0 by A2,MESFUNC2:def 3;
    end;
    suppose
      not x in E;
      then chi(E,X).x = 0. by FUNCT_3:def 3;
      then -chi(E,X).x = 0;
      then max(-(chi(E,X).x),0.) = 0;
      hence (max-(chi(E,X))).x = 0 by A2,MESFUNC2:def 3;
    end;
  end;
A3: XX = dom chi(E,X) by FUNCT_3:def 3;
  then
A4: XX = dom(max+(chi(E,X))) by MESFUNC7:23;
A5: XX /\ F = F by XBOOLE_1:28;
  then
A6: dom((max+(chi(E,X)))|F) = F by A4,RELAT_1:61;
A7: now
    let x be Element of X;
    assume
A8: x in dom((max+(chi(E,X)))|F);
    then chi(E,X).x = 0 by A6,FUNCT_3:37;
    then (max+(chi(E,X))).x = 0 by MESFUNC7:23;
    hence ((max+(chi(E,X)))|F).x = 0 by A8,FUNCT_1:47;
  end;
A9: chi(E,X) is XX-measurable by MESFUNC2:29;
  then
A10: max+(chi(E,X)) is XX-measurable by MESFUNC7:23;
  then max+(chi(E,X)) is F-measurable by MESFUNC1:30;
  then
A11: integral+(M,(max+ chi(E,X))|F) = 0 by A4,A5,A6,A7,MESFUNC5:42,87;
A12: XX /\ E = E by XBOOLE_1:28;
  then
A13: dom((max+(chi(E,X)))|E) = E by A4,RELAT_1:61;
  E \/ F = XX by A12,XBOOLE_1:51;
  then
A14: (max+ chi(E,X))|(E\/F) = max+ chi(E,X);
A15: for x be object st x in dom max+(chi(E,X)) holds 0. <= (max+(chi(E,X))).x
  by MESFUNC2:12;
  then
A16: max+(chi(E,X)) is nonnegative by SUPINF_2:52;
  then integral+(M,(max+ chi(E,X))|(E\/F)) = integral+(M,(max+ chi(E,X))|E) +
  integral+(M,(max+ chi(E,X))|F) by A4,A10,MESFUNC5:81,XBOOLE_1:79;
  then
A17: integral+(M,max+ chi(E,X)) = integral+(M,(max+ chi(E,X))|E) by A14,A11,
XXREAL_3:4;
A18: now
    let x be object;
    assume
A19: x in dom((max+(chi(E,X)))|E);
    then chi(E,X).x = 1 by A13,FUNCT_3:def 3;
    then (max+(chi(E,X))).x = 1 by MESFUNC7:23;
    hence ((max+(chi(E,X)))|E).x = 1 by A19,FUNCT_1:47;
  end;
  then (max+(chi(E,X)))|E is_simple_func_in S by A13,MESFUNC6:2;
  then integral+(M,max+ chi(E,X)) = integral'(M,(max+ chi(E,X))|E) by A16,A17,
MESFUNC5:15,77;
  then
A20: integral+(M,max+ chi(E,X)) =  jj * M.(dom((max+(chi(E,X)))|E))
   by A13,A18,MESFUNC5:104;
  max+(chi(E,X)) is E-measurable by A10,MESFUNC1:30;
  then (max+(chi(E,X)))|E is E-measurable by A4,A12,MESFUNC5:42;
  then
A21: (chi(E,X))|E is E-measurable by MESFUNC7:23;
  (max+(chi(E,X)))|E is nonnegative by A15,MESFUNC5:15,SUPINF_2:52;
  then
A22: (chi(E,X))|E is nonnegative by MESFUNC7:23;
  E = dom((chi(E,X))|E) by A13,MESFUNC7:23;
  then
A23: Integral(M,(chi(E,X))|E) =integral+(M,(chi(E,X))|E) by A21,A22,MESFUNC5:88
;
  XX = dom(max- chi(E,X)) by A3,MESFUNC2:def 3;
  then integral+(M,max- chi(E,X)) = 0 by A3,A9,A1,MESFUNC2:26,MESFUNC5:87;
  then Integral(M,chi(E,X)) =  1 * M.E by A13,A20,XXREAL_3:15;
  hence Integral(M,chi(E,X)) = M.E by XXREAL_3:81;
  (chi(E,X))|E = (max+ chi(E,X))|E by MESFUNC7:23;
  hence thesis by A13,A17,A20,A23,XXREAL_3:81;
end;

theorem Th15:
  E c= dom f & E c= dom g & f is E-measurable & g
is E-measurable & f is nonnegative & (for x be Element of X st x in E holds
  f.x <= g.x) implies Integral(M,f|E) <= Integral(M,g|E)
proof
  assume that
A1: E c= dom f and
A2: E c= dom g and
A3: f is E-measurable and
A4: g is E-measurable and
A5: f is nonnegative and
A6: for x be Element of X st x in E holds f.x <= g.x;
  set F2 = g|E;
A7: E = dom(f|E) by A1,RELAT_1:62;
  set F1 = f|E;
A8: F1 is nonnegative by A5,MESFUNC5:15;
A9: E = dom(g|E) by A2,RELAT_1:62;
A10: for x be Element of X st x in dom F1 holds F1.x <= F2.x
  proof
    let x be Element of X;
    assume
A11: x in dom F1;
    then
A12: F1.x = f.x by FUNCT_1:47;
    F2.x = g.x by A7,A9,A11,FUNCT_1:47;
    hence thesis by A6,A7,A11,A12;
  end;
  for x be object st x in dom F2 holds 0 <= F2.x
  proof
    let x be object;
    assume
A13: x in dom F2;
    0 <= F1.x by A8,SUPINF_2:51;
    hence thesis by A7,A9,A10,A13;
  end;
  then
A14: F2 is nonnegative by SUPINF_2:52;
A15: dom g /\ E = E by A2,XBOOLE_1:28;
  then
A16: F2 is E-measurable by A4,MESFUNC5:42;
A17: dom f /\ E = E by A1,XBOOLE_1:28;
  then F1 is E-measurable by A3,MESFUNC5:42;
  then integral+(M,F1) <= integral+(M,F2) by A8,A7,A9,A10,A14,A16,MESFUNC5:85;
  then Integral(M,F1) <= integral+(M,F2) by A3,A8,A7,A17,MESFUNC5:42,88;
  hence thesis by A4,A9,A14,A15,MESFUNC5:42,88;
end;

begin :: Selected Properties of Extended Real Sequence

definition
  let s be ext-real-valued Function;
  func Partial_Sums s -> ExtREAL_sequence means
  :Def1:
  it.0=s.0 & for n be Nat holds it.(n+1) = it.n + s.(n+1);
  existence
  proof
    deffunc U(Nat,R_eal) = $2 + s.($1+1);
    consider f being sequence of ExtREAL such that
A1: f.0 = s.0 & for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1:
    sch 12;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let s1,s2 be ExtREAL_sequence;
    assume that
A2: s1.0=s.0 and
A3: for n be Nat holds s1.(n+1)=s1.n + s.(n+1) and
A4: s2.0=s.0 and
A5: for n be Nat holds s2.(n+1)=s2.n + s.(n+1);
    defpred X[Nat] means s1.$1 = s2.$1;
A6: for k be Nat st X[k] holds X[k+1]
    proof
      let k be Nat;
      assume s1.k =s2.k;
      hence s1.(k+1) = s2.k + s.(k+1) by A3
        .= s2.(k+1) by A5;
    end;
A7: X[ 0 ] by A2,A4;
    for n be Nat holds X[n] from NAT_1:sch 2(A7,A6);
    hence s1 = s2;
  end;
end;

definition
  let s be ext-real-valued Function;
  attr s is summable means
  Partial_Sums s is convergent;
end;

definition
  let s be ext-real-valued Function;
  func Sum s -> R_eal equals
  lim Partial_Sums s;
  correctness;
end;

theorem Th16:
  seq is nonnegative implies Partial_Sums seq is nonnegative &
  Partial_Sums seq is non-decreasing
proof
  set PS = Partial_Sums seq;
  defpred P[Nat] means 0 <= PS.$1;
  assume
A1: seq is nonnegative;
A2: for k be Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A3: P[k];
A4: PS.(k+1) = PS.k + seq.(k+1) by Def1;
    seq.(k+1) >= 0 by A1,SUPINF_2:51;
    hence thesis by A3,A4;
  end;
  PS.0 = seq.0 by Def1;
  then
A5: P[ 0 ] by A1,SUPINF_2:51;
  for m be Nat holds P[m] from NAT_1:sch 2(A5,A2);
  then for k be object st k in dom PS holds 0 <= PS.k;
  hence PS is nonnegative by SUPINF_2:52;
  for n,m be Nat st m <= n holds (Partial_Sums seq).m <= (
  Partial_Sums seq).n
  proof
    let n,m be Nat;
    reconsider m1=m as Nat;
    defpred Q[Nat] means PS.m1 <= PS.$1;
A6: for k be Nat holds PS.k <= PS.(k+1)
    proof
      let k be Nat;
A7:   0 <= seq.(k+1) by A1,SUPINF_2:51;
      PS.(k+1) = PS.k + seq.(k+1) by Def1;
      hence thesis by A7,XXREAL_3:39;
    end;
A8: for k be Nat st k >= m1 & (for l be Nat st l >= m1 & l < k holds Q[l])
    holds Q[k]
    proof
      let k be Nat;
      assume that
A9:   k >= m1 and
A10:  for l be Nat st l >= m1 & l < k holds Q[l];
      now
        assume k > m1;
        then
A11:    k >= m1 + 1 by NAT_1:13;
        per cases by A11,XXREAL_0:1;
        suppose
          k = m1 + 1;
          hence thesis by A6;
        end;
        suppose
A12:      k > m1 + 1;
          then reconsider l = k-1 as Element of NAT by NAT_1:20;
          k < k+1 by NAT_1:13;
          then
A13:      k > l by XREAL_1:19;
          k = l+1;
          then
A14:      PS.l <= PS.k by A6;
          l >= m1 by A12,XREAL_1:19;
          then PS.m1 <= PS.l by A10,A13;
          hence thesis by A14,XXREAL_0:2;
        end;
      end;
      hence thesis by A9,XXREAL_0:1;
    end;
A15: for k be Nat st k >= m1 holds Q[k] from NAT_1:sch 9(A8);
    assume m <= n;
    hence thesis by A15;
  end;
  hence thesis by RINFSUP2:7;
end;

theorem
  (for n be Nat holds 0 < seq.n) implies for m be Nat holds 0 < (
  Partial_Sums seq).m
proof
  defpred P[Nat] means 0 < (Partial_Sums seq).$1;
  assume
A1: for n be Nat holds 0 < seq.n;
A2: for k be Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A3: P[k];
A4: (Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1) by Def1;
    seq.(k+1) > 0 by A1;
    hence thesis by A3,A4;
  end;
  (Partial_Sums seq).0 = seq.0 by Def1;
  then
A5: P[ 0 ] by A1;
  thus for m be Nat holds P[m] from NAT_1:sch 2(A5,A2);
end;

theorem Th18:
  F is with_the_same_dom & (for n be Nat holds G.n = (F.n)|D)
  implies G is with_the_same_dom
proof
  assume that
A1: F is with_the_same_dom and
A2: for n be Nat holds G.n = (F.n)|D;
  let n,m be Nat;
  G.m = (F.m)|D by A2;
  then
A3: dom(G.m) = dom(F.m) /\ D by RELAT_1:61;
  G.n = (F.n)|D by A2;
  then dom(G.n) = dom(F.n) /\ D by RELAT_1:61;
  hence thesis by A1,A3;
end;

theorem Th19:
  D c= dom(F.0) & (for n be Nat holds G.n = (F.n)|D) & (for x be
  Element of X st x in D holds F#x is convergent) implies (lim F)|D = lim G
proof
  assume that
A1: D c= dom(F.0) and
A2: for n be Nat holds G.n = (F.n)|D and
A3: for x be Element of X st x in D holds F#x is convergent;
  G.0 = (F.0)|D by A2;
  then
A4: dom(G.0) = D by A1,RELAT_1:62;
A5: dom((lim F)|D) = dom(lim F) /\ D by RELAT_1:61;
  then dom((lim F)|D) = dom(F.0) /\ D by MESFUNC8:def 9;
  then dom((lim F)|D) = D by A1,XBOOLE_1:28;
  then
A6: dom((lim F)|D) = dom(lim G) by A4,MESFUNC8:def 9;
  now
    let x be Element of X;
    assume
A7: x in dom((lim F)|D);
    then
A8: ((lim F)|D).x = (lim F).x by FUNCT_1:47;
    x in dom(lim F) by A5,A7,XBOOLE_0:def 4;
    then
A9: ((lim F)|D).x = lim(F#x) by A8,MESFUNC8:def 9;
A10: x in D by A7,RELAT_1:57;
    then
A11: F#x is convergent by A3;
    per cases by A11;
    suppose
A12:  F#x is convergent_to_+infty;
      then G#x is convergent_to_+infty by A2,A10,Th12;
      then lim(G#x) = +infty by Th7;
      then (lim G).x = +infty by A6,A7,MESFUNC8:def 9;
      hence (lim G).x = ((lim F)|D).x by A9,A12,Th7;
    end;
    suppose
A13:  F#x is convergent_to_-infty;
      then G#x is convergent_to_-infty by A2,A10,Th12;
      then lim(G#x) = -infty by Th7;
      then (lim G).x = -infty by A6,A7,MESFUNC8:def 9;
      hence (lim G).x = ((lim F)|D).x by A9,A13,Th7;
    end;
    suppose
A14:  F#x is convergent_to_finite_number;
      then consider g be Real such that
A15:  lim(F#x) = g and
A16:  for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
      holds |. (F#x).m - lim(F#x) .| < p by Th7;
A17:  now
        let p be Real;
        assume 0 < p;
        then consider n be Nat such that
A18:    for m be Nat st n <= m holds |. (F#x).m - lim(F#x) .| < p by A16;
        take n;
        let m be Nat;
        (F#x).m = (F.m).x by MESFUNC5:def 13;
        then (F#x).m = ((F.m)|D).x by A10,FUNCT_1:49;
        then
A19:    (F#x).m = (G.m).x by A2;
        assume n <= m;
        then |. (F#x).m - lim(F#x) .| < p by A18;
        hence |. (G#x).m -  g .| < p by A15,A19,MESFUNC5:def 13;
      end;
      reconsider g as R_eal by XXREAL_0:def 1;
A20:  G#x is convergent_to_finite_number by A2,A10,A14,Th12;
      then G#x is convergent;
      then lim(G#x) = g by A17,A20,MESFUNC5:def 12;
      hence (lim G).x = ((lim F)|D).x by A6,A7,A9,A15,MESFUNC8:def 9;
    end;
  end;
  hence thesis by A6,PARTFUN1:5;
end;

theorem Th20:
  F is with_the_same_dom & E c= dom(F.0) & (for m be Nat holds F.m
  is E-measurable & G.m= (F.m)|E) implies G.n is E-measurable
proof
  assume that
A1: F is with_the_same_dom and
A2: E c= dom(F.0) and
A3: for m be Nat holds F.m is E-measurable & G.m= (F.m)|E;
  dom(F.n) = dom(F.0) by A1;
  then dom(F.n) /\ E = E by A2,XBOOLE_1:28;
  then (F.n)|E is E-measurable by A3,MESFUNC5:42;
  hence thesis by A3;
end;

theorem Th21:
  E c= dom(F.0) & G is with_the_same_dom & (for x be Element of X
  st x in E holds F#x is summable) & (for n be Nat holds G.n= (F.n)|E) implies
  for x be Element of X st x in E holds G#x is summable
proof
  assume that
A1: E c= dom(F.0) and
A2: G is with_the_same_dom and
A3: for x be Element of X st x in E holds F#x is summable and
A4: for n be Nat holds G.n= (F.n)|E;
  let x be Element of X;
  assume
A5: x in E;
  dom((F.0)|E) = E by A1,RELAT_1:62;
  then
A6: E = dom(G.0) by A4;
  for n be Element of NAT holds (F#x).n = (G#x).n
  proof
    let n be Element of NAT;
    dom(G.n) = E by A2,A6;
    then x in dom((F.n)|E) by A4,A5;
    then ((F.n)|E).x = (F.n).x by FUNCT_1:47;
    then
A7: (G.n).x = (F.n).x by A4;
    (F#x).n = (F.n).x by MESFUNC5:def 13;
    hence thesis by A7,MESFUNC5:def 13;
  end;
  then
A8: Partial_Sums(F#x) = Partial_Sums(G#x) by FUNCT_2:63;
  F#x is summable by A3,A5;
  then Partial_Sums(F#x) is convergent;
  hence thesis by A8;
end;

begin :: Partial Sums of Functional Sequence and their Properties

definition
  let X be non empty set, F be Functional_Sequence of X,ExtREAL;
  func Partial_Sums F -> Functional_Sequence of X,ExtREAL means
  :Def4:
  it.0 = F.0 & for n be Nat holds it.(n+1) = it.n + F.(n+1);
  existence
  proof
    defpred P[Nat,set,set] means (not $2 is PartFunc of X,ExtREAL &
$3 = F.$1) or ($2 is PartFunc of X,ExtREAL & for F2 be PartFunc of X,ExtREAL st
    F2 = $2 holds $3 = F2 + F.($1+1));
A1: for n being Nat for x being set ex y being set st P[n,x,y]
    proof
      let n be Nat;
      let x be set;
      thus ex y be set st P[n,x,y]
      proof
        per cases;
        suppose
A2:       not x is PartFunc of X,ExtREAL;
          take y = F.n;
          thus not x is PartFunc of X,ExtREAL & y = F.n or (x is PartFunc of X
,ExtREAL & for F2 be PartFunc of X,ExtREAL st F2 = x holds y = F2 + F.(n+1))
by A2;
        end;
        suppose
          x is PartFunc of X,ExtREAL;
          then reconsider G2 = x as PartFunc of X,ExtREAL;
          take y = G2 + F.(n+1);
          thus not x is PartFunc of X,ExtREAL & y = F.n or (x is PartFunc of X
,ExtREAL & for F2 be PartFunc of X,ExtREAL st F2 = x holds y = F2 + F.(n+1));
        end;
      end;
    end;
    consider IT being Function such that
A3: dom IT = NAT & IT.0 = F.0 & for n being Nat holds P[n,
    IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
    now
      defpred IND[Nat] means IT.$1 is PartFunc of X,ExtREAL;
      let f be object;
      assume f in rng IT;
      then consider m be object such that
A4:   m in dom IT and
A5:   f = IT.m by FUNCT_1:def 3;
      reconsider m as Element of NAT by A3,A4;
A6:   for n be Nat st IND[n] holds IND[n+1]
      proof
        let n be Nat;
        assume IND[n];
        then reconsider F2 = IT.n as PartFunc of X,ExtREAL;
        IT.(n+1) = F2 + F.(n+1) by A3;
        hence thesis;
      end;
A7:   IND[ 0 ] by A3;
      for n be Nat holds IND[n] from NAT_1:sch 2(A7,A6);
      then IT.m is PartFunc of X,ExtREAL;
      hence f in PFuncs(X,ExtREAL) by A5,PARTFUN1:45;
    end;
    then rng IT c= PFuncs(X,ExtREAL);
    then reconsider IT as Functional_Sequence of X,ExtREAL by A3,FUNCT_2:def 1
,RELSET_1:4;
    take IT;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let PS1,PS2 be Functional_Sequence of X,ExtREAL;
    assume that
A8: PS1.0 = F.0 and
A9: for n be Nat holds PS1.(n+1) = PS1.n + F.(n+1) and
A10: PS2.0 = F.0 and
A11: for n be Nat holds PS2.(n+1) = PS2.n + F.(n+1);
    defpred IND[Nat] means PS1.$1 = PS2.$1;
A12: for n be Nat st IND[n] holds IND[n+1]
    proof
      let n be Nat;
      assume
A13:  IND[n];
      PS1.(n+1) = PS1.n + F.(n+1) by A9;
      hence thesis by A11,A13;
    end;
A14: IND[ 0 ] by A8,A10;
    for n be Nat holds IND[n] from NAT_1:sch 2(A14,A12);
    then for m be Element of NAT holds PS1.m = PS2.m;
    hence thesis;
  end;
end;

definition
  let X be set, F be Functional_Sequence of X,ExtREAL;
  attr F is additive means

  for n,m be Nat st n <> m holds for x be set
  st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or (F.m).x <> -infty;
end;

Lm1: z in dom((Partial_Sums F).n) & m <= n implies z in dom((Partial_Sums F).m
)
proof
  set PF = Partial_Sums F;
  assume that
A1: z in dom(PF.n) and
A2: m <= n;
  defpred P[Nat] means m <= $1 & $1 <= n implies not z in dom(PF.$1);
  assume
A3: not z in dom(PF.m);
A4: for k be Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A5: P[k];
    assume that
A6: m <= k+1 and
A7: k+1 <= n;
    per cases by A6,NAT_1:8;
    suppose
A8:   m <= k;
      PF.(k+1) = PF.k + F.(k+1) by Def4;
      then
A9:   dom(PF.(k+1)) = (dom(PF.k) /\ dom(F.(k+1))) \(((PF.k)"{-infty} /\ (
F.(k+1))"{+infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty})) by
MESFUNC1:def 3;
      not z in dom(PF.k) /\ dom(F.(k+1)) by A5,A7,A8,NAT_1:13,XBOOLE_0:def 4;
      hence thesis by A9,XBOOLE_0:def 5;
    end;
    suppose
      m = k+1;
      hence thesis by A3;
    end;
  end;
A10: P[ 0 ] by A3;
  for k be Nat holds P[k] from NAT_1:sch 2(A10,A4);
  hence contradiction by A1,A2;
end;

theorem Th22:
  z in dom((Partial_Sums F).n) & m <= n implies z in dom((
  Partial_Sums F).m) & z in dom(F.m)
proof
  set PF = Partial_Sums F;
  assume that
A1: z in dom(PF.n) and
A2: m <= n;
  thus
A3: z in dom(PF.m) by A1,A2,Lm1;
  per cases;
  suppose
    m = 0;
    then PF.m = F.m by Def4;
    hence thesis by A1,A2,Lm1;
  end;
  suppose
    m <> 0;
    then consider k be Nat such that
A4: m = k + 1 by NAT_1:6;
    PF.m = PF.k + F.m by A4,Def4;
    then dom(PF.m) = (dom(PF.k) /\ dom(F.m)) \(((PF.k)"{-infty} /\ (F.m)"{
    +infty}) \/ ((PF.k)"{+infty} /\ (F.m)"{-infty})) by MESFUNC1:def 3;
    then z in dom(PF.k) /\ dom(F.m) by A3,XBOOLE_0:def 5;
    hence thesis by XBOOLE_0:def 4;
  end;
end;

theorem Th23:
  z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = +infty
  implies ex m be Nat st m <= n & (F.m).z = +infty
proof
  set PF = Partial_Sums F;
  assume that
A1: z in dom(PF.n) and
A2: (PF.n).z = +infty;
  now
    defpred P[Nat] means $1 <= n implies (PF.$1).z <> +infty;
    assume
A3: for m be Element of NAT st m <= n holds (F.m).z <> +infty;
A4: for k being Nat st P[k] holds P[k + 1]
    proof
      let k be Nat;
      assume
A5:   P[k];
      assume
A6:   k+1 <= n;
      then k <= n by NAT_1:13;
      then
A7:   z in dom(PF.k) by A1,Th22;
      not (PF.k).z in {+infty} by A5,A6,NAT_1:13,TARSKI:def 1;
      then not z in (PF.k)"{+infty} by FUNCT_1:def 7;
      then
A8:   not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} by XBOOLE_0:def 4;
      z in dom(F.(k+1)) by A1,A6,Th22;
      then
A9:   z in dom(PF.k) /\ dom(F.(k+1)) by A7,XBOOLE_0:def 4;
A10:  PF.(k+1) = PF.k + F.(k+1) by Def4;
A11:  (F.(k+1)).z <> +infty by A3,A6;
      then not (F.(k+1)).z in {+infty} by TARSKI:def 1;
      then not z in (F.(k+1))"{+infty} by FUNCT_1:def 7;
      then not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} by XBOOLE_0:def 4;
      then
      not z in ((PF.k)"{+infty} /\ (F.(k+1))"{-infty}) \/ ((PF.k)"{-infty
      } /\ (F.(k+1))"{+infty}) by A8,XBOOLE_0:def 3;
      then
      z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{+infty} /\ (F.(k+1))"{
-infty}) \/ ((PF.k)"{-infty} /\ (F.(k+1))"{+infty})) by A9,XBOOLE_0:def 5;
      then z in dom(PF.(k+1)) by A10,MESFUNC1:def 3;
      then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by A10,MESFUNC1:def 3;
      hence thesis by A5,A6,A11,NAT_1:13,XXREAL_3:16;
    end;
    PF.0 = F.0 by Def4;
    then
A12: P[ 0 ] by A3;
    for k being Nat holds P[k] from NAT_1:sch 2(A12,A4);
    hence contradiction by A2;
  end;
  hence thesis;
end;

theorem
  F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z
  = +infty & m <= n implies (F.m).z <> -infty
proof
  assume that
A1: F is additive and
A2: z in dom((Partial_Sums F).n) and
A3: ((Partial_Sums F).n).z = +infty and
A4: m <= n;
A5: z in dom(F.m) by A2,A4,Th22;
  consider k be Nat such that
A6: k <= n and
A7: (F.k).z = +infty by A2,A3,Th23;
  z in dom(F.k) by A2,A6,Th22;
  then z in dom(F.m) /\ dom(F.k) by A5,XBOOLE_0:def 4;
  hence thesis by A1,A7;
end;

theorem Th25:
  z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = -infty
  implies ex m be Nat st m <= n & (F.m).z = -infty
proof
  set PF = Partial_Sums F;
  assume that
A1: z in dom(PF.n) and
A2: (PF.n).z = -infty;
  now
    defpred P[Nat] means $1 <= n implies (PF.$1).z <> -infty;
    assume
A3: for m be Nat st m <= n holds (F.m).z <> -infty;
A4: for k being Nat st P[k] holds P[k + 1]
    proof
      let k be Nat;
      assume
A5:   P[k];
      assume
A6:   k+1 <= n;
      then k <= n by NAT_1:13;
      then
A7:   z in dom(PF.k) by A1,Th22;
      not (PF.k).z in {-infty} by A5,A6,NAT_1:13,TARSKI:def 1;
      then not z in (PF.k)"{-infty} by FUNCT_1:def 7;
      then
A8:   not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} by XBOOLE_0:def 4;
      z in dom(F.(k+1)) by A1,A6,Th22;
      then
A9:   z in dom(PF.k) /\ dom(F.(k+1)) by A7,XBOOLE_0:def 4;
A10:  PF.(k+1) = PF.k + F.(k+1) by Def4;
A11:  (F.(k+1)).z <> -infty by A3,A6;
      then not (F.(k+1)).z in {-infty} by TARSKI:def 1;
      then not z in (F.(k+1))"{-infty} by FUNCT_1:def 7;
      then not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} by XBOOLE_0:def 4;
      then
      not z in ((PF.k)"{-infty} /\ (F.(k+1))"{+infty}) \/ ((PF.k)"{+infty
      } /\ (F.(k+1))"{-infty}) by A8,XBOOLE_0:def 3;
      then
      z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{-infty} /\ (F.(k+1))"{
+infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty})) by A9,XBOOLE_0:def 5;
      then z in dom(PF.(k+1)) by A10,MESFUNC1:def 3;
      then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by A10,MESFUNC1:def 3;
      hence thesis by A5,A6,A11,NAT_1:13,XXREAL_3:17;
    end;
    PF.0 = F.0 by Def4;
    then
A12: P[ 0 ] by A3;
    for k being Nat holds P[k] from NAT_1:sch 2(A12,A4);
    hence contradiction by A2;
  end;
  hence thesis;
end;

theorem
  F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z
  = -infty & m <= n implies (F.m).z <> +infty
proof
  assume
A1: F is additive;
  assume that
A2: z in dom((Partial_Sums F).n) and
A3: ((Partial_Sums F).n).z = -infty;
  assume m <= n;
  then
A4: z in dom(F.m) by A2,Th22;
  consider k be Nat such that
A5: k <= n and
A6: (F.k).z = -infty by A2,A3,Th25;
  z in dom(F.k) by A2,A5,Th22;
  then z in dom(F.m) /\ dom(F.k) by A4,XBOOLE_0:def 4;
  hence thesis by A1,A6;
end;

theorem Th27:
  F is additive implies ((Partial_Sums F).n)"{-infty} /\ (F.(n+1))
  "{+infty} = {} & ((Partial_Sums F).n)"{+infty} /\ (F.(n+1))"{-infty} = {}
proof
  set PF = Partial_Sums F;
  assume
A1: F is additive;
  now
    given z be object such that
A2: z in (PF.n)"{-infty} and
A3: z in (F.(n+1))"{+infty};
A4: z in dom(PF.n) by A2,FUNCT_1:def 7;
    (PF.n).z in {-infty} by A2,FUNCT_1:def 7;
    then (PF.n).z = -infty by TARSKI:def 1;
    then consider k be Nat such that
A5: k <= n and
A6: (F.k).z = -infty by A4,Th25;
A7: z in dom(F.(n+1)) by A3,FUNCT_1:def 7;
    (F.(n+1)).z in {+infty} by A3,FUNCT_1:def 7;
    then
A8: (F.(n+1)).z = +infty by TARSKI:def 1;
    z in dom(F.k) by A4,A5,Th22;
    then z in dom(F.k) /\ dom(F.(n+1)) by A7,XBOOLE_0:def 4;
    hence contradiction by A1,A8,A6;
  end;
  then (PF.n)"{-infty} misses (F.(n+1))"{+infty} by XBOOLE_0:3;
  hence (PF.n)"{-infty} /\ (F.(n+1))"{+infty} = {} by XBOOLE_0:def 7;
  now
    given z be object such that
A9: z in (PF.n)"{+infty} and
A10: z in (F.(n+1))"{-infty};
A11: z in dom(PF.n) by A9,FUNCT_1:def 7;
    (PF.n).z in {+infty} by A9,FUNCT_1:def 7;
    then (PF.n).z = +infty by TARSKI:def 1;
    then consider k be Nat such that
A12: k <= n and
A13: (F.k).z = +infty by A11,Th23;
A14: z in dom(F.(n+1)) by A10,FUNCT_1:def 7;
    (F.(n+1)).z in {-infty} by A10,FUNCT_1:def 7;
    then
A15: (F.(n+1)).z = -infty by TARSKI:def 1;
    z in dom(F.k) by A11,A12,Th22;
    then z in dom(F.k) /\ dom(F.(n+1)) by A14,XBOOLE_0:def 4;
    hence contradiction by A1,A15,A13;
  end;
  then (PF.n)"{+infty} misses (F.(n+1))"{-infty} by XBOOLE_0:3;
  hence thesis by XBOOLE_0:def 7;
end;

theorem Th28:
  F is additive implies dom((Partial_Sums F).n) = meet{dom(F.k)
  where k is Element of NAT : k <= n}
proof
  deffunc DOM1(Nat) = {dom(F.k) where k is Element of NAT : k <= $1};
  set PF = Partial_Sums F;
  defpred P[Nat] means dom(PF.$1) = meet {dom(F.k) where k is Element of NAT :
  k <= $1};
A1: dom(PF.0) = dom(F.0) by Def4;
  now
    let V be object;
    assume V in DOM1(0);
    then consider k be Element of NAT such that
A2: V = dom(F.k) and
A3: k <= 0;
    k = 0 by A3;
    hence V in {dom(F.0)} by A2,TARSKI:def 1;
  end;
  then
A4: DOM1(0) c= {dom(F.0)};
  assume
A5: F is additive;
A6: for m be Nat st P[m] holds P[m+1]
  proof
    let m be Nat;
A7: PF.(m+1) = PF.m + F.(m+1) by Def4;
A8: (PF.m)"{+infty} /\ (F.(m+1))"{-infty} = {} by A5,Th27;
A9: dom(F.0) in DOM1(m+1);
    now
      let V be object;
      assume
A10:  V in meet DOM1(m) /\ dom(F.(m+1));
      then
A11:  V in dom(F.(m+1)) by XBOOLE_0:def 4;
A12:  V in meet DOM1(m) by A10,XBOOLE_0:def 4;
      for W be set holds W in DOM1(m+1) implies V in W
      proof
        let W be set;
        assume W in DOM1(m+1);
        then consider i be Element of NAT such that
A13:    W = dom(F.i) and
A14:    i <= m+1;
        now
          assume i <= m;
          then W in DOM1(m) by A13;
          hence thesis by A12,SETFAM_1:def 1;
        end;
        hence thesis by A11,A13,A14,NAT_1:8;
      end;
      hence V in meet DOM1(m+1) by A9,SETFAM_1:def 1;
    end;
    then
A15: meet DOM1(m) /\ dom(F.(m+1)) c= meet DOM1(m+1);
A16: dom(F.0) in DOM1(m);
    now
      now
        let V be object;
        assume V in DOM1(m);
        then consider i be Element of NAT such that
A17:    V = dom(F.i) and
A18:    i <= m;
        i <= m+1 by A18,NAT_1:12;
        hence V in DOM1(m+1) by A17;
      end;
      then DOM1(m) c= DOM1(m+1);
      then
A19:  meet DOM1(m+1) c= meet DOM1(m) by A16,SETFAM_1:6;
      let V be object;
      assume
A20:  V in meet DOM1(m+1);
      dom(F.(m+1)) in DOM1(m+1);
      then V in dom(F.(m+1)) by A20,SETFAM_1:def 1;
      hence V in meet DOM1(m) /\ dom(F.(m+1)) by A20,A19,XBOOLE_0:def 4;
    end;
    then
A21: meet DOM1(m+1) c= meet DOM1(m) /\ dom(F.(m+1));
    (PF.m)"{-infty} /\ (F.(m+1))"{+infty} = {} by A5,Th27;
    then
A22: dom(PF.(m+1)) = (dom(PF.m)/\dom(F.(m+1))) \ ({}\/{}) by A8,A7,
MESFUNC1:def 3;
    assume P[m];
    hence thesis by A22,A21,A15,XBOOLE_0:def 10;
  end;
  now
    let V be object;
    assume V in {dom(F.0)};
    then V = dom(F.0) by TARSKI:def 1;
    hence V in DOM1(0);
  end;
  then {dom(F.0)} c= DOM1(0);
  then DOM1(0) = {dom(F.0)} by A4,XBOOLE_0:def 10;
  then
A23: P[ 0 ] by A1,SETFAM_1:10;
  for k be Nat holds P[k] from NAT_1:sch 2(A23,A6);
  hence thesis;
end;

theorem Th29:
  F is additive & F is with_the_same_dom implies dom((Partial_Sums
  F).n) = dom(F.0)
proof
  assume that
A1: F is additive and
A2: F is with_the_same_dom;
  now
    let D be object;
A3: dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n};
    assume D in meet {dom(F.k) where k is Element of NAT : k <= n};
    then D in dom(F.0) by A3,SETFAM_1:def 1;
    hence D in meet {dom(F.0)} by SETFAM_1:10;
  end;
  then
A4: meet{dom(F.k) where k is Element of NAT : k <= n} c= meet{dom(F.0)};
  now
    let D be object;
    assume D in meet {dom(F.0)};
    then
A5: D in dom(F.0) by SETFAM_1:10;
A6: for E be set holds E in {dom(F.k) where k is Element of NAT : k <= n}
    implies D in E
    proof
      let E be set;
      assume E in {dom(F.k) where k is Element of NAT : k <= n};
      then ex k1 be Element of NAT st E = dom(F.k1) & k1 <= n;
      hence thesis by A2,A5;
    end;
    dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n};
    hence D in meet {dom(F.k) where k is Element of NAT : k <= n} by A6,
SETFAM_1:def 1;
  end;
  then
  meet{dom(F.0)} c= meet {dom(F.k) where k is Element of NAT : k <= n};
  then meet{dom(F.k) where k is Element of NAT : k <= n} = meet {dom(F.0)} by
A4,XBOOLE_0:def 10;
  then dom((Partial_Sums F).n) = meet{dom(F.0)} by A1,Th28;
  hence thesis by SETFAM_1:10;
end;

theorem Th30:
  (for n be Nat holds F.n is nonnegative) implies F is additive
by SUPINF_2:51;

theorem Th31:
  F is additive & (for n holds G.n = (F.n)|D) implies G is additive
proof
  assume that
A1: F is additive and
A2: for n holds G.n = (F.n)|D;
  let n,m be Nat;
A3: G.m = (F.m)|D by A2;
  then
A4: dom(G.m) c= dom(F.m) by RELAT_1:60;
  assume n <> m;
  let x be set;
  assume
A5: x in dom(G.n) /\ dom(G.m);
  then
A6: x in dom(G.m) by XBOOLE_0:def 4;
A7: G.n = (F.n)|D by A2;
  then dom(G.n) c= dom(F.n) by RELAT_1:60;
  then dom(G.n) /\ dom(G.m) c= dom(F.n) /\ dom(F.m) by A4,XBOOLE_1:27;
  then
A8: (F.n).x <> +infty or (F.m).x <> -infty by A1,A5;
  x in dom(G.n) by A5,XBOOLE_0:def 4;
  hence thesis by A7,A3,A8,A6,FUNCT_1:47;
end;

theorem Th32:
  F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D
  implies (Partial_Sums(F#x)).n = ((Partial_Sums F)#x).n
proof
  set PF = Partial_Sums F;
  set PFx = Partial_Sums(F#x);
  assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: D c= dom(F.0) and
A4: x in D;
  defpred P[Nat] means PFx.$1 = (PF#x).$1;
A5: for k be Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A6: P[k];
    PFx.(k+1) = PFx.k + (F#x).(k+1) by Def1;
    then PFx.(k+1) = (PF#x).k + (F.(k+1)).x by A6,MESFUNC5:def 13;
    then
A7: PFx.(k+1) = (PF.k).x + (F.(k+1)).x by MESFUNC5:def 13;
A8: PF.(k+1) = PF.k + F.(k+1) by Def4;
    D c= dom(PF.(k+1)) by A1,A2,A3,Th29;
    then PFx.(k+1) = (PF.(k+1)).x by A4,A8,A7,MESFUNC1:def 3;
    hence thesis by MESFUNC5:def 13;
  end;
  PFx.0 = (F#x).0 by Def1;
  then PFx.0 = (F.0).x by MESFUNC5:def 13;
  then PFx.0 = (PF.0).x by Def4;
  then
A9: P[ 0 ] by MESFUNC5:def 13;
  for k being Nat holds P[k] from NAT_1:sch 2(A9,A5);
  hence thesis;
end;

theorem Th33:
  F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D
implies ( Partial_Sums(F#x) is convergent_to_finite_number iff (Partial_Sums F)
  #x is convergent_to_finite_number ) & ( Partial_Sums(F#x) is
  convergent_to_+infty iff (Partial_Sums F)#x is convergent_to_+infty ) & (
  Partial_Sums(F#x) is convergent_to_-infty iff (Partial_Sums F)#x is
convergent_to_-infty ) & ( Partial_Sums(F#x) is convergent iff (Partial_Sums F)
  #x is convergent )
proof
  set PFx = Partial_Sums(F#x);
  set PF = Partial_Sums F;
  assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: D c= dom(F.0) and
A4: x in D;
  thus
A5: now
    assume PFx is convergent_to_finite_number;
    then consider g be Real such that
A6: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
    holds |. PFx.m -  g .| < p;
    now
      let p be Real;
      assume 0<p;
      then consider n be Nat such that
A7:   for m be Nat st n<=m holds |. PFx.m -  g .| < p by A6;
      take n;
      let m be Nat;
      assume
A8:   n<=m;
      PFx.m = (PF#x).m by A1,A2,A3,A4,Th32;
      hence |. (PF#x).m -  g .| < p by A7,A8;
    end;
    hence PF#x is convergent_to_finite_number;
  end;
  thus
A9: now
    assume PF#x is convergent_to_finite_number;
    then consider g be Real such that
A10: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
    holds |. (PF#x).m- g .| < p;
    now
      let p be Real;
      assume 0<p;
      then consider n be Nat such that
A11:  for m be Nat st n<=m holds |. (PF#x).m- g .| < p by A10;
      take n;
      let m be Nat;
      assume
A12:  n<=m;
      PFx.m = (PF#x).m by A1,A2,A3,A4,Th32;
      hence |. PFx.m -  g .| < p by A11,A12;
    end;
    hence PFx is convergent_to_finite_number;
  end;
  thus
A13: now
    assume
A14: PFx is convergent_to_+infty;
    now
      let r be Real;
      assume 0 < r;
      then consider n be Nat such that
A15:  for m be Nat st n <= m holds r <= PFx.m by A14;
      take n;
      let m be Nat;
      assume n <= m;
      then r <= PFx.m by A15;
      hence r <= (PF#x).m by A1,A2,A3,A4,Th32;
    end;
    hence PF#x is convergent_to_+infty;
  end;
  thus
A16: now
    assume
A17: PF#x is convergent_to_+infty;
    now
      let r be Real;
      assume 0 < r;
      then consider n be Nat such that
A18:  for m be Nat st n <= m holds r <= (PF#x).m by A17;
      take n;
      let m be Nat;
      assume n <= m;
      then r <= (PF#x).m by A18;
      hence r <= PFx.m by A1,A2,A3,A4,Th32;
    end;
    hence PFx is convergent_to_+infty;
  end;
  thus
A19: now
    assume
A20: PFx is convergent_to_-infty;
    now
      let r be Real;
      assume r < 0;
      then consider n be Nat such that
A21:  for m be Nat st n <= m holds PFx.m <= r by A20;
      take n;
      let m be Nat;
      assume n <= m;
      then PFx.m <= r by A21;
      hence (PF#x).m <= r by A1,A2,A3,A4,Th32;
    end;
    hence PF#x is convergent_to_-infty;
  end;
  thus
A22: now
    assume
A23: PF#x is convergent_to_-infty;
    now
      let r be Real;
      assume r < 0;
      then consider n be Nat such that
A24:  for m be Nat st n <= m holds (PF#x).m <= r by A23;
      take n;
      let m be Nat;
      assume n <= m;
      then (PF#x).m <= r by A24;
      hence PFx.m <= r by A1,A2,A3,A4,Th32;
    end;
    hence PFx is convergent_to_-infty;
  end;
  hereby
    assume
A25: PFx is convergent;
    per cases by A25;
    suppose
      PFx is convergent_to_+infty;
      hence PF#x is convergent by A13;
    end;
    suppose
      PFx is convergent_to_-infty;
      hence PF#x is convergent by A19;
    end;
    suppose
      PFx is convergent_to_finite_number;
      hence PF#x is convergent by A5;
    end;
  end;
  assume
A26: PF#x is convergent;
  per cases by A26;
  suppose
    PF#x is convergent_to_+infty;
    hence thesis by A16;
  end;
  suppose
    PF#x is convergent_to_-infty;
    hence thesis by A22;
  end;
  suppose
    PF#x is convergent_to_finite_number;
    hence thesis by A9;
  end;
end;

theorem Th34:
  F is additive & F is with_the_same_dom & dom f c= dom(F.0) & x
in dom f & F#x is summable & f.x = Sum(F#x) implies f.x = lim((Partial_Sums F)#
  x)
proof
  set PF = Partial_Sums F;
  assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: dom f c= dom(F.0) and
A4: x in dom f and
A5: F#x is summable and
A6: f.x = Sum(F#x);
  set PFx = Partial_Sums(F#x);
  PFx is convergent by A5;
  then
A7: PF#x is convergent by A1,A2,A3,A4,Th33;
  per cases by A7,MESFUNC5:def 12;
  suppose
A8: ex g be Real st lim(PF#x) = g & (for p be Real st 0<p
ex n be Nat st for m be Nat st n<=m holds |. (PF#x).m- lim (PF#x) .| < p) & (PF
    #x) is convergent_to_finite_number;
    then
A9: PFx is convergent_to_finite_number by A1,A2,A3,A4,Th33;
    then
A10: not PFx is convergent_to_+infty by MESFUNC5:50;
A11: not PFx is convergent_to_-infty by A9,MESFUNC5:51;
    PFx is convergent by A9;
    then
A12: ex g be Real st f.x = g & (for p be Real st 0<p ex n be
    Nat st for m be Nat st n<=m holds |. PFx.m- f.x .| < p) & PFx is
    convergent_to_finite_number by A6,A10,A11,MESFUNC5:def 12;
    now
      let p be Real;
      assume 0<p;
      then consider n be Nat such that
A13:  for m be Nat st n<=m holds |. PFx.m - f.x .| < p by A12;
      take n;
      let m be Nat;
      assume
A14:  n<=m;
      PFx.m = (PF#x).m by A1,A2,A3,A4,Th32;
      hence |. (PF#x).m - f.x .| < p by A13,A14;
    end;
    hence thesis by A7,A8,A12,MESFUNC5:def 12;
  end;
  suppose
A15: lim(PF#x)=+infty & PF#x is convergent_to_+infty;
    then
A16: PFx is convergent_to_+infty by A1,A2,A3,A4,Th33;
    then PFx is convergent;
    hence thesis by A6,A15,A16,MESFUNC5:def 12;
  end;
  suppose
A17: lim(PF#x)=-infty & PF#x is convergent_to_-infty;
    then
A18: PFx is convergent_to_-infty by A1,A2,A3,A4,Th33;
    then PFx is convergent;
    hence thesis by A6,A17,A18,MESFUNC5:def 12;
  end;
end;

theorem Th35:
  (for m be Nat holds F.m is_simple_func_in S) implies F is
  additive & (Partial_Sums F).n is_simple_func_in S
proof
  defpred P[Nat] means (Partial_Sums F).$1 is_simple_func_in S;
  assume
A1: for m be Nat holds F.m is_simple_func_in S;
  hereby
    let n,m be Nat;
    assume n <> m;
    F.n is_simple_func_in S by A1;
    then F.n is without+infty by MESFUNC5:14;
    hence for x be set st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or
    (F.m).x <> -infty;
  end;
A2: for k be Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A3: P[k];
    F.(k+1) is_simple_func_in S by A1;
    then (Partial_Sums F).k + F.(k+1) is_simple_func_in S by A3,MESFUNC5:38;
    hence thesis by Def4;
  end;
  (Partial_Sums F).0 = F.0 by Def4;
  then
A4: P[ 0 ] by A1;
  for k be Nat holds P[k] from NAT_1:sch 2(A4,A2);
  hence thesis;
end;

theorem Th36:
  (for m be Nat holds F.m is nonnegative) implies (Partial_Sums F)
  .n is nonnegative
proof
  defpred P[Nat] means (Partial_Sums F).$1 is nonnegative;
  assume
A1: for m be Nat holds F.m is nonnegative;
A2: now
    let k be Nat;
    assume
A3: P[k];
A4: (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4;
    F.(k+1) is nonnegative by A1;
    hence P[k+1] by A3,A4,MESFUNC5:22;
  end;
  (Partial_Sums F).0 = F.0 by Def4;
  then
A5: P[ 0 ] by A1;
  for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
  hence thesis;
end;

theorem Th37:
  F is with_the_same_dom & x in dom(F.0) & (for k be Nat holds F.k
is nonnegative) & n <= m implies ((Partial_Sums F).n).x <= ((Partial_Sums F).m)
  .x
proof
  assume
A1: F is with_the_same_dom;
  set PF = Partial_Sums F;
  assume
A2: x in dom(F.0);
  defpred P[Nat] means (PF.n).x <= (PF.$1).x;
  assume
A3: for m be Nat holds F.m is nonnegative;
A4: for k be Nat holds (PF.k).x <= (PF.(k+1)).x
  proof
    let k be Nat;
A5: PF.(k+1) = PF.k + F.(k+1) by Def4;
    F.(k+1) is nonnegative by A3;
    then
A6: 0. <= (F.(k+1)).x by SUPINF_2:39;
    dom(PF.(k+1)) = dom(F.0) by A1,A3,Th29,Th30;
    then (PF.(k+1)).x = (PF.k).x + (F.(k+1)).x by A2,A5,MESFUNC1:def 3;
    hence thesis by A6,XXREAL_3:39;
  end;
A7: for k be Nat st k >= n & (for l be Nat st l >= n & l < k holds P[l])
  holds P[k]
  proof
    let k be Nat;
    assume that
A8: k >= n and
A9: for l be Nat st l >= n & l < k holds P[l];
    now
A10:  now
        assume
A11:    k > n+1;
        then reconsider l = k-1 as Element of NAT by NAT_1:20;
        k < k+1 by NAT_1:13;
        then
A12:    k > l by XREAL_1:19;
        k = l+1;
        then
A13:    (PF.l).x <= (PF.k).x by A4;
        l >= n by A11,XREAL_1:19;
        then (PF.n).x <= (PF.l).x by A9,A12;
        hence thesis by A13,XXREAL_0:2;
      end;
      assume k > n;
      then k >= n + 1 by NAT_1:13;
      then k = n+1 or k > n+1 by XXREAL_0:1;
      hence thesis by A4,A10;
    end;
    hence thesis by A8,XXREAL_0:1;
  end;
A14: for k being Nat st k >= n holds P[k] from NAT_1:sch 9(A7);
  assume n <= m;
  hence thesis by A14;
end;

theorem Th38:
  F is with_the_same_dom & x in dom(F.0) & (for m be Nat holds F.m
is nonnegative) implies (Partial_Sums F)#x is non-decreasing & (Partial_Sums F)
  #x is convergent
proof
  assume
A1: F is with_the_same_dom;
  assume
A2: x in dom(F.0);
  assume
A3: for m be Nat holds F.m is nonnegative;
  for n,m be Nat st m<=n holds ((Partial_Sums F)#x).m <= ((
  Partial_Sums F)#x).n
  proof
    let n,m be Nat;
    assume m <= n;
    then ((Partial_Sums F).m).x <= ((Partial_Sums F).n).x by A1,A2,A3,Th37;
    then ((Partial_Sums F)#x).m <= ((Partial_Sums F).n).x by MESFUNC5:def 13;
    hence thesis by MESFUNC5:def 13;
  end;
  hence ((Partial_Sums F)#x) is non-decreasing by RINFSUP2:7;
  hence thesis by RINFSUP2:37;
end;

theorem Th39:
  (for m be Nat holds F.m is without-infty) implies (Partial_Sums
  F).n is without-infty
proof
  defpred P[Nat] means (Partial_Sums F).$1 is without-infty;
  assume
A1: for m be Nat holds F.m is without-infty;
A2: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A3: P[k];
A4: F.(k+1) is without-infty by A1;
    (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4;
    hence thesis by A3,A4,Th3;
  end;
  (Partial_Sums F).0 = F.0 by Def4;
  then
A5: P[ 0 ] by A1;
  for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
  hence thesis;
end;

theorem
  (for m be Nat holds F.m is without+infty) implies (Partial_Sums F).n
  is without+infty
proof
  defpred P[Nat] means (Partial_Sums F).$1 is without+infty;
  assume
A1: for m be Nat holds F.m is without+infty;
A2: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A3: P[k];
A4: F.(k+1) is without+infty by A1;
    (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4;
    hence thesis by A3,A4,Th4;
  end;
  (Partial_Sums F).0 = F.0 by Def4;
  then
A5: P[ 0 ] by A1;
  for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
  hence thesis;
end;

theorem Th41:
  (for n be Nat holds F.n is E-measurable & F.n is
  without-infty) implies (Partial_Sums F).m is E-measurable
proof
  set PF = Partial_Sums F;
  defpred P[Nat] means PF.$1 is E-measurable;
  assume
A1: for n be Nat holds F.n is E-measurable & F.n is without-infty;
A2: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A3: P[k];
A4: F.(k+1) is E-measurable by A1;
A5: F.(k+1) is without-infty by A1;
    PF.k is without-infty by A1,Th39;
    then PF.k + F.(k+1) is E-measurable by A3,A4,A5,MESFUNC5:31;
    hence thesis by Def4;
  end;
  PF.0 = F.0 by Def4;
  then
A6: P[ 0 ] by A1;
  for k being Nat holds P[k] from NAT_1:sch 2(A6,A2);
  hence thesis;
end;

theorem Th42:
  F is additive & F is with_the_same_dom & G is additive & G is
with_the_same_dom & x in dom(F.0) /\ dom(G.0) & (for k be Nat, y be Element of
X st y in dom(F.0) /\ dom(G.0) holds (F.k).y <= (G.k).y) implies ((Partial_Sums
  F).n).x <= ((Partial_Sums G).n).x
proof
  assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: G is additive and
A4: G is with_the_same_dom and
A5: x in dom(F.0) /\ dom(G.0) and
A6: for k be Nat, y be Element of X st y in dom(F.0) /\ dom(G.0) holds (
  F.k).y <= (G.k).y;
  set PG = Partial_Sums G;
  set PF = Partial_Sums F;
  defpred P[Nat] means (PF.$1).x <= (PG.$1).x;
A7: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A8: P[k];
    dom(PF.(k+1)) = dom(F.0) by A1,A2,Th29;
    then
A9: x in dom(PF.(k+1)) by A5,XBOOLE_0:def 4;
    dom(PG.(k+1)) = dom(G.0) by A3,A4,Th29;
    then
A10: x in dom(PG.(k+1)) by A5,XBOOLE_0:def 4;
    PG.(k+1) = PG.k + G.(k+1) by Def4;
    then
A11: (PG.(k+1)).x = (PG.k).x + (G.(k+1)).x by A10,MESFUNC1:def 3;
    PF.(k+1) = PF.k + F.(k+1) by Def4;
    then
A12: (PF.(k+1)).x = (PF.k).x + (F.(k+1)).x by A9,MESFUNC1:def 3;
    (F.(k+1)).x <= (G.(k+1)).x by A5,A6;
    hence thesis by A8,A12,A11,XXREAL_3:36;
  end;
A13: (PG.0) = G.0 by Def4;
  (PF.0) = F.0 by Def4;
  then
A14: P[ 0 ] by A5,A6,A13;
  for k being Nat holds P[k] from NAT_1:sch 2(A14,A7);
  hence thesis;
end;

theorem Th43:
  for X be non empty set, F be Functional_Sequence of X,ExtREAL st
  F is additive & F is with_the_same_dom holds Partial_Sums F is
  with_the_same_dom
proof
  let X be non empty set, F be Functional_Sequence of X,ExtREAL;
  assume that
A1: F is additive and
A2: F is with_the_same_dom;
  let n,m be Nat;
  dom((Partial_Sums F).n) = dom(F.0) by A1,A2,Th29;
  hence thesis by A1,A2,Th29;
end;

theorem Th44:
  dom(F.0) = E & F is additive & F is with_the_same_dom & (for n
be Nat holds (Partial_Sums F).n is E-measurable) & (for x be Element of X 
st
  x in E holds F#x is summable) implies lim(Partial_Sums F) is E-measurable
proof
  assume that
A1: dom(F.0) = E and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds (Partial_Sums F).n is E-measurable and
A5: for x be Element of X st x in E holds F#x is summable;
  reconsider PF = Partial_Sums F as with_the_same_dom Functional_Sequence of X
  ,ExtREAL by A2,A3,Th43;
A6: now
    let x be Element of X;
    assume
A7: x in E;
    then F#x is summable by A5;
    then Partial_Sums(F#x) is convergent;
    hence PF#x is convergent by A1,A2,A3,A7,Th33;
  end;
  dom((Partial_Sums F).0) = E by A1,A2,A3,Th29;
  hence thesis by A4,A6,MESFUNC8:25;
end;

theorem
  (for n be Nat holds F.n is_integrable_on M) implies for m be Nat holds
  (Partial_Sums F).m is_integrable_on M
proof
  set PF = Partial_Sums F;
  defpred P1[Nat] means PF.$1 is_integrable_on M;
  assume
A1: for n be Nat holds F.n is_integrable_on M;
A2: for k be Nat st P1[k] holds P1[k+1]
  proof
    let k be Nat;
    assume
A3: P1[k];
    F.(k+1) is_integrable_on M by A1;
    then PF.k + F.(k+1) is_integrable_on M by A3,MESFUNC5:108;
    hence thesis by Def4;
  end;
  PF.0 = F.0 by Def4;
  then
A4: P1[ 0 ] by A1;
  thus for m be Nat holds P1[m] from NAT_1:sch 2(A4,A2);
end;

theorem Th46:
  E = dom(F.0) & F is additive & F is with_the_same_dom & (for n
be Nat holds F.n is E-measurable & F.n is nonnegative & I.n = 
Integral(M,F.n
  )) implies Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m
proof
  assume that
A1: E = dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is E-measurable & F.n is nonnegative & I.n
  = Integral(M,F.n);
  set PF = Partial_Sums F;
A5: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12;
  thus Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m
  proof
    set PI = Partial_Sums I;
    defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1;
A6: for k be Nat st P2[k] holds P2[k+1]
    proof
      let k be Nat;
      assume
A7:   P2[k];
A8:   F.(k+1) is E-measurable by A4;
A9:   dom(F.(k+1)) = E by A1,A3;
A10:  PF.(k+1) is E-measurable by A4,A5,Th41;
A11:  PF.(k+1) is nonnegative by A4,Th36;
A12:  F.(k+1) is nonnegative by A4;
A13:  PF.k is nonnegative by A4,Th36;
A14:  dom(PF.k) = E by A1,A2,A3,Th29;
A15:  PF.k is E-measurable by A4,A5,Th41;
      then consider D be Element of S such that
A16:  D = dom(PF.k + F.(k+1)) and
A17:  integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+
      (M,( F.(k+1))|D) by A14,A9,A8,A13,A12,MESFUNC5:78;
A18:  D = E /\ E by A14,A9,A13,A12,A16,MESFUNC5:22;
      then
A19:  (PF.k)|D = PF.k by A14;
A20:  (F.(k+1))|D = F.(k+1) by A9,A18;
      dom(PF.(k+1)) = E by A1,A2,A3,Th29;
      then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by A10,A11,MESFUNC5:88
        .= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A17,Def4
        .= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A14,A15,A13,A19,
MESFUNC5:88
        .= Integral(M,PF.k) + Integral(M,F.(k+1)) by A9,A8,A12,A20,MESFUNC5:88
        .= PI.k + I.(k+1) by A4,A7;
      hence thesis by Def1;
    end;
    Integral(M,PF.0) = Integral(M,F.0) by Def4;
    then Integral(M,PF.0) = I.0 by A4;
    then
A21: P2[ 0 ] by Def1;
    for k be Nat holds P2[k] from NAT_1:sch 2(A21,A6);
    hence thesis;
  end;
end;

begin :: Sequence of Measurable Functions

Lm2: E c= dom f & f is E-measurable & E ={} & (for n be Nat holds F.n
is_simple_func_in S) implies ex I be ExtREAL_sequence st (for n be Nat holds I.
n = Integral(M,(F.n)|E)) & I is summable & Integral(M,f|E) = Sum(I)
proof
  assume that
A1: E c= dom f and
A2: f is E-measurable and
A3: E ={} and
A4: for n be Nat holds F.n is_simple_func_in S;
  take I = NAT --> 0.;
A5: M.E = 0 by A3,VALUED_0:def 19;
  thus for n be Nat holds I.n = Integral(M,(F.n)|E)
  proof
    let n be Nat;
    reconsider m = n as Element of NAT by ORDINAL1:def 12;
    reconsider D = dom(F.m) as Element of S by A4,MESFUNC5:37;
    F.m is D-measurable by A4,MESFUNC2:34;
    then Integral(M,(F.m)|E) = 0 by A5,MESFUNC5:94;
    hence thesis by FUNCOP_1:7;
  end;
  defpred P[Nat] means (Partial_Sums I).$1 = 0;
A6: for k be Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A7: P[k];
A8: I.(k+1) = 0 by FUNCOP_1:7;
    (Partial_Sums I).(k+1) = (Partial_Sums I).k + I.(k+1) by Def1;
    hence thesis by A7,A8;
  end;
  (Partial_Sums I).0 = I.0 by Def1;
  then
A9: P[ 0 ] by FUNCOP_1:7;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A9,A6);
A11: for n be Nat holds (Partial_Sums I).n = 0
  by A10;
  then
A12: lim(Partial_Sums I) = 0 by MESFUNC5:52;
  Partial_Sums I is convergent_to_finite_number by A11,MESFUNC5:52;
  then Partial_Sums I is convergent;
  hence I is summable;
A13: E = dom(f|E) by A1,RELAT_1:62;
  then E = dom f /\ E by RELAT_1:61;
  then Integral(M,(f|E)|E) = 0 by A2,A5,A13,MESFUNC5:42,94;
  hence thesis by A12;
end;

Lm3: E c= dom f & f is nonnegative & f is E-measurable & 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 E-measurable and
A4: F is additive and
A5: E common_on_dom F and
A6: for n be Nat holds F.n is_simple_func_in S & F.n is nonnegative and
A7: for x be Element of X st x in E holds F#x is summable & f.x = Sum(F# x);
  deffunc G1(Nat) = (F.$1)|E;
  consider g1 be Functional_Sequence of X,ExtREAL such that
A8: for n be Nat holds g1.n = G1(n) from SEQFUNC:sch 1;
A9: for n be Nat holds (F.n)|E is_simple_func_in S & (F.n)|E is nonnegative &
  dom((F.n)|E) = E
  proof
    let n be Nat;
    reconsider n9=n as Element of NAT by ORDINAL1:def 12;
    thus (F.n)|E is_simple_func_in S by A6,MESFUNC5:34;
    thus (F.n)|E is nonnegative by A6,MESFUNC5:15;
    E c= dom(F.n9) by A5,SEQFUNC:def 9;
    hence thesis by RELAT_1:62;
  end;
  for n,m be Nat holds dom(g1.n) = dom(g1.m)
  proof
    let n,m be Nat;
    dom(g1.m) = dom((F.m)|E) by A8;
    then
A10: dom(g1.m) = E by A9;
    dom(g1.n) = dom((F.n)|E) by A8;
    hence thesis by A9,A10;
  end;
  then
A11: g1 is with_the_same_dom;
  set G = Partial_Sums g1;
  deffunc I(Element of NAT) = Integral(M,g1.$1);
  consider I be ExtREAL_sequence such that
A12: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
  take I;
A13: dom(f|E) = E by A1,RELAT_1:62;
  then dom f /\ E = E by RELAT_1:61;
  then
A14: f|E is E-measurable by A3,MESFUNC5:42;
  set L = Partial_Sums I;
A15: for n be Nat holds I.n = Integral(M,(F.n)|E)
  proof
    let n be Nat;
    reconsider m = n as Element of NAT by ORDINAL1:def 12;
    I.m = Integral(M,g1.m) by A12;
    hence thesis by A8;
  end;
A16: for k be Nat holds g1.k is nonnegative
  proof
    let k be Nat;
    (F.k)|E is nonnegative by A9;
    hence thesis by A8;
  end;
A17: for n be Nat holds G.n is_simple_func_in S & G.n is nonnegative & dom(G.
  n)=E
  proof
    let n be Nat;
A18: for n be Nat holds g1.n is_simple_func_in S
    proof
      let n be Nat;
      (F.n)|E is_simple_func_in S by A9;
      hence thesis by A8;
    end;
    hence G.n is_simple_func_in S by Th35;
    thus G.n is nonnegative by A16,Th36;
    dom(g1.0) = dom((F.0)|E) by A8;
    then dom(g1.0) = E by A9;
    hence thesis by A11,A18,Th29,Th35;
  end;
  G.0 = g1.0 by Def4;
  then
A19: G.0 = (F.0)|E by A8;
A20: for n be Nat holds integral'(M,G.n) = L.n
  proof
    defpred L[Nat] means L.$1 = integral'(M,G.$1);
    let n be Nat;
A21: G.0 is nonnegative by A17;
A22: for k be Nat st L[k] holds L[k+1]
    proof
      let k be Nat;
      assume
A23:  L[k];
      L.(k+1) = (Partial_Sums I).k + I.(k+1) by Def1;
      then
A24:  L.(k+1) = integral'(M,G.k) + Integral(M,(F.(k+1))|E) by A15,A23;
A25:  (F.(k+1))|E is_simple_func_in S by A9;
A26:  dom((F.(k+1))|E) = E by A9;
A27:  G.k is_simple_func_in S by A17;
      G.(k+1) = G.k + g1.(k+1) by Def4;
      then
A28:  G.(k+1) = G.k + (F.(k+1))|E by A8;
A29:  (F.(k+1))|E is nonnegative by A9;
A30:  G.k is nonnegative by A17;
A31:  dom(G.k) = E by A17;
      then E = dom(G.k) /\ dom((F.(k+1))|E) by A26;
      then dom( G.k + (F.(k+1))|E ) = E by A25,A29,A27,A30,MESFUNC5:65;
      then
A32:  integral'(M,G.k + (F.(k+1))|E) = integral'(M,(G.k)|E) + integral'(M
      ,((F.(k+1))|E)|E) by A25,A29,A27,A30,MESFUNC5:65;
      (G.k)|E = G.k by A31;
      hence thesis by A28,A24,A25,A29,A32,MESFUNC5:89;
    end;
    L.0 = I.0 by Def1;
    then
A33: L.0 = Integral(M,G.0) by A15,A19;
    G.0 is_simple_func_in S by A17;
    then
A34: L[ 0 ] by A33,A21,MESFUNC5:89;
A35: for k be Nat holds L[k] from NAT_1:sch 2(A34,A22);
    thus thesis by A35;
  end;
  g1.0 = (F.0)|E by A8;
  then
A36: dom(g1.0) = E by A9;
A37: for x be Element of X st x in dom(f|E) holds g1#x is summable & (f|E).x
  = Sum(g1#x)
  proof
    let x be Element of X;
    assume
A38: x in dom(f|E);
    then
A39: f.x = (f|E).x by FUNCT_1:47;
A40: for n be object st n in NAT holds (F#x).n = (g1#x).n
    proof
      let n be object;
      assume n in NAT;
      then reconsider n1 = n as Nat;
A41:  (F#x).n = (F.n1).x by MESFUNC5:def 13;
A42:  dom((F.n1)|E) = E by A9;
      (F.n1)|E = g1.n1 by A8;
      then (g1.n1).x = (F.n1).x by A13,A38,A42,FUNCT_1:47;
      hence thesis by A41,MESFUNC5:def 13;
    end;
A43: f.x = Sum(F#x) by A7,A13,A38;
    F#x is summable by A7,A13,A38;
    hence thesis by A43,A39,A40,FUNCT_2:12;
  end;
A44: f|E is nonnegative by A2,MESFUNC5:15;
  then consider
  F be Functional_Sequence of X,ExtREAL, K be ExtREAL_sequence such
  that
A45: for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom(f|E) and
A46: for n be Nat holds F.n is nonnegative and
A47: for n,m be Nat st n <=m holds for x be Element of X st x in dom(f|
  E) holds (F.n).x <= (F.m).x and
A48: for x be Element of X st x in dom(f|E) holds F#x is convergent &
  lim(F#x) = (f|E).x and
A49: for n be Nat holds K.n=integral'(M,F.n) and
  K is convergent and
A50: integral+(M,(f|E))=lim K by A13,A14,MESFUNC5:def 15;
A51: g1 is additive by A4,A8,Th31;
A52: for x be Element of X st x in E holds F#x is convergent & G#x is
  convergent & lim(F#x) = lim(G#x)
  proof
    let x be Element of X;
    assume
A53: x in E;
    hence F#x is convergent by A13,A48;
    g1#x is summable by A13,A37,A53;
    then Partial_Sums(g1#x) is convergent;
    hence G#x is convergent by A11,A51,A36,A53,Th33;
A54: (f|E).x = Sum(g1#x) by A13,A37,A53;
    g1#x is summable by A13,A37,A53;
    then lim(G#x) = (f|E).x by A4,A13,A8,A11,A36,A53,A54,Th31,Th34;
    hence thesis by A13,A48,A53;
  end;
A55: for n,m be Nat st n <=m holds for x be Element of X st x in E holds (G.n
  ).x <= (G.m).x by A11,A16,A36,Th37;
  then
A56: L is convergent by A13,A17,A20,A45,A46,A47,A49,A52,MESFUNC5:76;
  lim L = integral+(M,(f|E)) by A13,A17,A20,A45,A46,A47,A49,A50,A55,A52,
MESFUNC5:76;
  hence thesis by A13,A15,A14,A44,A56,MESFUNC5:88;
end;

theorem
  E c= dom f & f is nonnegative & f is E-measurable & F is additive &
(for n holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom(F.n)) & (
  for x st x in E holds F#x is summable & f.x = Sum(F#x)) implies ex I be
  ExtREAL_sequence st (for n holds I.n = Integral(M,(F.n)|E)) & I is summable &
  Integral(M,f|E) = Sum I
proof
  assume that
A1: E c= dom f and
A2: f is nonnegative and
A3: f is E-measurable and
A4: F is additive and
A5: for n holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom
  (F.n) and
A6: for x st x in E holds F#x is summable & f.x = Sum(F#x);
  per cases;
  suppose
    E = {};
    hence thesis by A1,A3,A5,Lm2;
  end;
  suppose
A7: E <> {};
    for n be Nat holds F.n is_simple_func_in S & F.n is
    nonnegative & E c= dom(F.n) by A5;
    then E common_on_dom F by A7,SEQFUNC:def 9;
    hence thesis by A1,A2,A3,A4,A5,A6,Lm3;
  end;
end;

theorem
  E c= dom f & f is nonnegative & f is E-measurable 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 E-measurable) & (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 E-measurable;
  set F = f|E;
A4: dom F = E by A1,RELAT_1:62;
  E = dom f /\ E by A1,XBOOLE_1:28;
  then F is E-measurable by A3,MESFUNC5:42;
  then consider h be Functional_Sequence of X,ExtREAL such that
A5: for n be Nat holds h.n is_simple_func_in S & dom(h.n) = dom F and
A6: for n be Nat holds h.n is nonnegative and
A7: for n,m be Nat st n <=m holds for x be Element of X st x in dom F
  holds (h.n).x <= (h.m).x and
A8: for x be Element of X st x in dom F holds (h#x) is convergent & lim
  (h#x) = F.x by A2,A4,MESFUNC5:15,64;
  defpred P[Nat,set,set] means $3 = h.($1+1) - h.$1;
A9: for n being Nat for x being set ex y being set st P[n,x,y];
  consider g being Function such that
A10: dom g = NAT & g.0 = h.0 & for n being Nat holds P[n,g.n,
  g.(n+1)] from RECDEF_1:sch 1(A9);
  now
    defpred IND[Nat] means g.$1 is PartFunc of X,ExtREAL;
    let f be object;
    assume f in rng g;
    then consider m be object such that
A11: m in dom g and
A12: f = g.m by FUNCT_1:def 3;
    reconsider m as Element of NAT by A10,A11;
A13: for n be Nat st IND[n] holds IND[n+1]
    proof
      let n be Nat;
      assume IND[n];
      g.(n+1) = h.(n+1) - h.n by A10;
      hence thesis;
    end;
A14: IND[ 0 ] by A10;
    for n be Nat holds IND[n] from NAT_1:sch 2(A14,A13);
    then g.m is PartFunc of X,ExtREAL;
    hence f in PFuncs(X,ExtREAL) by A12,PARTFUN1:45;
  end;
  then rng g c= PFuncs(X,ExtREAL);
  then reconsider g as Functional_Sequence of X,ExtREAL by A10,FUNCT_2:def 1
,RELSET_1:4;
  take g;
A15: for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n
  is E-measurable & E c= dom(g.n)
  proof
    let n be Nat;
    per cases;
    suppose
A16:  n = 0;
      hence g.n is_simple_func_in S & g.n is nonnegative by A5,A6,A10;
      hence g.n is E-measurable by MESFUNC2:34;
      thus thesis by A4,A5,A10,A16;
    end;
    suppose
      n <> 0;
      then consider m be Nat such that
A17:  n = m+1 by NAT_1:6;
      reconsider m as Element of NAT by ORDINAL1:def 12;
A18:  g.n = h.n - h.m by A10,A17;
      then
A19:  g.n = h.n + (-(h.m)) by MESFUNC2:8;
A20:  h.n is_simple_func_in S by A5;
      then
A21:  h.n is without-infty by MESFUNC5:14;
A22:  dom(h.n) = dom F by A5;
      (-jj)(#)(h.m) is_simple_func_in S by A5,MESFUNC5:39;
      then
A23:  -(h.m) is_simple_func_in S by MESFUNC2:9;
      hence g.n is_simple_func_in S by A19,A20,MESFUNC5:38;
A24:  h.m is_simple_func_in S by A5;
      then h.m is without+infty by MESFUNC5:14;
      then
A25:  dom(h.n - h.m) = dom(h.n) /\ dom(h.m) by A21,MESFUNC5:17;
A26:  dom(h.m) = dom F by A5;
      then for x being object st x in dom(h.n - h.m) holds(h.m).x <= (h.n).x
       by A7,A17,A25,A22,NAT_1:11;
      hence g.n is nonnegative by A18,A20,A24,MESFUNC5:40;
      thus g.n is E-measurable by A19,A20,A23,MESFUNC2:34,MESFUNC5:38;
      thus thesis by A4,A10,A17,A25,A22,A26;
    end;
  end;
  hence
A27: g is additive by Th35;
  thus for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n
  is E-measurable by A15;
A28: now
    let x be Element of X;
    assume
A29: x in E;
    then
A30: (h#x) is convergent by A4,A8;
A31: for m be Nat holds (Partial_Sums(g#x)).m = (h#x).m
    proof
      defpred P[Nat] means (Partial_Sums(g#x)).$1 = (h#x).$1;
      let m be Nat;
A32:  for k be Nat st P[k] holds P[k+1]
      proof
        set Pgx = Partial_Sums(g#x);
        let k be Nat;
        assume P[k];
        then
A33:    Pgx.k = (h.k).x by MESFUNC5:def 13;
A34:    dom(h.(k+1)) = dom F by A5;
A35:    h.(k+1) is_simple_func_in S by A5;
        then
A36:    h.(k+1) is without-infty by MESFUNC5:14;
        then
A37:    -infty < (h.(k+1)).x;
        h.(k+1) is without+infty by A35,MESFUNC5:14;
        then
A38:    (h.(k+1)).x < +infty;
A39:    dom(h.k) = dom F by A5;
A40:    h.k is_simple_func_in S by A5;
        then
A41:    h.k is without+infty by MESFUNC5:14;
        then
A42:    (h.k).x < +infty;
        h.k is without-infty by A40,MESFUNC5:14;
        then
A43:    -infty < (h.k).x;
        reconsider k as Element of NAT by ORDINAL1:def 12;
        reconsider hk1x=(h.(k+1)).x as Element of REAL
by A37,A38,XXREAL_0:14;
A44:    g.(k+1) = h.(k+1) - h.k by A10;
        reconsider hkx=(h.k).x as Element of REAL
by A43,A42,XXREAL_0:14;
        (h.(k+1)).x - (h.k).x = hk1x - hkx by SUPINF_2:3;
        then
A45:    (h.(k+1)).x - (h.k).x + (h.k).x = hk1x - hkx + hkx by SUPINF_2:1;
        Pgx.(k+1) = Pgx.k + ((g#x).(k+1)) by Def1;
        then
A46:    Pgx.(k+1) = (h.k).x + (g.(k+1)).x by A33,MESFUNC5:def 13;
        dom(h.(k+1) - h.k) = dom(h.(k+1)) /\ dom(h.k) by A36,A41,MESFUNC5:17;
        then (g.(k+1)).x = (h.(k+1)).x - (h.k).x by A4,A29,A34,A39,A44,
MESFUNC1:def 4;
        hence thesis by A46,A45,MESFUNC5:def 13;
      end;
      (Partial_Sums(g#x)).0 = (g#x).0 by Def1;
      then (Partial_Sums(g#x)).0 = (g.0).x by MESFUNC5:def 13;
      then
A47:  P[ 0 ] by A10,MESFUNC5:def 13;
      for k being Nat holds P[k] from NAT_1:sch 2(A47,A32);
      hence thesis;
    end;
A48: lim(h#x) = F.x by A4,A8,A29;
    per cases by A30;
    suppose
A49:  h#x is convergent_to_finite_number;
      then
A50:  not h#x is convergent_to_-infty by MESFUNC5:51;
      not h#x is convergent_to_+infty by A49,MESFUNC5:50;
      then consider s be Real such that
A51:  lim(h#x) = s and
A52:  for p be Real st 0 < p ex N be Nat st for m be Nat st N
      <= m holds |. (h#x).m - lim(h#x) .| < p and
      h#x is convergent_to_finite_number by A30,A50,MESFUNC5:def 12;
      for p be Real st 0 < p ex N be Nat st for m be Nat st N <= m
      holds |. (Partial_Sums(g#x)).m -  s .| < p
      proof
        let p be Real;
        assume 0 < p;
        then consider N be Nat such that
A53:    for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by A52;
        take N;
        let m be Nat;
        assume N <= m;
        then |. (h#x).m - lim(h#x) .| < p by A53;
        hence thesis by A31,A51;
      end;
      then
A54:  Partial_Sums(g#x) is convergent_to_finite_number;
      then
A55:  Partial_Sums(g#x) is convergent;
      hence g#x is summable;
      for p be Real st 0 < p ex N be Nat st for m be Nat st N <=
      m holds |. (Partial_Sums(g#x)).m - lim(h#x) .| < p
      proof
        let p be Real;
        assume 0 < p;
        then consider N be Nat such that
A56:    for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by A52;
        take N;
        let m be Nat;
        assume N <= m;
        then |. (h#x).m - lim(h#x) .| < p by A56;
        hence thesis by A31;
      end;
      then lim Partial_Sums(g#x) = lim(h#x) by A51,A54,A55,MESFUNC5:def 12;
      hence Sum(g#x) = f.x by A29,A48,FUNCT_1:49;
    end;
    suppose
A57:  (h#x) is convergent_to_+infty;
      for p be Real st 0 < p ex N be Nat st for m be Nat st N<=m
      holds p <= (Partial_Sums(g#x)).m
      proof
        let p be Real;
        assume 0 < p;
        then consider N be Nat such that
A58:    for m be Nat st N<=m holds p <= (h#x).m by A57;
        take N;
        let m be Nat;
        assume N <= m;
        then p <= (h#x).m by A58;
        hence thesis by A31;
      end;
      then
A59:  Partial_Sums(g#x) is convergent_to_+infty;
      then
A60:  Partial_Sums(g#x) is convergent;
      then
A61:  lim Partial_Sums(g#x) = +infty by A59,MESFUNC5:def 12;
      thus g#x is summable by A60;
      lim(h#x) = +infty by A30,A57,MESFUNC5:def 12;
      hence Sum(g#x) = f.x by A29,A48,A61,FUNCT_1:49;
    end;
    suppose
A62:  (h#x) is convergent_to_-infty;
      for p be Real st p < 0 ex N be Nat st for m be Nat st N<=m
      holds (Partial_Sums(g#x)).m <= p
      proof
        let p be Real;
        assume p < 0;
        then consider N be Nat such that
A63:    for m be Nat st N<=m holds (h#x).m <= p by A62;
        take N;
        let m be Nat;
        assume N <= m;
        then (h#x).m <= p by A63;
        hence thesis by A31;
      end;
      then
A64:  Partial_Sums(g#x) is convergent_to_-infty;
      then
A65:  Partial_Sums(g#x) is convergent;
      then
A66:  lim Partial_Sums(g#x) = -infty by A64,MESFUNC5:def 12;
      thus g#x is summable by A65;
      lim(h#x) = -infty by A30,A62,MESFUNC5:def 12;
      hence Sum(g#x) = f.x by A29,A48,A66,FUNCT_1:49;
    end;
  end;
  hence for x be Element of X st x in E holds g#x is summable & f.x = Sum(g#x);
  per cases;
  suppose
    E = {};
    hence thesis by A1,A3,A15,Lm2;
  end;
  suppose
A67: E <> {};
    for m be Nat holds g.m is_simple_func_in S & g.m is
    nonnegative & g.m is E-measurable & E c= dom(g.m) by A15;
    then E common_on_dom g by A67,SEQFUNC:def 9;
    hence thesis by A1,A2,A3,A15,A27,A28,Lm3;
  end;
end;

registration
  let X be non empty set;
  cluster additive with_the_same_dom for Functional_Sequence of X,ExtREAL;
  existence
  proof
    deffunc f(Nat) = <:{},X,ExtREAL:>;
    consider F be Functional_Sequence of X,ExtREAL such that
A1: for n be Nat holds F.n = f(n) from SEQFUNC:sch 1;
    now
      let n,m be Nat;
      F.n = <:{},X,ExtREAL:> by A1;
      hence dom(F.n) = dom(F.m) by A1;
    end;
    then reconsider
    F as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
    take F;
    now
      let n,m be Nat;
      assume n <> m;
      let x be set;
      assume
A2:   x in dom(F.n) /\ dom(F.m);
      F.n = <:{},X,ExtREAL:> by A1;
      then x in dom {} /\ dom(F.m) by A2,PARTFUN1:34;
      hence (F.n).x <> +infty or (F.m).x <> -infty;
    end;
    hence thesis;
  end;
end;

definition
  let C,D,X be non empty set, F be Function of [:C,D:],PFuncs(X,ExtREAL);
  let c be Element of C, d be Element of D;
  redefine func F.(c,d) -> PartFunc of X,ExtREAL;
  correctness
  proof
    thus F.(c,d) is PartFunc of X,ExtREAL by PARTFUN1:47;
  end;
end;

definition
  let C,D,X be non empty set;
  let F be Function of [:C,D:],X;
  let c be Element of C;
  func ProjMap1(F,c) -> Function of D,X means
  for d be Element of D holds it.d = F.(c,d);
  existence
  proof
    deffunc F(Element of D) = F.(c,$1);
    consider IT be Function such that
A1: dom IT = D & for d be Element of D holds IT.d = F(d) from FUNCT_1:
    sch 4;
    now
      let d be object;
      assume
A2:   d in D;
      then
A3:   [c,d] in [:C,D:] by ZFMISC_1:87;
      IT.d = F.(c,d) by A1,A2;
      hence IT.d in X by A3,FUNCT_2:5;
    end;
    then reconsider IT as Function of D,X by A1,FUNCT_2:3;
    take IT;
    let d be Element of D;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let P1,P2 be Function of D,X;
    assume that
A4: for d be Element of D holds P1.d = F.(c,d) and
A5: for d be Element of D holds P2.d = F.(c,d);
    now
      let d be object;
      assume d in D;
      then reconsider d1 = d as Element of D;
      P1.d1 = F.(c,d1) by A4;
      hence P1.d = P2.d by A5;
    end;
    hence thesis;
  end;
end;

definition
  let C,D,X be non empty set;
  let F be Function of [:C,D:],X;
  let d be Element of D;
  func ProjMap2(F,d) -> Function of C,X means
  for c be Element of C holds it.c = F.(c,d);
  existence
  proof
    deffunc F(Element of C) = F.($1,d);
    consider IT be Function such that
A1: dom IT = C & for c be Element of C holds IT.c = F(c) from FUNCT_1:
    sch 4;
    now
      let c be object;
      assume
A2:   c in C;
      then
A3:   [c,d] in [:C,D:] by ZFMISC_1:87;
      IT.c = F.(c,d) by A1,A2
        .= F.[c,d];
      hence IT.c in X by A3,FUNCT_2:5;
    end;
    then reconsider IT as Function of C,X by A1,FUNCT_2:3;
    take IT;
    let c be Element of C;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let P1,P2 be Function of C,X;
    assume that
A4: for c be Element of C holds P1.c = F.(c,d) and
A5: for c be Element of C holds P2.c = F.(c,d);
    now
      let c be object;
      assume c in C;
      then reconsider c1 = c as Element of C;
      P1.c1 = F.(c1,d) by A4;
      hence P1.c = P2.c by A5;
    end;
    hence thesis;
  end;
end;

definition
  let X,Y be set, F be Function of [:NAT,NAT:],PFuncs(X,Y), n be Nat;
  func ProjMap1(F,n) -> Functional_Sequence of X,Y means
  :Def8:
  for m be Nat holds it.m = F.(n,m);
  existence
  proof
    deffunc P1(Element of NAT) = F.(n,$1);
    consider IT be Function such that
A1: dom IT = NAT & for m be Element of NAT holds IT.m = P1(m) from
    FUNCT_1:sch 4;
    now
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
      let y be object;
      assume y in rng IT;
      then consider k be object such that
A2:   k in dom IT and
A3:   y = IT.k by FUNCT_1:def 3;
      reconsider k as Element of NAT by A1,A2;
      y = F.(n1,k) by A1,A3;
      hence y in PFuncs(X,Y);
    end;
    then rng IT c= PFuncs(X,Y);
    then reconsider IT as Functional_Sequence of X,Y by A1,FUNCT_2:def 1
,RELSET_1:4;
    take IT;
    thus for m be Nat holds IT.m = F.(n,m)
    proof
      let m be Nat;
      reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
      IT.m = F.(n1,m1) by A1;
      hence thesis;
    end;
  end;
  uniqueness
  proof
    let G1,G2 be Functional_Sequence of X,Y;
    assume that
A4: for m be Nat holds G1.m = F.(n,m) and
A5: for m be Nat holds G2.m = F.(n,m);
    for m be Element of NAT holds G1.m = G2.m
    proof
      let m be Element of NAT;
      reconsider m1=m as Nat;
      G1.m = F.(n,m1) by A4;
      hence thesis by A5;
    end;
    hence thesis;
  end;
  func ProjMap2(F,n) -> Functional_Sequence of X,Y means
  :Def9:
  for m be Nat holds it.m = F.(m,n);
  existence
  proof
    deffunc P2(Element of NAT) = F.($1,n);
    consider IT be Function such that
A6: dom IT = NAT & for m be Element of NAT holds IT.m = P2(m) from
    FUNCT_1:sch 4;
    now
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
      let y be object;
      assume y in rng IT;
      then consider k be object such that
A7:   k in dom IT and
A8:   y = IT.k by FUNCT_1:def 3;
      reconsider k as Element of NAT by A6,A7;
      y = F.(k,n1) by A6,A8;
      hence y in PFuncs(X,Y);
    end;
    then rng IT c= PFuncs(X,Y);
    then reconsider IT as Functional_Sequence of X,Y by A6,FUNCT_2:def 1
,RELSET_1:4;
    take IT;
    thus for m be Nat holds IT.m = F.(m,n)
    proof
      let m be Nat;
      reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
      IT.m = F.(m1,n1) by A6;
      hence thesis;
    end;
  end;
  uniqueness
  proof
    let G1,G2 be Functional_Sequence of X,Y;
    assume that
A9: for m be Nat holds G1.m = F.(m,n) and
A10: for m be Nat holds G2.m = F.(m,n);
    for m be Element of NAT holds G1.m = G2.m
    proof
      let m be Element of NAT;
      reconsider m1=m as Nat;
      G1.m = F.(m1,n) by A9;
      hence thesis by A10;
    end;
    hence thesis;
  end;
end;

definition
  let X be non empty set, F be sequence of Funcs(NAT,PFuncs(X,ExtREAL)), n
  be Nat;
  redefine func F.n -> Functional_Sequence of X,ExtREAL;
  correctness
  proof
    ex f be Function st F.n = f & dom f = NAT & rng f c= PFuncs(X,ExtREAL)
    by FUNCT_2:def 2;
    hence thesis by FUNCT_2:def 1,RELSET_1:4;
  end;
end;

theorem Th49:
  E = dom(F.0) & F is with_the_same_dom & (for n be Nat holds F.n
  is nonnegative & F.n is E-measurable) implies ex FF be sequence of
Funcs(NAT,PFuncs(X,ExtREAL)) st for n be Nat holds (for m be Nat holds (FF.n).m
is_simple_func_in S & dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m
is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in
  dom(F.n) holds ((FF.n).j).x <= ((FF.n).k).x) & for x be Element of X st x in
  dom(F.n) holds (FF.n)#x is convergent & lim((FF.n)#x) = (F.n).x
proof
  assume that
A1: E = dom(F.0) and
A2: F is with_the_same_dom and
A3: for n be Nat holds F.n is nonnegative & F.n is E-measurable;
  defpred Q[Element of NAT,set] means for G be Functional_Sequence of X,
ExtREAL st $2 = G holds (for m be Nat holds G.m is_simple_func_in S & dom(G.m)
  = dom(F.$1)) & (for m be Nat holds G.m is nonnegative) & (for j,k be Nat st j
<= k holds for x be Element of X st x in dom(F.$1) holds (G.j).x <= (G.k).x) &
(for x be Element of X st x in dom(F.$1) holds G#x is convergent & lim(G#x) = (
  F.$1).x);
A4: for n be Element of NAT holds ex G be Functional_Sequence of X,ExtREAL st
(for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n)) & (for m be
  Nat holds G.m is nonnegative) & (for j,k be Nat st j <= k holds for x be
Element of X st x in dom(F.n) holds (G.j).x <= (G.k).x ) & for x be Element of
  X st x in dom(F.n) holds (G#x) is convergent & lim(G#x) = (F.n).x
  proof
    let n be Element of NAT;
A5: F.n is E-measurable by A3;
A6: F.n is nonnegative by A3;
    E = dom(F.n) by A1,A2;
    hence thesis by A5,A6,MESFUNC5:64;
  end;
A7: for n be Element of NAT ex G be Element of Funcs(NAT,PFuncs(X,ExtREAL))
  st Q[n,G]
  proof
    let n be Element of NAT;
    consider G be Functional_Sequence of X,ExtREAL such that
A8: for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n) and
A9: for m be Nat holds G.m is nonnegative and
A10: for j,k be Nat st j <= k holds for x be Element of X st x in dom(
    F. n) holds (G.j).x <= (G.k).x and
A11: for x be Element of X st x in dom(F.n) holds (G#x) is convergent
    & lim(G#x) = (F.n).x by A4;
    reconsider G as Element of Funcs(NAT,PFuncs(X,ExtREAL)) by FUNCT_2:8;
    take G;
    thus thesis by A8,A9,A10,A11;
  end;
  consider FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) such that
A12: for n be Element of NAT holds Q[n,FF.n] from FUNCT_2:sch 3(A7);
  take FF;
  thus for n be Nat holds (for m be Nat holds (FF.n).m is_simple_func_in S &
dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m is nonnegative) & (for
j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds ((FF.n)
.j).x <= ((FF.n).k).x) & for x be Element of X st x in dom(F.n) holds (FF.n)#x
  is convergent & lim((FF.n)#x) = (F.n).x
  proof
    let n be Nat;
    reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
    for G be Functional_Sequence of X,ExtREAL st FF.n1 = G holds (for m
be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n1)) & (for m be Nat
holds G.m is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of
X st x in dom(F.n1) holds (G.j).x <= (G.k).x) & for x be Element of X st x in
    dom(F.n1) holds G#x is convergent & lim(G#x) = (F.n1).x by A12;
    hence thesis;
  end;
end;

theorem Th50:
  E = dom(F.0) & F is additive & F is with_the_same_dom & (for n
  be Nat holds F.n is E-measurable & F.n is nonnegative) implies ex I be
  ExtREAL_sequence st for n be Nat holds I.n = Integral(M,F.n) & Integral(M,(
  Partial_Sums F).n) = (Partial_Sums I).n
proof
  assume that
A1: E = dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is E-measurable & F.n is nonnegative;
  set PF = Partial_Sums F;
  deffunc I(Element of NAT) = Integral(M,F.$1);
  consider I be sequence of ExtREAL such that
A5: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
  reconsider I as ExtREAL_sequence;
  take I;
A6: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12;
  thus for n be Nat holds I.n = Integral(M,F.n) & Integral(M,(Partial_Sums F).
  n) = (Partial_Sums I).n
  proof
    set PI = Partial_Sums I;
    defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1;
    let n be Nat;
    reconsider n9=n as Element of NAT by ORDINAL1:def 12;
    I.n = Integral(M,F.n9) by A5;
    hence I.n = Integral(M,F.n);
A7: for k be Nat st P2[k] holds P2[k+1]
    proof
      let k be Nat;
      assume
A8:   P2[k];
A9:   F.(k+1) is E-measurable by A4;
A10:  dom(F.(k+1)) = E by A1,A3;
A11:  PF.(k+1) is E-measurable by A4,A6,Th41;
A12:  F.(k+1) is nonnegative by A4;
A13:  PF.k is nonnegative by A4,Th36;
A14:  dom(PF.k) = E by A1,A2,A3,Th29;
A15:  PF.k is E-measurable by A4,A6,Th41;
      then consider D be Element of S such that
A16:  D = dom(PF.k + F.(k+1)) and
A17:  integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+
      (M,( F.(k+1))|D) by A14,A10,A9,A13,A12,MESFUNC5:78;
A18:  D = dom(PF.k) /\ dom(F.(k+1)) by A13,A12,A16,MESFUNC5:22
        .= E by A14,A10;
      then
A19:  (PF.k)|D = PF.k by A14;
A20:  (F.(k+1))|D = F.(k+1) by A10,A18;
      dom(PF.(k+1)) = E by A1,A2,A3,Th29;
      then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by A4,A11,Th36,
MESFUNC5:88
        .= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A17,Def4
        .= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A14,A15,A13,A19,
MESFUNC5:88
        .= Integral(M,PF.k) + Integral(M,F.(k+1)) by A10,A9,A12,A20,MESFUNC5:88
        .= PI.k + I.(k+1) by A5,A8;
      hence thesis by Def1;
    end;
    Integral(M,PF.0) = Integral(M,F.0) by Def4;
    then Integral(M,PF.0) = I.0 by A5;
    then
A21: P2[ 0 ] by Def1;
    for k be Nat holds P2[k] from NAT_1:sch 2(A21,A7);
    hence thesis;
  end;
end;

Lm4: E = dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat
holds F.n is nonnegative & F.n is E-measurable) & (for x be Element of X 
st
x in E holds F#x is summable) implies ex I be ExtREAL_sequence st (for n be Nat
holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,(lim(Partial_Sums
F))|E) = Sum I
proof
  assume that
A1: E = dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is nonnegative & F.n is E-measurable and
A5: for x be Element of X st x in E holds F#x is summable;
  consider FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) such that
A6: for n be Nat holds (for m be Nat holds (FF.n).m is_simple_func_in S
& dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m is nonnegative) & (
for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds ((
FF.n).j).x <= ((FF.n).k).x) & for x be Element of X st x in dom(F.n) holds (FF.
  n)#x is convergent & lim((FF.n)#x) = (F.n).x by A1,A3,A4,Th49;
  defpred PP[Element of NAT,Element of NAT,set] means for n,m be Nat st n = $1
  & m = $2 holds $3 = (FF.n).m;
A7: for i1 be Element of NAT for j1 be Element of NAT ex F1 be Element of
  PFuncs(X,ExtREAL) st PP[i1,j1,F1]
  proof
    let i1 be Element of NAT;
    let j1 be Element of NAT;
    reconsider i = i1, j = j1 as Nat;
    reconsider F1 = (FF.i).j as Element of PFuncs(X,ExtREAL) by PARTFUN1:45;
    take F1;
    thus thesis;
  end;
  consider FF2 be Function of [:NAT,NAT:],PFuncs(X,ExtREAL) such that
A8: for i be Element of NAT for j be Element of NAT holds PP[i,j,FF2.(i
  ,j)] from BINOP_1:sch 3(A7);
  deffunc Phi(Nat) = (Partial_Sums ProjMap2(FF2,$1)).$1;
  consider P be Functional_Sequence of X,ExtREAL such that
A9: for k be Nat holds P.k = Phi(k) from SEQFUNC:sch 1;
A10: for n be Nat holds (for m be Nat holds dom(ProjMap1(FF2,n).m) = E & dom(
ProjMap2(FF2,n).m) = E & ProjMap1(FF2,n).m is_simple_func_in S & ProjMap2(FF2,n
  ).m is_simple_func_in S) & ProjMap1(FF2,n) is additive & ProjMap2(FF2,n) is
  additive & ProjMap1(FF2,n) is with_the_same_dom & ProjMap2(FF2,n) is
  with_the_same_dom
  proof
    let n be Nat;
A11: now
      let m be Nat;
      reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
A12:  ProjMap1(FF2,n).m = FF2.(n,m) by Def8;
A13:  FF2.(n1,m1) = (FF.n1).m by A8;
A14:  dom(F.m1) = dom(F.0) by A3;
A15:  ProjMap2(FF2,n).m = FF2.(m,n) by Def9;
A16:  FF2.(m1,n1) = (FF.m1).n by A8;
      dom(F.n1) = dom(F.m1) by A3;
      hence dom(ProjMap1(FF2,n).m) = E & dom(ProjMap2(FF2,n).m) = E by A1,A6
,A12,A15,A13,A16,A14;
      thus ProjMap1(FF2,n).m is_simple_func_in S & ProjMap2(FF2,n).m
      is_simple_func_in S by A6,A12,A15,A13,A16;
    end;
    for i1,j1 be Nat holds dom(ProjMap1(FF2,n).i1) = dom(ProjMap1(FF2,n).
    j1) & dom(ProjMap2(FF2,n).i1) = dom(ProjMap2(FF2,n).j1)
    proof
      let i1,j1 be Nat;
A17:  dom(ProjMap2(FF2,n).i1) = E by A11;
      dom(ProjMap1(FF2,n).i1) = E by A11;
      hence thesis by A11,A17;
    end;
    hence thesis by A11,Th35;
  end;
  for n,m be Nat holds dom(P.n) = dom(P.m)
  proof
    let n,m be Nat;
A18: ProjMap2(FF2,n) is with_the_same_dom by A10;
A19: dom(P.n) = dom((Partial_Sums ProjMap2(FF2,n)).n) by A9;
    ProjMap2(FF2,n) is additive by A10;
    then dom(P.n) = dom((ProjMap2(FF2,n)).0) by A18,A19,Th29;
    then dom(P.n) = E by A10;
    then
A20: dom(P.n) = dom((ProjMap2(FF2,m)).0) by A10;
A21: ProjMap2(FF2,m) is with_the_same_dom by A10;
    ProjMap2(FF2,m) is additive by A10;
    then dom(P.n) = dom((Partial_Sums ProjMap2(FF2,m)).m) by A21,A20,Th29;
    hence thesis by A9;
  end;
  then reconsider P as with_the_same_dom Functional_Sequence of X,ExtREAL by
MESFUNC8:def 2;
  dom(lim P) = dom(P.0) by MESFUNC8:def 9;
  then dom(lim P) = dom((Partial_Sums ProjMap2(FF2,0)).0) by A9;
  then dom(lim P) = dom((ProjMap2(FF2,0)).0) by Def4;
  then dom(lim P) = dom( FF2.(0,0) ) by Def9;
  then
A22: dom(lim P) = dom( (FF.0).0 ) by A8;
  then
A23: dom (lim P) = dom(F.0) by A6;
A24: for k be Nat holds for m be Nat, x be Element of X st x in dom(F.0) /\
  dom((ProjMap2(FF2,k)).0) holds ((ProjMap2(FF2,k)).m).x <= (F.m).x
  proof
    let k be Nat;
    let m be Nat, x be Element of X;
    reconsider m1 = m, k1 = k as Element of NAT by ORDINAL1:def 12;
    assume x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0);
    then x in dom(F.0) by XBOOLE_0:def 4;
    then
A25: x in dom(F.m) by A3;
    (FF.m1)#x is non-decreasing
    proof
      let j,k be ExtReal;
      assume that
A26:  j in dom((FF.m1)#x) and
A27:  k in dom((FF.m1)#x) and
A28:  j <= k;
      reconsider j,k as Element of NAT by A26,A27;
A29:  ((FF.m1)#x).k = ((FF.m1).k).x by MESFUNC5:def 13;
      ((FF.m1)#x).j = ((FF.m1).j).x by MESFUNC5:def 13;
      hence thesis by A6,A25,A28,A29;
    end;
    then lim((FF.m1)#x) = sup ((FF.m1)#x) by RINFSUP2:37;
    then ((FF.m1)#x).k1 <= lim((FF.m1)#x) by RINFSUP2:23;
    then
A30: ((FF.m1)#x).k <= (F.m1).x by A6,A25;
    (ProjMap2(FF2,k)).m = FF2.(m1,k1) by Def9;
    then (ProjMap2(FF2,k)).m = (FF.m).k by A8;
    hence thesis by A30,MESFUNC5:def 13;
  end;
A31: for x be Element of X, k be Element of NAT st x in dom(lim P) holds (P#
  x).k <= ((Partial_Sums F)#x).k
  proof
    let x be Element of X;
    let k be Element of NAT;
    assume
A32: x in dom(lim P);
    dom((ProjMap2(FF2,k)).0) = E by A10;
    then
A33: x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0) by A1,A6,A22,A32;
A34: ProjMap2(FF2,k) is with_the_same_dom by A10;
    (P#x).k = (P.k).x by MESFUNC5:def 13;
    then
A35: (P#x).k = ((Partial_Sums ProjMap2(FF2,k)).k).x by A9;
A36: for m be Nat, x be Element of X st x in dom(F.0) /\ dom((ProjMap2(
    FF2, k)).0) holds ((ProjMap2(FF2,k)).m).x <= (F.m).x by A24;
    ProjMap2(FF2,k) is additive by A10;
    then ((Partial_Sums ProjMap2(FF2,k)).k).x <= ((Partial_Sums F).k).x by A2
,A3,A33,A34,A36,Th42;
    hence thesis by A35,MESFUNC5:def 13;
  end;
  dom(lim(Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 9;
  then
A37: dom(lim(Partial_Sums F)) = E by A1,Def4;
A38: for n,m be Nat holds (ProjMap1(FF2,n)).m is nonnegative & (ProjMap2(FF2,
  n)).m is nonnegative
  proof
    let n,m be Nat;
    reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
    (ProjMap1(FF2,n)).m = FF2.(n1,m1) by Def8;
    then (ProjMap1(FF2,n)).m = (FF.n).m by A8;
    hence (ProjMap1(FF2,n)).m is nonnegative by A6;
    (ProjMap2(FF2,n)).m = FF2.(m1,n1) by Def9;
    then (ProjMap2(FF2,n)).m = (FF.m).n by A8;
    hence thesis by A6;
  end;
A39: for n be Element of NAT holds for x be Element of X st x in E holds (
  ProjMap1(FF2,n))#x is convergent & (F.n).x = lim( (ProjMap1(FF2,n))#x )
  proof
    let n be Element of NAT;
    reconsider n1 = n as Nat;
    let x be Element of X;
    assume
A40: x in E;
    for k be Nat holds ex m be Nat st k <= m & ((ProjMap1(FF2,n))#x).m > -1
    proof
      let k be Nat;
      take m = k;
A41:  ((ProjMap1(FF2,n))#x).m = ((ProjMap1(FF2,n)).m).x by MESFUNC5:def 13;
      (ProjMap1(FF2,n)).m is nonnegative by A38;
      hence thesis by A41,SUPINF_2:39;
    end;
    then
A42: not (ProjMap1(FF2,n))#x is convergent_to_-infty;
A43: E = dom(F.n1) by A1,A3;
    (ProjMap1(FF2,n))#x is non-decreasing
    proof
      let i,j be ExtReal;
      assume that
A44:  i in dom((ProjMap1(FF2,n))#x) and
A45:  j in dom((ProjMap1(FF2,n))#x) and
A46:  i <= j;
      reconsider i1=i, j1=j as Element of NAT by A44,A45;
A47:  ((ProjMap1(FF2,n))#x).i1 = ((ProjMap1(FF2,n)).i1).x by MESFUNC5:def 13;
      (ProjMap1(FF2,n)).i1 = FF2.(n,i1) by Def8;
      then
A48:  (ProjMap1(FF2,n)).i1 = (FF.n1).i1 by A8;
A49:  ((ProjMap1(FF2,n))#x).j1 = ((ProjMap1(FF2,n)).j1).x by MESFUNC5:def 13;
A50:  (ProjMap1(FF2,n)).j1 = FF2.(n,j1) by Def8;
      ((FF.n1).i1).x <= ((FF.n1).j1).x by A6,A43,A40,A46;
      hence thesis by A8,A47,A49,A48,A50;
    end;
    hence
A51: (ProjMap1(FF2,n))#x is convergent by RINFSUP2:37;
    per cases by A51,A42;
    suppose
A52:  (ProjMap1(FF2,n))#x is convergent_to_finite_number;
      then
A53:  not (ProjMap1(FF2,n))#x is convergent_to_-infty by MESFUNC5:51;
      not (ProjMap1(FF2,n))#x is convergent_to_+infty by A52,MESFUNC5:50;
      then consider lP be Real such that
A54:  lim( (ProjMap1(FF2,n))#x ) = lP and
A55:  for p be Real st 0<p ex nn be Nat st for mm be Nat st nn
<= mm holds |. ((ProjMap1(FF2,n))#x).mm - lim( (ProjMap1(FF2,n))#x ).| < p and
      (ProjMap1(FF2,n))#x is convergent_to_finite_number by A51,A53,
MESFUNC5:def 12;
A56:  for p be Real st 0<p ex nn be Nat st for mm be Nat st nn<=mm
      holds |. ((FF.n1)#x).mm -  lP .| < p
      proof
        let p be Real;
        assume 0<p;
        then consider nn be Nat such that
A57:    for mm be Nat st nn<=mm holds |. ((ProjMap1(FF2,n))#x).mm -
        lim( (ProjMap1(FF2,n))#x ).| < p by A55;
        take nn;
        let mm be Nat;
        assume
A58:    nn<=mm;
        reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;
        (ProjMap1(FF2,n)).mm = FF2.(n,mm) by Def8;
        then
A59:    (ProjMap1(FF2,n)).mm = (FF.n1).mm1 by A8;
        ((ProjMap1(FF2,n))#x).mm = ((ProjMap1(FF2,n)).mm).x by MESFUNC5:def 13;
        then ((FF.n1)#x).mm = ((ProjMap1(FF2,n))#x).mm by A59,MESFUNC5:def 13;
        hence thesis by A54,A57,A58;
      end;
      then
A60:  (FF.n1)#x is convergent_to_finite_number;
      reconsider lP as R_eal by XXREAL_0:def 1;
      (FF.n1)#x is convergent by A60;
      then lim((FF.n1)#x) =  lP by A56,A60,MESFUNC5:def 12;
      hence thesis by A6,A43,A40,A54;
    end;
    suppose
A61:  (ProjMap1(FF2,n))#x is convergent_to_+infty;
      for g be Real st 0 < g ex nn be Nat st for mm be Nat st nn<=
      mm holds g <= ((FF.n1)#x).mm
      proof
        let g be Real;
        assume 0 < g;
        then consider nn be Nat such that
A62:    for mm be Nat st nn<=mm holds g <= ((ProjMap1(FF2,n))#x).mm
        by A61;
        take nn;
        let mm be Nat;
        assume nn<=mm;
        then
A63:    g <= ((ProjMap1(FF2,n))#x).mm by A62;
        reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;
        (ProjMap1(FF2,n)).mm = FF2.(n,mm1) by Def8;
        then
A64:    (ProjMap1(FF2,n)).mm = (FF.n).mm by A8;
        ((ProjMap1(FF2,n))#x).mm = ((ProjMap1(FF2,n)).mm).x by MESFUNC5:def 13;
        hence thesis by A63,A64,MESFUNC5:def 13;
      end;
      then
A65:  (FF.n1)#x is convergent_to_+infty;
      then (FF.n1)#x is convergent;
      then
A66:  lim((FF.n1)#x) = +infty by A65,MESFUNC5:def 12;
      lim( (ProjMap1(FF2,n))#x ) = +infty by A51,A61,MESFUNC5:def 12;
      hence thesis by A6,A43,A40,A66;
    end;
  end;
A67: dom(lim(Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 9;
  then
A68: dom(lim(Partial_Sums F)) = E by A1,Def4;
A69: for n be Nat holds dom(P.n) = dom(lim(Partial_Sums F))
  proof
    let n be Nat;
A70: ProjMap2(FF2,n) is with_the_same_dom by A10;
A71: dom(P.n) = dom((Partial_Sums ProjMap2(FF2,n)).n) by A9;
    ProjMap2(FF2,n) is additive by A10;
    then dom(P.n) = dom((ProjMap2(FF2,n)).0) by A70,A71,Th29;
    hence thesis by A68,A10;
  end;
A72: for n,m be Nat st n <= m holds for i be Nat, x be Element of X st x in
  E holds ((ProjMap2(FF2,n)).i).x <= ((ProjMap2(FF2,m)).i).x
  proof
    let n,m be Nat;
    assume
A73: n <= m;
    let i be Nat, x be Element of X;
    reconsider i1=i, n1=n, m1=m as Element of NAT by ORDINAL1:def 12;
    ((ProjMap2(FF2,n)).i).x = (FF2.(i1,n1)).x by Def9;
    then
A74: ((ProjMap2(FF2,n)).i).x = ((FF.i).n).x by A8;
    ((ProjMap2(FF2,m)).i).x = (FF2.(i1,m1)).x by Def9;
    then
A75: ((ProjMap2(FF2,m)).i).x = ((FF.i).m).x by A8;
    assume x in E;
    then x in dom(F.i) by A1,A3;
    hence thesis by A6,A73,A74,A75;
  end;
A76: for n,m be Nat st n <= m holds for i be Nat, x be Element of X st x in
E holds ((Partial_Sums ProjMap2(FF2,n)).i).x <= ((Partial_Sums ProjMap2(FF2,m))
  .i).x
  proof
    let n,m be Nat;
A77: ProjMap2(FF2,n) is with_the_same_dom by A10;
A78: ProjMap2(FF2,m) is additive by A10;
    assume
A79: n <= m;
A80: for i be Nat, x be Element of X st x in dom(ProjMap2(FF2,n).0) /\
dom(ProjMap2(FF2,m).0) holds ((ProjMap2(FF2,n)).i).x <= ((ProjMap2(FF2,m)).i).x
    proof
      let i be Nat, x be Element of X;
      assume x in dom(ProjMap2(FF2,n).0) /\ dom(ProjMap2(FF2,m).0);
      then x in dom(ProjMap2(FF2,n).0) by XBOOLE_0:def 4;
      then x in E by A10;
      hence thesis by A72,A79;
    end;
    let i be Nat, x be Element of X;
    assume
A81: x in E;
    then
A82: x in dom(ProjMap2(FF2,m).0) by A10;
    x in dom(ProjMap2(FF2,n).0) by A10,A81;
    then
A83: x in dom(ProjMap2(FF2,n).0) /\ dom(ProjMap2(FF2,m).0) by A82,
XBOOLE_0:def 4;
A84: ProjMap2(FF2,m) is with_the_same_dom by A10;
    ProjMap2(FF2,n) is additive by A10;
    hence thesis by A83,A77,A78,A84,A80,Th42;
  end;
A85: for n,m be Nat st n <= m holds for x be Element of X st x in E holds (P
  .n).x <= (P.m).x
  proof
    let n,m be Nat;
    reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
    assume
A86: n <= m;
    let x be Element of X;
A87: ProjMap2(FF2,m) is with_the_same_dom by A10;
A88: for n be Nat holds (ProjMap2(FF2,m)).n is nonnegative by A38;
    assume
A89: x in E;
    then x in dom(ProjMap2(FF2,m).0) by A10;
    then (Partial_Sums ProjMap2(FF2,m))#x is non-decreasing by A87,A88,Th38;
    then ((Partial_Sums ProjMap2(FF2,m))#x).n1 <= ((Partial_Sums ProjMap2(FF2
    ,m))#x).m1 by A86,RINFSUP2:7;
    then ((Partial_Sums ProjMap2(FF2,m)).n).x <= ((Partial_Sums ProjMap2(FF2,
    m))#x).m1 by MESFUNC5:def 13;
    then ((Partial_Sums ProjMap2(FF2,m)).n).x <= ((Partial_Sums ProjMap2(FF2,
    m)).m).x by MESFUNC5:def 13;
    then
A90: ((Partial_Sums ProjMap2(FF2,m)).n).x <= (P.m).x by A9;
    ((Partial_Sums ProjMap2(FF2,n)).n).x <= ((Partial_Sums ProjMap2(FF2,
    m)).n).x by A76,A86,A89;
    then (P.n).x <= ((Partial_Sums ProjMap2(FF2,m)).n).x by A9;
    hence thesis by A90,XXREAL_0:2;
  end;
A91: 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
A92: x in dom(lim P);
    for n,m be Nat st m<=n holds (P#x).m <= (P#x).n
    proof
      let n,m be Nat;
      assume m <= n;
      then (P.m).x <= (P.n).x by A1,A85,A23,A92;
      then (P#x).m <= (P.n).x by MESFUNC5:def 13;
      hence thesis by MESFUNC5:def 13;
    end;
    then P#x is non-decreasing by RINFSUP2:7;
    hence thesis by RINFSUP2:37;
  end;
A93: for x be Element of X st x in dom(lim P) holds lim(P#x) = lim((
  Partial_Sums F)#x)
  proof
    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;
    let x be Element of X;
A94: 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:45;
      take F1;
      thus thesis;
    end;
    consider PP2 be Function of [:NAT,NAT:],PFuncs(X,ExtREAL) such that
A95: for i be Element of NAT for j be Element of NAT holds PP2[i,j,
    PP2.(i,j)] from BINOP_1:sch 3(A94);
    assume
A96: x in dom(lim P);
    then
A97: P#x is convergent by A91;
A98: 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;
      (ProjMap2(PP2,n)).p = PP2.(p,n) by Def9;
      hence thesis by A95;
    end;
A99: 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;
      (ProjMap2(PP2,n))#x is non-decreasing
      proof
        let j,k be ExtReal;
        assume that
A100:   j in dom((ProjMap2(PP2,n))#x) and
A101:   k in dom((ProjMap2(PP2,n))#x) and
A102:   j <= k;
        reconsider j,k as Element of NAT by A100,A101;
A103:   ProjMap2(FF2,j) is additive by A10;
A104:   ProjMap2(FF2,k) is with_the_same_dom by A10;
A105:   dom((ProjMap2(FF2,k)).0) = E by A10;
        ((ProjMap2(PP2,n))#x).k = ((ProjMap2(PP2,n)).k).x by MESFUNC5:def 13;
        then
A106:   ((ProjMap2(PP2,n))#x).k = ((Partial_Sums ProjMap2(FF2,k)).n).x by A98;
A107:   ProjMap2(FF2,k) is additive by A10;
        ((ProjMap2(PP2,n))#x).j = ((ProjMap2(PP2,n)).j).x by MESFUNC5:def 13;
        then
A108:   ((ProjMap2(PP2,n))#x).j = ((Partial_Sums ProjMap2(FF2,j)).n).x by A98;
A109:   ProjMap2(FF2,j) is with_the_same_dom by A10;
A110:   dom((ProjMap2(FF2,j)).0) = E by A10;
        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 A72,A102,A105;
        hence thesis by A1,A23,A96,A108,A106,A103,A109,A107,A104,A110,A105,Th42
;
      end;
      hence (ProjMap2(PP2,n))#x is convergent by RINFSUP2:37;
      hence thesis by RINFSUP2:21;
    end;
A111: for n be Nat holds ((Partial_Sums F)#x).n <= lim(P#x)
    proof
      for p be object st p in NAT holds ((ProjMap2(PP2,0))#x).p = ((
      ProjMap1(FF2,0))#x).p
      proof
        let p be object;
        assume p in NAT;
        then reconsider p9=p as Element of NAT;
        (ProjMap2(PP2,0)).p9 = (Partial_Sums ProjMap2(FF2,p9)).0 by A98;
        then (ProjMap2(PP2,0)).p9 = (ProjMap2(FF2,p9)).0 by Def4;
        then (ProjMap2(PP2,0)).p9 = FF2.(0,p9) by Def9;
        then
A112:   (ProjMap2(PP2,0)).p9 = (ProjMap1(FF2,0)).p9 by Def8;
        ((ProjMap2(PP2,0))#x).p = ((ProjMap2(PP2,0)).p9).x by MESFUNC5:def 13;
        hence thesis by A112,MESFUNC5:def 13;
      end;
      then (ProjMap2(PP2,0))#x = (ProjMap1(FF2,0))#x;
      then
A113: lim((ProjMap2(PP2,0))#x) = (F.0).x by A1,A39,A23,A96;
      defpred C[Nat] means lim((ProjMap2(PP2,$1))#x) = ((Partial_Sums F)#x).$1;
      let n be Nat;
      reconsider n9=n as Element of NAT by ORDINAL1:def 12;
A114: lim((P#x)^\n9) = lim(P#x) by A97,RINFSUP2:21;
A115: ((ProjMap2(PP2,n))#x)^\n9 is convergent by A99;
A116: for k be Nat st C[k] holds C[k+1]
      proof
        let k be Nat;
        reconsider k9=k as Element of NAT by ORDINAL1:def 12;
        assume
A117:   C[k];
A118:   (ProjMap2(PP2,k9))#x is convergent by A99;
        now
          let m be object;
          assume m in dom((ProjMap1(FF2,k+1))#x);
          then reconsider m1=m as Element of NAT;
          (ProjMap1(FF2,k+1)).m1 is nonnegative by A38;
          then 0. <= ((ProjMap1(FF2,k+1)).m1).x by SUPINF_2:51;
          hence 0. <= ((ProjMap1(FF2,k+1))#x).m by MESFUNC5:def 13;
        end;
        then
A119:   (ProjMap1(FF2,k+1))#x is nonnegative by SUPINF_2:52;
        now
          let m be object;
          assume m in dom((ProjMap2(PP2,k))#x);
          then reconsider m1=m as Element of NAT;
A120:     (ProjMap2(PP2,k)).m1 = (Partial_Sums ProjMap2(FF2,m1)).k9 by A98;
          for l be Nat holds (ProjMap2(FF2,m1)).l is nonnegative by A38;
          then (ProjMap2(PP2,k)).m1 is nonnegative by A120,Th36;
          then 0. <= ((ProjMap2(PP2,k)).m1).x by SUPINF_2:51;
          hence 0. <= ((ProjMap2(PP2,k))#x).m by MESFUNC5:def 13;
        end;
        then
A121:   (ProjMap2(PP2,k))#x is nonnegative by SUPINF_2:52;
        x in dom((Partial_Sums F).(k+1)) by A2,A3,A23,A96,Th29;
        then
A122:   x in dom((Partial_Sums F).k + F.(k+1)) by Def4;
A123:   for p be Nat holds ((ProjMap2(PP2,k+1))#x).p = ((ProjMap2(PP2,k)
        )#x).p + ((ProjMap1(FF2,k+1))#x).p
        proof
          let p be Nat;
          reconsider p9= p as Element of NAT by ORDINAL1:def 12;
A124:     (ProjMap2(FF2,p9)).(k+1) = FF2.(k+1,p9) by Def9;
A125:     ProjMap2(FF2,p) is with_the_same_dom by A10;
A126:     dom((ProjMap2(FF2,p)).0) = E by A10;
          ProjMap2(FF2,p) is additive by A10;
          then E c= dom((Partial_Sums ProjMap2(FF2,p)).(k+1)) by A125,A126,Th29
;
          then
A127:     E c= dom((ProjMap2(PP2,k+1)).p9) by A98;
          (ProjMap2(PP2,k+1)).p9 = (Partial_Sums ProjMap2(FF2,p9)).(k+1)
          by A98;
          then
A128:     (ProjMap2(PP2,k+1)).p9 = (Partial_Sums ProjMap2(FF2,p9)).k + (
          ProjMap2(FF2,p9)).(k+1) by Def4;
          (Partial_Sums ProjMap2(FF2,p9)).k9 = (ProjMap2(PP2,k)).p9 by A98;
          then (ProjMap2(PP2,k+1)).p9 = (ProjMap2(PP2,k)).p9 + (ProjMap1(FF2,
          k+1)).p9 by A128,A124,Def8;
          then ((ProjMap2(PP2,k+1)).p9).x =((ProjMap2(PP2,k)).p9).x + ((
          ProjMap1(FF2,k+1)).p9).x by A1,A23,A96,A127,MESFUNC1:def 3;
          then
A129:     ((ProjMap2(PP2,k+1)).p9).x = ((ProjMap2(PP2,k))#x).p + ((
          ProjMap1(FF2,k+1)).p9).x by MESFUNC5:def 13;
          ((ProjMap2(PP2,k+1))#x).p = ((ProjMap2(PP2,k+1)).p9).x by
MESFUNC5:def 13;
          hence thesis by A129,MESFUNC5:def 13;
        end;
A130:   lim((ProjMap1(FF2,k+1))#x) = (F.(k+1)).x by A1,A39,A23,A96;
        (ProjMap1(FF2,k+1))#x is convergent by A1,A39,A23,A96;
        then lim((ProjMap2(PP2,k+1))#x) = lim((ProjMap2(PP2,k))#x) + lim((
        ProjMap1(FF2,k+1))#x) by A118,A121,A119,A123,Th11;
        then lim((ProjMap2(PP2,k+1))#x) = ((Partial_Sums F).k).x + (F.(k+1)).
        x by A117,A130,MESFUNC5:def 13;
        then lim((ProjMap2(PP2,k+1))#x) = ( (Partial_Sums F).k + F.(k+1) ).x
        by A122,MESFUNC1:def 3;
        then lim((ProjMap2(PP2,k+1))#x) = ((Partial_Sums F).(k+1)).x by Def4;
        hence thesis by MESFUNC5:def 13;
      end;
A131: for p be Nat holds (((ProjMap2(PP2,n))#x)^\n9).p <= ((P
      #x)^\n9).p
      proof
        let p be Nat;
A132:      n+p in NAT by ORDINAL1:def 12;
A133:   n <= n+p by NAT_1:11;
A134:   ProjMap2(FF2,n+p) is with_the_same_dom by A10;
A135:   for i be Nat holds ProjMap2(FF2,n+p).i is nonnegative by A38;
        x in dom((ProjMap2(FF2,n+p)).0) by A1,A10,A23,A96;
        then (Partial_Sums ProjMap2(FF2,n+p))#x is non-decreasing by A134,A135
,Th38;
        then ((Partial_Sums ProjMap2(FF2,n+p))#x).n9 <= ((Partial_Sums
        ProjMap2(FF2,n+p))#x).(n9+p) by A133,RINFSUP2:7;
        then
A136:   ((Partial_Sums ProjMap2(FF2,n+p))#x).n9 <= ((Partial_Sums
        ProjMap2(FF2,n+p)).(n+p)).x by MESFUNC5:def 13;
        ((P#x)^\n9).p = (P#x).(n+p) by NAT_1:def 3;
        then ((P#x)^\n9).p = (P.(n+p)).x by MESFUNC5:def 13;
        then
A137:   ((P#x)^\n9).p = ((Partial_Sums ProjMap2(FF2,n+p)).(n+p)).x by A9;
        (((ProjMap2(PP2,n))#x)^\n9).p = ((ProjMap2(PP2,n))#x).(n+p) by
NAT_1:def 3;
        then (((ProjMap2(PP2,n))#x)^\n9).p = ((ProjMap2(PP2,n)).(n+p)).x by
MESFUNC5:def 13;
        then (((ProjMap2(PP2,n))#x)^\n9).p = ((Partial_Sums ProjMap2(FF2,n+p)
        ).n).x by A98,A132;
        hence thesis by A137,A136,MESFUNC5:def 13;
      end;
      ((Partial_Sums F)#x).0 = ((Partial_Sums F).0).x by MESFUNC5:def 13;
      then
A138: C[ 0 ] by A113,Def4;
A139: for k be Nat holds C[k] from NAT_1:sch 2(A138,A116);
      (P#x)^\n9 is convergent by A97,RINFSUP2:21;
      then lim(((ProjMap2(PP2,n))#x)^\n9) <= lim((P#x)^\n9) by A115,A131,
RINFSUP2:38;
      then lim((ProjMap2(PP2,n))#x) <= lim (P#x) by A99,A114;
      hence thesis by A139;
    end;
    F#x is summable by A1,A5,A23,A96;
    then
A140: Partial_Sums(F#x) is convergent;
    (Partial_Sums F)#x is convergent
    proof
      per cases by A140;
      suppose
        Partial_Sums(F#x) is convergent_to_finite_number;
        then (Partial_Sums F)#x is convergent_to_finite_number by A2,A3,A23,A96
,Th33;
        hence thesis;
      end;
      suppose
        Partial_Sums(F#x) is convergent_to_+infty;
        then (Partial_Sums F)#x is convergent_to_+infty by A2,A3,A23,A96,Th33;
        hence thesis;
      end;
      suppose
        Partial_Sums(F#x) is convergent_to_-infty;
        then (Partial_Sums F)#x is convergent_to_-infty by A2,A3,A23,A96,Th33;
        hence thesis;
      end;
    end;
    then
A141: lim((Partial_Sums F)#x) <= lim(P#x) by A111,Th9;
A142: for k be Nat holds (P#x).k <= ((Partial_Sums F)#x).k
   proof let n be Nat;
     n in NAT by ORDINAL1:def 12;
    hence thesis by A31,A96;
   end;
    (Partial_Sums F)#x is convergent by A3,A4,A23,A96,Th38;
    then lim(P#x) <= lim((Partial_Sums F)#x) by A97,A142,RINFSUP2:38;
    hence thesis by A141,XXREAL_0:1;
  end;
A143: for x be Element of X st x in dom(lim(Partial_Sums F)) holds P#x is
  convergent & lim(P#x) = (lim(Partial_Sums F)).x
  proof
    let x be Element of X;
    assume
A144: x in dom(lim(Partial_Sums F));
    then x in dom(lim P) by A1,A6,A22,A37;
    hence P#x is convergent by A91;
    lim(P#x) = lim((Partial_Sums F)#x) by A1,A23,A37,A93,A144;
    hence thesis by A144,MESFUNC8:def 9;
  end;
A145: for n be Nat holds P.n is nonnegative
  proof
    let n be Nat;
    for k be Nat holds (ProjMap2(FF2,n)).k is nonnegative by A38;
    then (Partial_Sums ProjMap2(FF2,n)).n is nonnegative by Th36;
    hence thesis by A9;
  end;
A146: for x be object st x in dom(lim(Partial_Sums F))
   holds (lim(Partial_Sums F)).x >= 0
  proof
    let x be object;
    assume
A147: x in dom(lim(Partial_Sums F));
    then reconsider x1=x as Element of X;
A148: for n be Nat holds ((Partial_Sums F)#x1).n >= 0
    proof
      let n be Nat;
      (Partial_Sums F).n is nonnegative by A4,Th36;
      then ((Partial_Sums F).n).x1 >= 0 by SUPINF_2:51;
      hence thesis by MESFUNC5:def 13;
    end;
    x in dom(F.0) by A67,A147,Def4;
    then (Partial_Sums F)#x1 is convergent by A3,A4,Th38;
    then lim((Partial_Sums F)#x1) >= 0 by A148,Th10;
    hence thesis by A147,MESFUNC8:def 9;
  end;
  then
A149: lim(Partial_Sums F) is nonnegative by SUPINF_2:52;
  consider I be ExtREAL_sequence such that
A150: for n be Nat holds I.n = Integral(M,F.n) & Integral(M,(
  Partial_Sums F).n) = (Partial_Sums I).n by A1,A2,A3,A4,Th50;
  for n be object st n in dom I holds 0 <= I.n
  proof
    let n be object;
    assume n in dom I;
    then reconsider n1 = n as Nat;
A151: F.n1 is nonnegative by A4;
A152: F.n1 is E-measurable by A4;
    E = dom(F.n1) by A1,A3;
    then 0 <= Integral(M,F.n1) by A151,A152,MESFUNC5:90;
    hence thesis by A150;
  end;
  then I is nonnegative by SUPINF_2:52;
  then
A153: Partial_Sums I is non-decreasing by Th16;
  then
A154: Partial_Sums I is convergent by RINFSUP2:37;
  deffunc J(Element of NAT) = integral'(M,P.$1);
  consider J be sequence of ExtREAL such that
A155: for n be Element of NAT holds J.n = J(n) from FUNCT_2:sch 4;
  reconsider J as ExtREAL_sequence;
A156: for n be Nat holds P.n is_simple_func_in S
  proof
    let n be Nat;
    for m be Nat holds ProjMap2(FF2,n).m is_simple_func_in S by A10;
    then (Partial_Sums ProjMap2(FF2,n)).n is_simple_func_in S by Th35;
    hence thesis by A9;
  end;
A157: for n be Nat holds J.n = integral'(M,P.n)
  proof
    let n be Nat;
    reconsider n9=n as Element of NAT by ORDINAL1:def 12;
    J.n = integral'(M,P.n9) by A155;
    hence thesis;
  end;
  for n,m be Nat st m<=n holds J.m <= J.n
  proof
    let n,m be Nat;
A158: P.n is nonnegative by A145;
A159: P.m is_simple_func_in S by A156;
A160: for n,m,l be Nat holds dom(P.n - P.m) = dom(P.l)
    proof
      let n,m,l be Nat;
      P.m is_simple_func_in S by A156;
      then
A161: P.m is without+infty by MESFUNC5:14;
      P.n is_simple_func_in S by A156;
      then P.n is without-infty by MESFUNC5:14;
      then dom(P.n - P.m) = dom(P.n) /\ dom(P.m) by A161,MESFUNC5:17;
      then dom(P.n - P.m) = dom(lim(Partial_Sums F)) /\ dom(P.m) by A69;
      then dom(P.n - P.m) = dom(lim(Partial_Sums F)) /\ dom(lim(Partial_Sums
      F)) by A69;
      hence thesis by A69;
    end;
    then
A162: dom(P.n - P.m) = dom(P.n);
    then
A163: (P.n)|dom(P.n - P.m) = P.n;
    assume
A164: m<=n;
A165: for x be object st x in dom(P.n - P.m) holds (P.m).x <= (P.n).x
    proof
      let x be object;
      assume x in dom(P.n - P.m);
      then x in dom(lim(Partial_Sums F)) by A69,A162;
      hence thesis by A68,A85,A164;
    end;
A166: P.m is nonnegative by A145;
    dom(P.n - P.m) = dom(P.m) by A160;
    then
A167: (P.m)|dom(P.n - P.m) = P.m;
    P.n is_simple_func_in S by A156;
    then integral'(M,(P.m)|dom(P.n - P.m)) <= integral'(M,(P.n)|dom(P.n - P.m
    )) by A158,A159,A166,A165,MESFUNC5:70;
    then J.m <= integral'(M,P.n) by A157,A167,A163;
    hence thesis by A157;
  end;
  then J is non-decreasing by RINFSUP2:7;
  then
A168: J is convergent by RINFSUP2:37;
A169: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12;
  then
A170: for n be Nat holds (Partial_Sums F).n is E-measurable by A4,Th41;
  then lim(Partial_Sums F) is E-measurable by A1,A2,A3,A5,Th44;
  then integral+(M,(lim(Partial_Sums F))) = lim J by A68,A156,A85,A157,A69,A143
,A145,A149,A168,MESFUNC5:def 15;
  then
A171: Integral(M,(lim(Partial_Sums F))) = lim J by A1,A2,A3,A5,A170,A37,A149
,Th44,MESFUNC5:88;
A172: for n be Nat, x be Element of X st x in dom(F.n) holds (FF.n)#x is
  non-decreasing
  proof
    let n be Nat, x be Element of X;
    assume
A173: x in dom(F.n);
    let i,j be ExtReal;
    assume that
A174: i in dom((FF.n)#x) and
A175: j in dom((FF.n)#x) and
A176: i<=j;
    reconsider i,j as Element of NAT by A174,A175;
    ((FF.n).i).x <= ((FF.n).j).x by A6,A173,A176;
    then ((FF.n)#x).i <= ((FF.n).j).x by MESFUNC5:def 13;
    hence thesis by MESFUNC5:def 13;
  end;
A177: for n,p be Nat st p >= n holds for x be Element of X st x in E holds ((
  Partial_Sums ProjMap2(FF2,p)).n).x <= (P.p).x & (P.p).x = ((Partial_Sums
ProjMap2(FF2,p)).p).x & ((Partial_Sums ProjMap2(FF2,p)).p).x <= ((Partial_Sums
  F).p).x & ((Partial_Sums F).p).x <= (lim (Partial_Sums F)).x
  proof
    let n,p be Nat;
    reconsider p1=p, n1=n as Element of NAT by ORDINAL1:def 12;
    assume
A178: p >= n;
    let x be Element of X;
A179: for i be Nat holds ProjMap2(FF2,p).i is nonnegative by A38;
    assume
A180: x in E;
    then
A181: x in dom((ProjMap2(FF2,p)).0) by A10;
    ProjMap2(FF2,p) is with_the_same_dom by A10;
    then (Partial_Sums ProjMap2(FF2,p))#x is non-decreasing by A181,A179,Th38;
    then ((Partial_Sums ProjMap2(FF2,p))#x).n1 <= ((Partial_Sums ProjMap2(FF2
    ,p))#x).p1 by A178,RINFSUP2:7;
    then ((Partial_Sums ProjMap2(FF2,p)).n).x <= ((Partial_Sums ProjMap2(FF2,
    p))#x).p by MESFUNC5:def 13;
    then ((Partial_Sums ProjMap2(FF2,p)).n).x <= ((Partial_Sums ProjMap2(FF2,
    p)).p).x by MESFUNC5:def 13;
    hence ((Partial_Sums ProjMap2(FF2,p)).n).x <= (P.p).x by A9;
    thus (P.p).x = ((Partial_Sums ProjMap2(FF2,p)).p).x by A9;
A182: ProjMap2(FF2,p) is additive by A10;
A183: ProjMap2(FF2,p) is with_the_same_dom by A10;
A184: for n be Nat, x be Element of X st x in dom(ProjMap2(FF2,p).0) /\ dom
    (F.0) holds (ProjMap2(FF2,p).n).x <= (F.n).x
    proof
      let n be Nat, x be Element of X;
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
      assume x in dom(ProjMap2(FF2,p).0) /\ dom(F.0);
      then x in dom(F.0) by XBOOLE_0:def 4;
      then
A185: x in dom(F.n) by A3;
      then (FF.n)#x is non-decreasing by A172;
      then lim((FF.n)#x) = sup((FF.n)#x) by RINFSUP2:37;
      then ((FF.n)#x).p1 <= lim((FF.n)#x) by RINFSUP2:23;
      then
A186: ((FF.n)#x).p <= (F.n).x by A6,A185;
      ((ProjMap2(FF2,p)).n).x = (FF2.(n1,p1)).x by Def9;
      then ((ProjMap2(FF2,p)).n).x = ((FF.n).p).x by A8;
      hence thesis by A186,MESFUNC5:def 13;
    end;
    x in dom(ProjMap2(FF2,p).0) /\ dom(F.0) by A1,A180,A181,XBOOLE_0:def 4;
    hence
    ((Partial_Sums ProjMap2(FF2,p)).p).x <= ((Partial_Sums F).p).x by A2,A3
,A182,A183,A184,Th42;
    (Partial_Sums F)#x is non-decreasing by A1,A3,A4,A180,Th38;
    then lim((Partial_Sums F)#x) = sup((Partial_Sums F)#x) by RINFSUP2:37;
    then ((Partial_Sums F)#x).p1 <= lim((Partial_Sums F)#x) by RINFSUP2:23;
    then ((Partial_Sums F).p).x <= lim((Partial_Sums F)#x) by MESFUNC5:def 13;
    hence thesis by A68,A180,MESFUNC8:def 9;
  end;
  for n be Nat holds (Partial_Sums I).n <= Integral(M,(lim(Partial_Sums F)))
  proof
    let n be Nat;
A187: (Partial_Sums F).n is nonnegative by A4,Th36;
A188: lim(Partial_Sums F) is E-measurable by A1,A2,A3,A5,A170,Th44;
A189: (Partial_Sums F).n is E-measurable by A4,A169,Th41;
A190: E = dom((Partial_Sums F).n) by A1,A2,A3,Th29;
    then for x be Element of X st x in dom((Partial_Sums F).n) holds ((
    Partial_Sums F).n).x <= (lim(Partial_Sums F)).x by A177;
    then integral+(M,(Partial_Sums F).n) <= integral+(M,(lim(Partial_Sums F))
    ) by A37,A149,A190,A189,A188,A187,MESFUNC5:85;
    then Integral(M,(Partial_Sums F).n) <= integral+(M,(lim(Partial_Sums F)))
    by A170,A190,A187,MESFUNC5:88;
    then Integral(M,(Partial_Sums F).n) <= Integral(M,(lim(Partial_Sums F)))
    by A37,A146,A188,MESFUNC5:88,SUPINF_2:52;
    hence thesis by A150;
  end;
  then
A191: lim(Partial_Sums I) <= Integral(M,(lim(Partial_Sums F))) by A153,Th9,
RINFSUP2:37;
  take I;
  thus for n be Nat holds I.n = Integral(M,(F.n)|E)
  proof
    let n be Nat;
    dom(F.0) = dom(F.n) by A3;
    then (F.n)|E = F.n by A1;
    hence thesis by A150;
  end;
A192: for n be Nat holds J.n = Integral(M,P.n)
  proof
    let n be Nat;
A193: P.n is nonnegative by A145;
A194: J.n = integral'(M,P.n) by A157;
    P.n is_simple_func_in S by A156;
    hence thesis by A193,A194,MESFUNC5:89;
  end;
  for n be Nat holds J.n <= (Partial_Sums I).n
  proof
    let n be Nat;
A195: P.n is E-measurable by A156,MESFUNC2:34;
A196: (Partial_Sums F).n is nonnegative by A4,Th36;
A197:    n in NAT by ORDINAL1:def 12;
A198: for x be Element of X st x in dom(P.n) holds (P.n).x <= ((
    Partial_Sums F).n).x
    proof
      let x be Element of X;
      assume x in dom(P.n);
      then x in dom(lim(Partial_Sums F)) by A69;
      then (P#x).n <= ((Partial_Sums F)#x).n by A1,A23,A37,A31,A197;
      then (P.n).x <= ((Partial_Sums F)#x).n by MESFUNC5:def 13;
      hence thesis by MESFUNC5:def 13;
    end;
A199: P.n is nonnegative by A145;
A200: dom(P.n) = E by A37,A69;
A201: E = dom((Partial_Sums F).n) by A1,A2,A3,Th29;
    (Partial_Sums F).n is E-measurable by A4,A169,Th41;
    then integral+(M,P.n) <= integral+(M,(Partial_Sums F).n) by A201,A200,A195
,A199,A196,A198,MESFUNC5:85;
    then Integral(M,P.n) <= integral+(M,(Partial_Sums F).n) by A145,A200,A195,
MESFUNC5:88;
    then Integral(M,P.n) <= Integral(M,(Partial_Sums F).n) by A170,A201,A196,
MESFUNC5:88;
    then J.n <= Integral(M,(Partial_Sums F).n) by A192;
    hence thesis by A150;
  end;
  then lim J <= lim (Partial_Sums I) by A168,A154,RINFSUP2:38;
  then Sum I = Integral(M,(lim(Partial_Sums F))) by A171,A191,XXREAL_0:1;
  hence thesis by A37,A154;
end;

theorem Th51:
  E c= dom(F.0) & F is additive & F is with_the_same_dom & (for n
  be Nat holds F.n is nonnegative & F.n is E-measurable) & (for x be 
Element
of X st x in E holds F#x is summable) implies ex I be ExtREAL_sequence st (for
  n be Nat holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,(lim(
  Partial_Sums F))|E) = Sum I
proof
  assume that
A1: E c= dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is nonnegative & F.n is E-measurable and
A5: for x be Element of X st x in E holds F#x is summable;
  deffunc F(Nat) = (F.$1)|E;
  consider G be Functional_Sequence of X,ExtREAL such that
A6: for n be Nat holds G.n = F(n) from SEQFUNC:sch 1;
  reconsider G as additive with_the_same_dom Functional_Sequence of X,ExtREAL
  by A2,A3,A6,Th18,Th31;
A7: for n be Nat holds G.n is nonnegative & G.n is E-measurable
  proof
    let n be Nat;
    (F.n)|E is nonnegative by A4,MESFUNC5:15;
    hence G.n is nonnegative by A6;
    thus thesis by A1,A3,A4,A6,Th20;
  end;
  dom((F.0)|E) = E by A1,RELAT_1:62;
  then
A8: E = dom(G.0) by A6;
A9: for x be Element of X st x in E holds F#x = G#x
  proof
    let x be Element of X;
    assume
A10: x in E;
    for n9 be object st n9 in NAT holds (F#x).n9 = (G#x).n9
    proof
      let n9 be object;
      assume n9 in NAT;
      then reconsider n = n9 as Nat;
      dom(G.n) = E by A8,MESFUNC8:def 2;
      then x in dom((F.n)|E) by A6,A10;
      then ((F.n)|E).x = (F.n).x by FUNCT_1:47;
      then
A11:  (G.n).x = (F.n).x by A6;
      (F#x).n = (F.n).x by MESFUNC5:def 13;
      hence thesis by A11,MESFUNC5:def 13;
    end;
    hence thesis;
  end;
A12: (lim(Partial_Sums G))|E = (lim(Partial_Sums F))|E
  proof
    set E1 = dom(F.0);
    set PF = Partial_Sums F;
    set PG = Partial_Sums G;
A13: dom(lim PG) = dom(PG.0) by MESFUNC8:def 9;
    dom(PF.0) = E1 by A2,A3,Th29;
    then
A14: E c= dom(lim(PF)) by A1,MESFUNC8:def 9;
A15: for x being Element of X st x in dom(lim PG) holds (lim PG).x = (lim PF).x
    proof
      let x being Element of X;
      set PFx = Partial_Sums(F#x);
      set PGx = Partial_Sums(G#x);
      assume
A16:  x in dom(lim PG);
      then
A17:  x in E by A8,A13,Th29;
      for n be Element of NAT holds (PG#x).n = (PF#x).n
      proof
        let n be Element of NAT;
A18:    PGx.n = (PG#x).n by A8,A17,Th32;
        PFx.n = (PF#x).n by A1,A2,A3,A17,Th32;
        hence thesis by A9,A17,A18;
      end;
      then
A19:  lim(PG#x) = lim(PF#x) by FUNCT_2:63;
      (lim PG).x = lim(PG#x) by A16,MESFUNC8:def 9;
      hence thesis by A14,A17,A19,MESFUNC8:def 9;
    end;
A20: dom(PG.0) = dom(G.0) by Th29;
    then
A21: dom((lim PG)|E) = dom(lim PG) by A8,A13;
A22: dom((lim PF)|E) = E by A14,RELAT_1:62;
    then
A23: dom((lim PG)|E) = dom((lim PF)|E) by A8,A20,A13;
    for x be Element of X st x in dom((lim PG)|E) holds ((lim PG)|E).x =
    ((lim PF)|E).x
    proof
      let x be Element of X;
      assume
A24:  x in dom((lim PG)|E);
      then
A25:  ((lim PF)|E).x = (lim PF).x by A23,FUNCT_1:47;
      (lim PG).x = (lim PF).x by A21,A15,A24;
      hence thesis by A24,A25,FUNCT_1:47;
    end;
    hence thesis by A8,A20,A13,A22,PARTFUN1:5;
  end;
  for x be Element of X st x in E holds G#x is summable by A1,A5,A6,Th21;
  then consider I be ExtREAL_sequence such that
A26: for n be Nat holds I.n = Integral(M,(G.n)|E) and
A27: I is summable and
A28: Integral(M,(lim(Partial_Sums G))|E) = Sum I by A8,A7,Lm4;
  take I;
  now
    let n be Nat;
    ((F.n)|E)|E = (F.n)|E;
    then (G.n)|E = (F.n)|E by A6;
    hence I.n = Integral(M,(F.n)|E) by A26;
  end;
  hence thesis by A27,A28,A12;
end;

:: Lebesgue Monotone Convergence Theorem

::$N Lebesgue's Monotone Convergence Theorem
theorem
  E = dom(F.0) & F.0 is nonnegative & F is with_the_same_dom & (for n be
  Nat holds F.n is E-measurable) & (for n,m be Nat st n <=m holds for x be
Element of X st x in E holds (F.n).x <= (F.m).x ) & (for x be Element of X st x
in E holds F#x is convergent) implies ex I be ExtREAL_sequence st (for n be Nat
  holds I.n = Integral(M,F.n)) & I is convergent & Integral(M,lim F) = lim I
proof
  assume that
A1: E = dom(F.0) and
A2: F.0 is nonnegative and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is E-measurable and
A5: for n,m be Nat st n <= m holds for x be Element of X st x in E holds
  (F.n).x <= (F.m).x and
A6: for x be Element of X st x in E holds F#x is convergent;
A7: lim F is E-measurable by A1,A3,A4,A6,MESFUNC8:25;
A8: for n be Nat holds F.n is nonnegative
  proof
    let n be Nat;
    for x be object st x in dom(F.n) holds 0 <= (F.n).x
    proof
      let x be object;
      assume x in dom(F.n);
      then x in E by A1,A3;
      then (F.0).x <= (F.n).x by A5;
      hence thesis by A2,SUPINF_2:51;
    end;
    hence thesis by SUPINF_2:52;
  end;
  per cases;
  suppose
    ex n be Nat st M.(E /\ eq_dom(F.n,+infty)) <> 0;
    then consider N be Nat such that
A9: M.(E /\ eq_dom(F.N,+infty)) <> 0;
A10: E = dom(F.N) by A1,A3;
    then reconsider EE = E /\ eq_dom(F.N,+infty) as Element of S by A4,
MESFUNC1:33;
A11: EE c= E by XBOOLE_1:17;
    then
A12: F.N is EE-measurable by A4,MESFUNC1:30;
    EE c= dom(F.N) by A1,A3,A11;
    then
A13: EE = dom((F.N)|EE) by RELAT_1:62;
    then EE = dom(F.N) /\ EE by RELAT_1:61;
    then
A14: (F.N)|EE is EE-measurable by A12,MESFUNC5:42;
    now
      let x be object;
      assume
A15:  x in EE;
      then x in eq_dom(F.N,+infty) by XBOOLE_0:def 4;
      then (F.N).x = +infty by MESFUNC1:def 15;
      then ((F.N)|EE).x = +infty by A13,A15,FUNCT_1:47;
      hence x in eq_dom((F.N)|EE,+infty) by A13,A15,MESFUNC1:def 15;
    end;
    then
A16: EE c= eq_dom((F.N)|EE,+infty);
    for x be object st x in eq_dom((F.N)|EE,+infty) holds x in EE by A13,
MESFUNC1:def 15;
    then eq_dom((F.N)|EE,+infty) c= EE;
    then EE = eq_dom((F.N)|EE,+infty) by A16,XBOOLE_0:def 10;
    then
A17: M.(EE /\ eq_dom((F.N)|EE,+infty)) <> 0 by A9;
    F.N is E-measurable by A4;
    then
A18: Integral(M,(F.N)|EE) <= Integral(M,(F.N)|E) by A8,A10,A11,MESFUNC5:93;
    reconsider N1 = N as Element of NAT by ORDINAL1:def 12;
    deffunc I1(Element of NAT) = Integral(M,F.$1);
    consider I be sequence of ExtREAL such that
A19: for n be Element of NAT holds I.n = I1(n) from FUNCT_2:sch 4;
    reconsider I as ExtREAL_sequence;
A20: 0 < M.(E /\ eq_dom(F.N,+infty)) by A9,SUPINF_2:51;
A21: for n be Nat holds I.n = Integral(M,F.n)
    proof
      let n be Nat;
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
      I.n = Integral(M,F.n1) by A19;
      hence thesis;
    end;
    take I;
A22: dom(lim F) = dom(F.0) by MESFUNC8:def 9;
    for x be object st x in dom(lim F) holds (lim F).x >= 0
    proof
      let x be object;
      assume
A23:  x in dom(lim F);
      then reconsider x1=x as Element of X;
      for n be Nat holds (F#x1).n >= 0
      proof
        let n be Nat;
A24:    (F.0).x1 >= 0 by A2,SUPINF_2:51;
        (F.n).x1 >= (F.0).x1 by A1,A5,A22,A23;
        hence thesis by A24,MESFUNC5:def 13;
      end;
      then lim(F#x1) >= 0 by A1,A6,A22,A23,Th10;
      hence thesis by A23,MESFUNC8:def 9;
    end;
    then
A25: lim F is nonnegative by SUPINF_2:52;
A26: E = dom(lim F) by A1,MESFUNC8:def 9;
A27: EE c= E /\ eq_dom(lim F,+infty)
    proof
      let x be object;
      assume
A28:  x in EE;
      then reconsider x1=x as Element of X;
      x in eq_dom(F.N,+infty) by A28,XBOOLE_0:def 4;
      then (F.N).x1 = +infty by MESFUNC1:def 15;
      then
A29:  (F#x1).N = +infty by MESFUNC5:def 13;
A30:  x in E by A28,XBOOLE_0:def 4;
      for n,m be Nat st m <= n holds (F#x1).m <= (F#x1).n
      proof
        let n,m be Nat;
        assume m <= n;
        then (F.m).x1 <= (F.n).x1 by A5,A30;
        then (F#x1).m <= (F.n).x1 by MESFUNC5:def 13;
        hence thesis by MESFUNC5:def 13;
      end;
      then
A31:  (F#x1) is non-decreasing by RINFSUP2:7;
      then
A32:  (F#x1)^\N1 is non-decreasing by RINFSUP2:26;
      ((F#x1)^\N1).0 = (F#x1).(0+N) by NAT_1:def 3;
      then for n be Element of NAT holds +infty <= ((F#x1)^\N1).n by A29,A32,
RINFSUP2:7;
      then (F#x1)^\N1 is convergent_to_+infty by RINFSUP2:32;
      then
A33:  lim((F#x1)^\N1) = +infty by Th7;
A34:  sup(F#x1) = sup((F#x1)^\N1) by A31,RINFSUP2:26;
      lim(F#x1) = sup(F#x1) by A31,RINFSUP2:37;
      then lim(F#x1) = +infty by A32,A34,A33,RINFSUP2:37;
      then (lim F).x1 = +infty by A1,A22,A30,MESFUNC8:def 9;
      then x in eq_dom(lim F,+infty) by A26,A30,MESFUNC1:def 15;
      hence thesis by A30,XBOOLE_0:def 4;
    end;
A35: for n,m be Nat st m<=n holds I.m<=I.n
    proof
      let n,m be Nat;
A36:  F.m is E-measurable by A4;
      assume m <= n;
      then
A37:  for x be Element of X st x in E holds (F.m).x <= (F.n).x by A5;
A38:  E = dom(F.m) by A1,A3;
A39:  E = dom(F.n) by A1,A3;
A40:    n in NAT by ORDINAL1:def 12;
A41:    m in NAT by ORDINAL1:def 12;
      F.n is E-measurable by A4;
      then Integral(M,(F.m)|E) <= Integral(M,(F.n)|E) by A8,A38,A39,A36,A37
,Th15;
      then Integral(M,F.m) <= Integral(M,(F.n)|E) by A38;
      then Integral(M,F.m) <= Integral(M,F.n) by A39;
      then I.m <= Integral(M,F.n) by A19,A41;
      hence thesis by A19,A40;
    end;
    then
A42: I is non-decreasing by RINFSUP2:7;
    then
A43: I^\N1 is non-decreasing by RINFSUP2:26;
    F.N is nonnegative by A8;
    then Integral(M,(F.N)|EE) = +infty by A13,A14,A17,Th13,MESFUNC5:15;
    then +infty <= Integral(M,F.N) by A10,A18;
    then
A44: Integral(M,F.N) = +infty by XXREAL_0:4;
    for k be Element of NAT holds +infty <= (I^\N1).k
    proof
      let k be Element of NAT;
      I.N1 <= I.(N1+k) by A35,NAT_1:12;
      then I.N1 <= (I^\N1).k by NAT_1:def 3;
      hence thesis by A44,A21;
    end;
    then I^\N1 is convergent_to_+infty by RINFSUP2:32;
    then
A45: lim(I^\N1) = +infty by Th7;
    E /\ eq_dom(lim F,+infty) is Element of S by A7,A26,MESFUNC1:33;
    then
A46: M.(E /\ eq_dom(lim F,+infty)) <> 0 by A27,A20,MEASURE1:31;
A47: sup I = sup(I^\N1) by A42,RINFSUP2:26;
    lim I = sup I by A42,RINFSUP2:37;
    then lim I = +infty by A43,A47,A45,RINFSUP2:37;
    hence thesis by A7,A21,A42,A26,A25,A46,Th13,RINFSUP2:37;
  end;
  suppose
A48: for n be Nat holds M.(E /\ eq_dom(F.n,+infty)) = 0;
    defpred L[Element of NAT,set] means $2 = E /\ eq_dom(F.$1,+infty);
A49: for n be Element of NAT ex A be Element of S st L[n,A]
    proof
      let n be Element of NAT;
      E c= dom(F.n) by A1,A3;
      then reconsider A = E /\ eq_dom(F.n,+infty) as Element of S by A4,
MESFUNC1:33;
      take A;
      thus thesis;
    end;
    consider L be sequence of S such that
A50: for n be Element of NAT holds L[n,L.n] from FUNCT_2:sch 3(A49);
A51: rng L c= S by RELAT_1:def 19;
    rng L is N_Sub_set_fam of X by MEASURE1:23;
    then reconsider E0 = rng L as N_Measure_fam of S by A51,MEASURE2:def 1;
    set E1 = E\(union E0);
    deffunc H(Nat) = (F.$1)|E1;
    consider H be Functional_Sequence of X,ExtREAL such that
A52: for n be Nat holds H.n = H(n) from SEQFUNC:sch 1;
    deffunc I2(Element of NAT) = Integral(M,(F.$1)|E1);
    consider I be sequence of ExtREAL such that
A53: for n be Element of NAT holds I.n = I2(n) from FUNCT_2:sch 4;
    reconsider I as ExtREAL_sequence;
A54: E1 c= E by XBOOLE_1:36;
    then
A55: for n be Nat holds F.n is E1-measurable by A4,MESFUNC1:30;
A56: for n be Nat holds dom(H.n) = E1 & H.n is without-infty & H.n is
    without+infty
    proof
      let n be Nat;
A57:  dom(H.n) = dom((F.n)|E1) by A52;
      E1 c= dom(F.n) by A1,A3,A54;
      hence dom(H.n) = E1 by A57,RELAT_1:62;
      (F.n)|E1 is nonnegative by A8,MESFUNC5:15;
      then H.n is nonnegative by A52;
      hence H.n is without-infty by MESFUNC5:12;
      for x be set st x in dom(H.n) holds (H.n).x < +infty
      proof
        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
        let x be set;
A58:    L.n = E /\ eq_dom(F.n1,+infty) by A50;
        dom L = NAT by FUNCT_2:def 1;
        then
A59:    L.n in rng L by A58,FUNCT_1:3;
        assume x in dom(H.n);
        then
A60:    x in dom((F.n)|E1) by A52;
        then
A61:    x in E1 by RELAT_1:57;
A62:    x in dom(F.n) by A60,RELAT_1:57;
        assume
A63:    (H.n).x >= +infty;
        (H.n).x = ((F.n)|E1).x by A52;
        then (H.n).x = (F.n).x by A61,FUNCT_1:49;
        then (F.n).x = +infty by A63,XXREAL_0:4;
        then x in eq_dom(F.n,+infty) by A62,MESFUNC1:def 15;
        then x in L.n by A54,A61,A58,XBOOLE_0:def 4;
        then x in union E0 by A59,TARSKI:def 4;
        hence contradiction by A61,XBOOLE_0:def 5;
      end;
      hence thesis by MESFUNC5:11;
    end;
    for n,m be Nat holds dom(H.n) = dom(H.m)
    proof
      let n,m be Nat;
      dom(H.n) = E1 by A56;
      hence thesis by A56;
    end;
    then reconsider
    H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
    defpred G[Nat,set,set] means $3 = H.($1+1) - H.($1);
A64: for n being Nat for x being set ex y being set st G[n,x,y ];
    consider G being Function such that
A65: dom G = NAT & G.0 = H.0 & for n being Nat holds G[n,G
    .n,G.(n+1)] from RECDEF_1:sch 1(A64);
A66: for n be Nat holds G.(n+1) = H.(n+1)-H.n
    by A65;
    now
      defpred IND[Nat] means G.$1 is PartFunc of X,ExtREAL;
      let f be object;
      assume f in rng G;
      then consider m be object such that
A67:  m in dom G and
A68:  f = G.m by FUNCT_1:def 3;
      reconsider m as Nat by A65,A67;
A69:  for n be Nat st IND[n] holds IND[n+1]
      proof
        let n be Nat;
        assume IND[n];
        G.(n+1) = H.(n+1) - H.n by A66;
        hence thesis;
      end;
A70:  IND[ 0 ] by A65;
      for n be Nat holds IND[n] from NAT_1:sch 2(A70,A69);
      then G.m is PartFunc of X,ExtREAL;
      hence f in PFuncs(X,ExtREAL) by A68,PARTFUN1:45;
    end;
    then rng G c= PFuncs(X,ExtREAL);
    then reconsider G as Functional_Sequence of X,ExtREAL by A65,FUNCT_2:def 1
,RELSET_1:4;
A71: for n be Nat holds dom(G.n) = E1
    proof
      let n be Nat;
      now
        assume n <> 0;
        then consider k be Nat such that
A72:    n = k+1 by NAT_1:6;
A73:    H.(k+1) is without-infty by A56;
A74:    H.k is without+infty by A56;
        G.(k+1) = H.(k+1) - H.k by A66;
        then dom(G.(k+1)) = dom(H.(k+1)) /\ dom(H.k) by A73,A74,MESFUNC5:17;
        then dom(G.(k+1)) = E1 /\ dom(H.k) by A56;
        then dom(G.(k+1)) = E1 /\ E1 by A56;
        hence thesis by A72;
      end;
      hence thesis by A56,A65;
    end;
A75: for n,m be Nat holds dom(G.n) = dom(G.m)
    proof
      let n,m be Nat;
      dom(G.n) = E1 by A71;
      hence thesis by A71;
    end;
A76: for n be Nat holds G.n is nonnegative
    proof
      let n be Nat;
A77:  n <> 0 implies G.n is nonnegative
      proof
        assume n <> 0;
        then consider k be Nat such that
A78:    n = k + 1 by NAT_1:6;
A79:    G.(k+1) = H.(k+1) - H.k by A66;
        for x be object st x in dom(G.(k+1)) holds 0 <= (G.(k+1)).x
        proof
          let x be object;
          assume
A80:      x in dom(G.(k+1));
A81:      dom(G.(k+1)) = E1 by A71;
          (H.k).x = ((F.k)|E1).x by A52;
          then
A82:      (H.k).x = (F.k).x by A80,A81,FUNCT_1:49;
          (H.(k+1)).x = ((F.(k+1))|E1).x by A52;
          then
A83:      (H.(k+1)).x = (F.(k+1)).x by A80,A81,FUNCT_1:49;
          (F.k).x <= (F.(k+1)).x by A5,A54,A80,A81,NAT_1:11;
          then (H.(k+1)).x - (H.k).x >= 0 by A83,A82,XXREAL_3:40;
          hence thesis by A79,A80,MESFUNC1:def 4;
        end;
        hence thesis by A78,SUPINF_2:52;
      end;
      n = 0 implies G.n is nonnegative
      proof
        assume
A84:    n = 0;
        (F.n)|E1 is nonnegative by A8,MESFUNC5:15;
        hence thesis by A52,A65,A84;
      end;
      hence thesis by A77;
    end;
A85: for n1 be object st n1 in NAT holds H.n1 = (Partial_Sums G).n1
    proof
      defpred PH[Nat] means H.$1 = (Partial_Sums G).$1;
      let n1 be object;
      assume n1 in NAT;
      then reconsider n = n1 as Nat;
A86:  for k be Nat st PH[k] holds PH[k+1]
      proof
        let k be Nat;
A87:    H.k is without+infty by A56;
A88:    H.k is without-infty by A56;
A89:    dom(G.(k+1)) = E1 by A71;
        G.(k+1) is without-infty by A76,MESFUNC5:12;
        then dom(G.(k+1) + H.k) = dom(G.(k+1)) /\ dom(H.k) by A88,MESFUNC5:16;
        then dom(G.(k+1) + H.k) = E1 /\ E1 by A56,A89;
        then
A90:    dom(H.(k+1)) = dom(G.(k+1) + H.k) by A56;
A91:    G.(k+1) = H.(k+1) - H.k by A66;
        for x being Element of X st x in dom(H.(k+1)) holds (H.(k+1)).x
        = (G.(k+1) + H.k).x
        proof
          let x be Element of X;
A92:      (H.k).x <> +infty by A87;
          (H.k).x <> -infty by A88;
          then ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x - ( (H.k).x
          - (H.k).x ) by A92,XXREAL_3:32;
          then
          ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x - 0. by XXREAL_3:7;
          then
A93:      ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x by XXREAL_3:4;
          assume
A94:      x in dom(H.(k+1));
          then x in E1 by A56;
          then (H.(k+1)).x = (G.(k+1)).x + (H.k).x by A91,A89,A93,
MESFUNC1:def 4;
          hence thesis by A90,A94,MESFUNC1:def 3;
        end;
        then
A95:    H.(k+1) = G.(k+1) + H.k by A90,PARTFUN1:5;
        assume PH[k];
        hence thesis by A95,Def4;
      end;
A96:  PH[ 0 ] by A65,Def4;
      for k be Nat holds PH[k] from NAT_1:sch 2(A96,A86);
      then H.n = (Partial_Sums G).n;
      hence thesis;
    end;
    then
A97: for n be Nat holds H.n = (Partial_Sums G).n & lim H = lim(
    Partial_Sums G) by FUNCT_2:12;
    reconsider G as with_the_same_dom Functional_Sequence of X,ExtREAL by A75,
MESFUNC8:def 2;
    reconsider G as additive with_the_same_dom Functional_Sequence of X,
    ExtREAL by A76,Th30;
A98: for k be Nat holds H.k is real-valued
    proof
      let k be Nat;
      for x be Element of X st x in dom(H.k) holds |. (H.k).x .| < +infty
      proof
        let x be Element of X;
        assume x in dom(H.k);
        H.k is without+infty by A56;
        then
A99:    (H.k).x < +infty;
        H.k is without-infty by A56;
        then -infty < (H.k).x;
        hence thesis by A99,EXTREAL1:40,XXREAL_0:4;
      end;
      hence thesis by MESFUNC2:def 1;
    end;
A100: for n be Nat holds G.n is E1-measurable
    proof
      let n be Nat;
      n <> 0 implies G.n is E1-measurable
      proof
        assume n <> 0;
        then consider k be Nat such that
A101:    n = k + 1 by NAT_1:6;
A102:   E1 = dom(H.k) by A56;
A103:   G.(k+1) = H.(k+1) - H.k by A66;
A104:   H.k is real-valued by A98;
A105:   H.k is E1-measurable by A1,A3,A55,A52,Th20,XBOOLE_1:36;
A106:   H.(k+1) is real-valued by A98;
        H.(k+1) is E1-measurable by A1,A3,A55,A52,Th20,XBOOLE_1:36;
        hence thesis by A101,A105,A102,A106,A104,A103,MESFUNC2:11;
      end;
      hence thesis by A1,A3,A54,A55,A52,A65,Th20;
    end;
A107: E1 = dom(G.0) by A56,A65;
    for x be Element of X st x in E1 holds G#x is summable
    proof
      let x be Element of X;
      assume
A108: x in E1;
      E1 c= E by XBOOLE_1:36;
      then F#x is convergent by A6,A108;
      then H#x is convergent by A52,A108,Th12;
      then (Partial_Sums G)#x is convergent by A85,FUNCT_2:12;
      then Partial_Sums (G#x) is convergent by A107,A108,Th33;
      hence thesis;
    end;
    then consider J be ExtREAL_sequence such that
A109: for n be Nat holds J.n = Integral(M,(G.n)|E1) and
    J is summable and
A110: Integral(M,(lim(Partial_Sums G))|E1) = Sum J by A76,A107,A100,Th51;
    for n be object st n in NAT holds I.n = (Partial_Sums J).n
    proof
      let n be object;
      assume n in NAT;
      then reconsider n1 = n as Element of NAT;
A111: for n be Nat holds J.n = Integral(M,G.n)
      proof
        let n be Nat;
        dom(G.n) = E1 by A71;
        then (G.n)|E1 = (G.n);
        hence thesis by A109;
      end;
      E1 = dom(G.0) by A71;
      then (Partial_Sums J).n1 = Integral(M,(Partial_Sums G).n1) by A76,A100
,A111,Th46;
      then (Partial_Sums J).n1 = Integral(M,H.n1) by A85;
      then (Partial_Sums J).n1 = Integral(M,(F.n1)|E1) by A52;
      hence thesis by A53;
    end;
    then
A112: I = Partial_Sums J;
    dom(lim(Partial_Sums G)) = dom(H.0) by A97,MESFUNC8:def 9;
    then dom(lim(Partial_Sums G)) = E1 by A56;
    then
A113: lim I = Integral(M,lim H) by A97,A110,A112;
    take I;
A114: for x be Element of X st x in E1 holds F#x is convergent
    proof
      let x be Element of X;
A115: E1 c= E by XBOOLE_1:36;
      assume x in E1;
      hence thesis by A6,A115;
    end;
A116: for n be Element of NAT st 0 <= n holds (M*L).n = 0
    proof
      let n be Element of NAT;
      assume 0 <= n;
      dom L = NAT by FUNCT_2:def 1;
      then (M*L).n = M.(L.n) by FUNCT_1:13;
      then (M*L).n = M.(E /\ eq_dom(F.n,+infty)) by A50;
      hence thesis by A48;
    end;
    M*L is nonnegative by MEASURE2:1;
    then SUM(M*L) = Ser(M*L).0 by A116,SUPINF_2:48;
    then SUM(M*L) = (M*L).0 by SUPINF_2:def 11;
    then SUM(M*L) = 0 by A116;
    then M.(union E0) <= 0 by MEASURE2:11;
    then
A117: M.(union E0) = 0 by SUPINF_2:51;
A118: for n be Nat holds I.n = Integral(M,F.n)
    proof
      let n be Nat;
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A119: I.n = Integral(M,(F.n1)|E1) by A53;
      dom(F.n) = E by A1,A3;
      hence thesis by A4,A117,A119,MESFUNC5:95;
    end;
    for n,m be Nat st m <= n holds I.m <= I.n
    proof
      let n,m be Nat;
A120: F.m is nonnegative by A8;
A121: dom(F.m) = E by A1,A3;
      assume m <= n;
      then
A122: for x be Element of X st x in dom(F.m) holds (F.m).x <= (F.n).x by A5
,A121;
A123: dom(F.n) = E by A1,A3;
A124: F.n is E-measurable by A4;
A125: F.n is nonnegative by A8;
      F.m is E-measurable by A4;
      then integral+(M,F.m) <= integral+(M,F.n) by A121,A123,A122,A120,A125
,A124,MESFUNC5:85;
      then Integral(M,F.m) <= integral+(M,F.n) by A4,A121,A120,MESFUNC5:88;
      then Integral(M,F.m) <= Integral(M,F.n) by A4,A123,A125,MESFUNC5:88;
      then I.m <= Integral(M,F.n) by A118;
      hence thesis by A118;
    end;
    then
A126: I is non-decreasing by RINFSUP2:7;
    E = dom(lim F) by A1,MESFUNC8:def 9;
    then
A127: Integral(M,lim F) = Integral(M,(lim F)|E1) by A7,A117,MESFUNC5:95;
    E1 c= dom(F.0) by A1,XBOOLE_1:36;
    hence thesis by A127,A52,A118,A126,A114,A113,Th19,RINFSUP2:37;
  end;
end;