:: Series of Positive Real Numbers. Measure Theory
::  by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2012 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 CARD_1, SUPINF_1, ARYTM_3, REAL_1, ARYTM_1, XBOOLE_0, SUBSET_1,
      NUMBERS, TARSKI, XXREAL_0, MEMBERED, ORDINAL2, ORDINAL1, XXREAL_2,
      FUNCT_1, RELAT_1, VALUED_0, FUNCT_3, CARD_3, FUNCT_4, FUNCOP_1, PARTFUN1,
      NAT_1, SERIES_1, SUPINF_2, MEMBER_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0,
      XXREAL_3, XCMPLX_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, FUNCT_3, FUNCOP_1, VALUED_0, FUNCT_4, NAT_1, CARD_3, XXREAL_2,
      SUPINF_1, MEMBER_1;
 constructors FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, REAL_1, NAT_1, SUPINF_1,
      VALUED_1, XXREAL_2, XXREAL_3, CARD_3, RELSET_1, MEMBER_1;
 registrations RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0,
      MEMBERED, VALUED_0, XXREAL_3, RELSET_1, MEMBER_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, XCMPLX_0, XXREAL_0, XXREAL_3, MEMBER_1;
 theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, RELSET_1, CARD_4, SUBSET_1, FUNCT_4,
      FUNCOP_1, RELAT_1, ZFMISC_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
      ORDINAL1, NUMBERS, XXREAL_2, XXREAL_3, CARD_3, MEMBER_1, MEMBERED;
 schemes FUNCT_2, RECDEF_1, NAT_1;

begin :: operations " + "," - " in R_eal numbers

notation
  synonym 0. for 0;
end;

definition
  redefine func 0. -> R_eal;
  coherence by XXREAL_0:def 1;
  let x be R_eal;
  redefine func - x -> R_eal;
  coherence by XXREAL_0:def 1;
  let y be R_eal;
  redefine func x + y -> R_eal;
  coherence by XXREAL_0:def 1;
  redefine func x - y -> R_eal;
  coherence by XXREAL_0:def 1;
end;

theorem
  for x,y being R_eal, a,b being Real st x = a & y = b holds
  x + y = a + b by XXREAL_3:def 2;

theorem
  for x being R_eal, a being Real st x = a holds - x = - a
  by XXREAL_3:def 3;

theorem
  for x,y being R_eal, a,b being Real st x = a & y = b holds x - y = a - b
proof
  let x,y be R_eal, a,b be Real;
  assume
A1: x = a;
  assume y = b;
  then -y = -b by XXREAL_3:def 3;
  hence thesis by A1,XXREAL_3:def 2;
end;

::
::       operations " + "," - " in a subset of ExtREAL
::

notation
  let X,Y be Subset of ExtREAL;
  synonym X + Y for X ++ Y;
end;

definition
  let X,Y be Subset of ExtREAL;
  redefine func X + Y -> Subset of ExtREAL;
  coherence by MEMBERED:2;
end;

notation
  let X be Subset of ExtREAL;
  synonym -X for --X;
end;

definition
  let X be Subset of ExtREAL;
  redefine func - X -> Subset of ExtREAL;
  coherence by MEMBERED:2;
end;

canceled;

theorem
  for X being non empty Subset of ExtREAL, z being R_eal holds
  z in X iff - z in - X by MEMBER_1:1;

theorem
  for X,Y being non empty Subset of ExtREAL holds X c= Y iff - X c= - Y
  by MEMBER_1:3;

theorem
  for z being R_eal holds z in REAL iff - z in REAL
proof
  let z be R_eal;
A1: for z being R_eal holds z in REAL implies - z in REAL
  proof
    let z be R_eal;
A2: - z in REAL or - z in {-infty,+infty} by XBOOLE_0:def 3;
    assume z in REAL;
    hence thesis by A2,TARSKI:def 2;
  end;
  - z in REAL implies z in REAL
  proof
    assume -z in REAL;
    then - -z in REAL by A1;
    hence thesis;
  end;
  hence thesis by A1;
end;

definition
  let X be ext-real-membered set;
  redefine func inf X -> R_eal;
  coherence by XXREAL_0:def 1;
  redefine func sup X -> R_eal;
  coherence by XXREAL_0:def 1;
end;

theorem Th8:
  for X,Y being non empty Subset of ExtREAL holds sup (X + Y) <= sup X + sup Y
proof
  let X,Y be non empty Subset of ExtREAL;
  for z being ext-real number holds z in X + Y implies z <= sup X + sup Y
  proof
    let z be ext-real number;
    assume z in X + Y;
    then consider x,y being R_eal such that
A1: z = x + y and
A2: x in X and
A3: y in Y;
A4: y <= sup Y by A3,XXREAL_2:4;
    x <= sup X by A2,XXREAL_2:4;
    hence thesis by A1,A4,XXREAL_3:36;
  end;
  then sup X + sup Y is UpperBound of X + Y by XXREAL_2:def 1;
  hence thesis by XXREAL_2:def 3;
end;

theorem Th9:
  for X,Y being non empty Subset of ExtREAL holds inf X + inf Y <= inf (X + Y)
proof
  let X,Y be non empty Subset of ExtREAL;
  for z being ext-real number holds z in X + Y implies inf X + inf Y <= z
  proof
    let z be ext-real number;
    assume z in X + Y;
    then consider x,y being R_eal such that
A1: z = x + y and
A2: x in X and
A3: y in Y;
A4: inf Y <= y by A3,XXREAL_2:3;
    inf X <= x by A2,XXREAL_2:3;
    hence thesis by A1,A4,XXREAL_3:36;
  end;
  then inf X + inf Y is LowerBound of X + Y by XXREAL_2:def 2;
  hence thesis by XXREAL_2:def 4;
end;

theorem
  for X,Y being non empty Subset of ExtREAL holds X is bounded_above & Y
  is bounded_above implies sup (X + Y) <= sup X + sup Y by Th8;

theorem
  for X,Y being non empty Subset of ExtREAL st X is bounded_below & Y is
  bounded_below holds inf X + inf Y <= inf (X + Y) by Th9;

theorem Th12:
  for X being non empty Subset of ExtREAL, a being R_eal holds
  a is UpperBound of X iff - a is LowerBound of - X
proof
  let X be non empty Subset of ExtREAL;
  let a be R_eal;
  hereby
    assume
A1: a is UpperBound of X;
    for x being ext-real number st x in - X holds -a <= x
    proof
      let x be ext-real number;
      assume
A2:   x in - X;
      reconsider x as Element of ExtREAL by XXREAL_0:def 1;
      - x in - -X by A2;
      then - x <= a by A1,XXREAL_2:def 1;
      then - a <= - -x by XXREAL_3:38;
      hence thesis;
    end;
    hence - a is LowerBound of - X by XXREAL_2:def 2;
  end;
  assume
A3: - a is LowerBound of - X;
  for x being ext-real number st x in X holds x <=a
  proof
    let x be ext-real number;
    assume
A4: x in X;
    reconsider x as Element of ExtREAL by XXREAL_0:def 1;
    - x in - X by A4;
    then - a <= - x by A3,XXREAL_2:def 2;
    hence thesis by XXREAL_3:38;
  end;
  hence thesis by XXREAL_2:def 1;
end;

theorem Th13:
  for X being non empty Subset of ExtREAL holds for a being R_eal
  holds a is LowerBound of X iff - a is UpperBound of - X
proof
  let X be non empty Subset of ExtREAL;
  let a be R_eal;
  hereby
    assume
A1: a is LowerBound of X;
    for x being ext-real number st x in - X holds x <= - a
    proof
      let x be ext-real number;
      assume
A2:   x in - X;
      reconsider x as Element of ExtREAL by XXREAL_0:def 1;
      - x in - (- X) by A2;
      then a <= - x by A1,XXREAL_2:def 2;
      then - (- x) <= - a by XXREAL_3:38;
      hence thesis;
    end;
    hence - a is UpperBound of - X by XXREAL_2:def 1;
  end;
  assume
A3: - a is UpperBound of - X;
  for x being ext-real number st x in X holds a <= x
  proof
    let x be ext-real number;
    assume
A4: x in X;
    reconsider x as Element of ExtREAL by XXREAL_0:def 1;
    - x in - X by A4;
    then - x <= - a by A3,XXREAL_2:def 1;
    hence thesis by XXREAL_3:38;
  end;
  hence thesis by XXREAL_2:def 2;
end;

theorem Th14:
  for X being non empty Subset of ExtREAL holds inf(- X) = - sup X
proof
  let X be non empty Subset of ExtREAL;
  set a = inf(- X);
  set b = sup X;
  a is LowerBound of - X by XXREAL_2:def 4;
  then - a is UpperBound of -(-X) by Th13;
  then b <= - a by XXREAL_2:def 3;
  then
A1: - (- a) <= - b by XXREAL_3:38;
  b is UpperBound of X by XXREAL_2:def 3;
  then - b is LowerBound of - X by Th12;
  then - b <= a by XXREAL_2:def 4;
  hence thesis by A1,XXREAL_0:1;
end;

theorem Th15:
  for X be non empty Subset of ExtREAL holds sup(- X) = - inf X
proof
  let X be non empty Subset of ExtREAL;
  set a = sup(- X);
  set b = inf X;
  a is UpperBound of - X by XXREAL_2:def 3;
  then - a is LowerBound of - (- X) by Th12;
  then - a <= b by XXREAL_2:def 4;
  then
A1: - b <= - (-a) by XXREAL_3:38;
  b is LowerBound of X by XXREAL_2:def 4;
  then - b is UpperBound of - X by Th13;
  then a <= - b by XXREAL_2:def 3;
  hence thesis by A1,XXREAL_0:1;
end;

definition
  let X be non empty set;
  let Y be non empty Subset of ExtREAL;
  let F be Function of X,Y;
  redefine func rng F -> non empty Subset of ExtREAL;
  coherence
  proof
    set x = the Element of X;
    F.x in rng F by FUNCT_2:4;
    hence thesis by XBOOLE_1:1;
  end;
end;

::
::       sup F and inf F for Function of X,ExtREAL
::

definition
  let D be ext-real-membered set;
  let X be set;
  let Y be Subset of D;
  let F be PartFunc of X,Y;
  func sup F -> Element of ExtREAL equals
  sup rng F;
  coherence;
  func inf F -> Element of ExtREAL equals
  inf rng F;
  coherence;
end;

definition
  let F be ext-real-valued Function;
  let x be set;
  redefine func F.x -> R_eal;
  coherence by XXREAL_0:def 1;
end;

definition
  let X be non empty set;
  let Y,Z be non empty Subset of ExtREAL;
  let F be Function of X,Y;
  let G be Function of X,Z;
  func F + G -> Function of X,Y + Z means
  :Def3:
  for x being Element of X holds it.x = F.x + G.x;
  existence
  proof
    deffunc F(Element of X) = F.$1 + G.$1;
A1: for x being Element of X holds F(x) in Y + Z
    proof
      let x be Element of X;
A2:   G.x in Z by FUNCT_2:5;
      F.x in Y by FUNCT_2:5;
      hence thesis by A2;
    end;
    ex H being Function of X,Y + Z st for x being Element of X holds H.x =
    F(x) from FUNCT_2:sch 8(A1);
    then consider H being Function of X,Y + Z such that
A3: for x being Element of X holds H.x = F.x + G.x;
    take H;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let H1,H2 be Function of X,Y + Z such that
A4: for x being Element of X holds H1.x = F.x + G.x and
A5: for x being Element of X holds H2.x = F.x + G.x;
    for x being set st x in X holds H1.x = H2.x
    proof
      let x be set;
      assume x in X;
      then reconsider x as Element of X;
      H1.x = F.x + G.x by A4
        .= H2.x by A5;
      hence thesis;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem Th16:
  for X being non empty set, Y,Z being non empty Subset of ExtREAL,
     F being Function of X,Y, G being Function of X,Z holds
  rng(F + G) c= rng F + rng G
proof
  let X be non empty set, Y,Z be non empty Subset of ExtREAL, F be Function of
  X,Y, G be Function of X,Z;
A1: for x being set st x in X holds (F + G).x in rng F + rng G
  proof
    let x be set;
    assume x in X;
    then reconsider x as Element of X;
    reconsider a = F.x, b = G.x as R_eal;
A2: a in rng F by FUNCT_2:4;
A3: b in rng G by FUNCT_2:4;
    (F + G).x = a + b by Def3;
    hence thesis by A2,A3;
  end;
  dom (F + G) = X by FUNCT_2:def 1;
  then F + G is Function of X,rng F + rng G by A1,FUNCT_2:3;
  hence thesis by RELAT_1:def 19;
end;

theorem Th17:
  for X being non empty set, Y,Z being non empty Subset of ExtREAL
for F being Function of X,Y for G being Function of X,Z holds sup(F + G) <= sup
  F + sup G
proof
  let X be non empty set, Y,Z be non empty Subset of ExtREAL;
  let F be Function of X,Y;
  let G be Function of X,Z;
A1: sup(rng F + rng G) <= sup(rng F) + sup(rng G) by Th8;
  sup(F + G) <= sup(rng F + rng G) by Th16,XXREAL_2:59;
  hence thesis by A1,XXREAL_0:2;
end;

theorem Th18:
  for X being non empty set holds for Y,Z being non empty Subset
of ExtREAL for F being Function of X,Y for G being Function of X,Z holds inf F
  + inf G <= inf(F + G)
proof
  let X be non empty set;
  let Y,Z be non empty Subset of ExtREAL;
  let F be Function of X,Y;
  let G be Function of X,Z;
A1: inf(rng F) + inf(rng G) <= inf(rng F + rng G) by Th9;
  inf(rng F + rng G) <= inf(F + G) by Th16,XXREAL_2:60;
  hence thesis by A1,XXREAL_0:2;
end;

definition
  let X be non empty set;
  let Y be non empty Subset of ExtREAL;
  let F be Function of X,Y;
  func - F -> Function of X,- Y means
  :Def4:
  for x being Element of X holds it.x = - F.x;
  existence
  proof
    deffunc F(Element of X) = - F.$1;
A1: for x being Element of X holds F(x) in - Y
    proof
      let x be Element of X;
      F.x in Y by FUNCT_2:5;
      hence thesis;
    end;
    ex H being Function of X,- Y st for x being Element of X holds H.x = F
    (x) from FUNCT_2:sch 8(A1);
    then consider H being Function of X,- Y such that
A2: for x being Element of X holds H.x = - F.x;
    take H;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let H1,H2 be Function of X,- Y such that
A3: for x being Element of X holds H1.x = - F.x and
A4: for x being Element of X holds H2.x = - F.x;
    for x being set st x in X holds H1.x = H2.x
    proof
      let x be set;
      assume x in X;
      then reconsider x as Element of X;
      H1.x = - F.x by A3
        .= H2.x by A4;
      hence thesis;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem Th19:
  for X being non empty set, Y being non empty Subset of ExtREAL,
  F being Function of X,Y holds rng(- F) = - rng F
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  thus rng(- F) c= - rng F
  proof
    let y be set;
A1: dom F = X by FUNCT_2:def 1;
    assume
A2: y in rng(- F);
    then reconsider y as R_eal;
    dom(- F) = X by FUNCT_2:def 1;
    then consider a being set such that
A3: a in X and
A4: y = (- F).a by A2,FUNCT_1:def 3;
    reconsider a as Element of X by A3;
    y = - F.a by A4,Def4;
    then - y in rng F by A1,FUNCT_1:def 3;
    then - (- y) in - rng F;
    hence thesis;
  end;
  thus - rng F c= rng(- F)
  proof
    let y be set;
    assume
A5: y in - rng F;
    then reconsider y as R_eal;
A6: - y in - (- rng F) by A5;
    dom F = X by FUNCT_2:def 1;
    then consider a being set such that
A7: a in X and
A8: - y = F.a by A6,FUNCT_1:def 3;
    reconsider a as Element of X by A7;
    y = - F.a by A8;
    then
A9: y = (- F).a by Def4;
    dom (- F) = X by FUNCT_2:def 1;
    hence thesis by A9,FUNCT_1:def 3;
  end;
end;

theorem Th20:
  for X being non empty set, Y being non empty Subset of ExtREAL
  for F being Function of X,Y holds inf(- F) = - sup F & sup(- F) = - inf F
proof
  let X be non empty set;
  let Y be non empty Subset of ExtREAL;
  let F be Function of X,Y;
  thus inf(- F) = inf(- rng F) by Th19
    .= - sup F by Th14;
  thus sup(- F) = sup(- rng F) by Th19
    .= - inf F by Th15;
end;

::
::       Bounded Function of X,ExtREAL
::

definition
  let X be set;
  let Y be Subset of ExtREAL;
  let F be Function of X,Y;
  attr F is bounded_above means
  :Def5:
  sup F < +infty;
  attr F is bounded_below means
  :Def6:
  -infty < inf F;
end;

definition
  let X be set, Y be Subset of ExtREAL, F be Function of X,Y;
  attr F is bounded means
  :Def7:
  F is bounded_above bounded_below;
end;

registration
  let X be set;
  let Y be Subset of ExtREAL;
  cluster bounded -> bounded_above bounded_below for Function of X, Y;
  coherence by Def7;
  cluster bounded_above bounded_below -> bounded for Function of X, Y;
  coherence by Def7;
end;

theorem
  for X being non empty set, Y being non empty Subset of ExtREAL, F
  being Function of X,Y holds F is bounded iff sup F <+infty & -infty <inf F
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  thus F is bounded implies sup F <+infty & -infty <inf F by Def5,Def6;
  assume that
A1: sup F <+infty and
A2: -infty <inf F;
A3: F is bounded_below by A2,Def6;
  F is bounded_above by A1,Def5;
  hence thesis by A3;
end;

theorem Th22:
  for X being non empty set, Y being non empty Subset of ExtREAL,
  F being Function of X,Y holds F is bounded_above iff - F is bounded_below
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  hereby
    assume F is bounded_above;
    then sup F <+infty by Def5;
    then
A1: - (+infty) <- sup F by XXREAL_3:38;
    - (+infty) = -infty by XXREAL_3:def 3;
    then -infty <inf(- F) by A1,Th20;
    hence - F is bounded_below by Def6;
  end;
  assume - F is bounded_below;
  then -infty <inf(- F) by Def6;
  then - inf(- F) <- (-infty) by XXREAL_3:38;
  then - (- sup F) <- (-infty) by Th20;
  hence thesis by Def5,XXREAL_3:5;
end;

theorem Th23:
  for X being non empty set, Y being non empty Subset of ExtREAL,
  F being Function of X,Y holds F is bounded_below iff - F is bounded_above
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  hereby
    assume F is bounded_below;
    then -infty <inf F by Def6;
    then - inf F <- (-infty) by XXREAL_3:38;
    then sup(- F) <+infty by Th20,XXREAL_3:5;
    hence - F is bounded_above by Def5;
  end;
  assume - F is bounded_above;
  then sup(- F) <+infty by Def5;
  then - inf F <+infty by Th20;
  then
A1: - (+infty) <- (- inf F) by XXREAL_3:38;
  - (+infty) = -infty by XXREAL_3:def 3;
  hence thesis by A1,Def6;
end;

theorem
  for X being non empty set, Y being non empty Subset of ExtREAL, F
  being Function of X,Y holds F is bounded iff - F is bounded
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  hereby
    assume
A1: F is bounded;
    then
A2: - F is bounded_below by Th22;
    - F is bounded_above by A1,Th23;
    hence - F is bounded by A2;
  end;
  assume
A3: - F is bounded;
  then
A4: F is bounded_below by Th23;
  F is bounded_above by A3,Th22;
  hence thesis by A4;
end;

theorem
  for X being non empty set, Y being non empty Subset of ExtREAL, F
being Function of X,Y, x being Element of X holds -infty <= F.x & F.x <= +infty
  by XXREAL_0:4,5;

theorem
  for X being non empty set, Y being non empty Subset of ExtREAL, F
being Function of X,Y, x being Element of X st Y c= REAL holds -infty <F.x & F.
  x <+infty
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y, x be Element of X;
A1: -infty <= F.x by XXREAL_0:5;
  assume Y c= REAL;
  hence thesis by A1,XXREAL_0:1,4;
end;

theorem Th27:
  for X being non empty set, Y being non empty Subset of ExtREAL,
F being Function of X,Y, x being Element of X holds inf F <= F.x & F.x <= sup F
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y, x be Element of X;
  X = dom F by FUNCT_2:def 1;
  then F.x in rng F by FUNCT_1:def 3;
  hence thesis by XXREAL_2:3,4;
end;

theorem Th28:
  for X being non empty set, Y being non empty Subset of ExtREAL,
  F being Function of X,Y holds Y c= REAL implies (F is bounded_above iff sup F
  in REAL)
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  assume
A1: Y c= REAL;
  hereby
    set x = the Element of X;
    X = dom F by FUNCT_2:def 1;
    then
A2: F.x in rng F by FUNCT_1:def 3;
    rng F c= Y by RELAT_1:def 19;
    then F.x in Y by A2;
    then
A3: not sup F = -infty by A1,Th27,XXREAL_0:12;
    assume F is bounded_above;
    then
A4: sup F <+infty by Def5;
    sup F in REAL or sup F in {-infty,+infty} by XBOOLE_0:def 3;
    hence sup F in REAL by A4,A3,TARSKI:def 2;
  end;
  assume sup F in REAL;
  then sup F <+infty by XXREAL_0:9;
  hence thesis by Def5;
end;

theorem Th29:
  for X being non empty set, Y being non empty Subset of ExtREAL,
  F being Function of X,Y st Y c= REAL holds (F is bounded_below iff inf F in
  REAL)
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  assume
A1: Y c= REAL;
  thus F is bounded_below implies inf F in REAL
  proof
    set x = the Element of X;
    X = dom F by FUNCT_2:def 1;
    then
A2: F.x in rng F by FUNCT_1:def 3;
    rng F c= Y by RELAT_1:def 19;
    then F.x in Y by A2;
    then
A3: not inf F = +infty by A1,Th27,XXREAL_0:9;
    assume F is bounded_below;
    then
A4: -infty <inf F by Def6;
    inf F in REAL or inf F in {-infty,+infty} by XBOOLE_0:def 3;
    hence thesis by A4,A3,TARSKI:def 2;
  end;
  assume inf F in REAL;
  then -infty <inf F by XXREAL_0:12;
  hence thesis by Def6;
end;

theorem
  for X being non empty set, Y being non empty Subset of ExtREAL, F
being Function of X,Y st Y c= REAL holds (F is bounded iff inf F in REAL & sup
  F in REAL)
proof
  let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
  ,Y;
  assume
A1: Y c= REAL;
  hence F is bounded implies inf F in REAL & sup F in REAL by Th28,Th29;
  assume that
A2: inf F in REAL and
A3: sup F in REAL;
A4: F is bounded_below by A1,A2,Th29;
  F is bounded_above by A1,A3,Th28;
  hence thesis by A4;
end;

theorem Th31:
  for X being non empty set, Y,Z being non empty Subset of ExtREAL
  holds for F1 being Function of X,Y, F2 being Function of X,Z st F1 is
  bounded_above & F2 is bounded_above holds F1 + F2 is bounded_above
proof
  let X be non empty set, Y,Z be non empty Subset of ExtREAL;
  let F1 be Function of X,Y, F2 be Function of X,Z;
  assume that
A1: F1 is bounded_above and
A2: F2 is bounded_above;
A3: not sup F2 = +infty by A2,Def5;
A4: sup F1 in REAL & sup F2 in REAL implies sup F1 + sup F2 <+infty
  proof
    reconsider a = sup F1, b = sup F2 as R_eal;
    assume that
A5: sup F1 in REAL and
A6: sup F2 in REAL;
    reconsider a,b as Real by A5,A6;
    sup F1 + sup F2 = a + b by XXREAL_3:def 2;
    hence thesis by XXREAL_0:9;
  end;
A7: sup F1 in REAL & sup F2 = -infty implies sup F1 + sup F2 <+infty by
XXREAL_0:7,XXREAL_3:def 2;
A8: sup F1 = -infty & sup F2 = -infty implies sup F1 + sup F2 <+infty by
XXREAL_0:7,XXREAL_3:def 2;
A9: sup F1 = -infty & sup F2 in REAL implies sup F1 + sup F2 <+infty by
XXREAL_0:7,XXREAL_3:def 2;
A10: not sup F1 = +infty by A1,Def5;
  sup(F1 + F2) <+infty
  proof
    assume not sup(F1 + F2) <+infty;
    then not sup(F1 + F2) <= +infty or sup(F1 + F2) = +infty by XXREAL_0:1;
    hence thesis by A10,A3,A4,A7,A9,A8,Th17,XXREAL_0:4,XXREAL_3:def 1;
  end;
  hence thesis by Def5;
end;

theorem Th32:
  for X being non empty set, Y,Z being non empty Subset of ExtREAL
  holds for F1 being Function of X,Y, F2 being Function of X,Z st F1 is
  bounded_below & F2 is bounded_below holds F1 + F2 is bounded_below
proof
  let X be non empty set, Y,Z be non empty Subset of ExtREAL;
  let F1 be Function of X,Y, F2 be Function of X,Z;
  assume that
A1: F1 is bounded_below and
A2: F2 is bounded_below;
A3: not inf F2 = -infty by A2,Def6;
A4: inf F1 in REAL & inf F2 in REAL implies -infty <inf F1 + inf F2
  proof
    reconsider a = inf F1, b = inf F2 as R_eal;
    assume that
A5: inf F1 in REAL and
A6: inf F2 in REAL;
    reconsider a,b as Real by A5,A6;
    inf F1 + inf F2 = a + b by XXREAL_3:def 2;
    hence thesis by XXREAL_0:12;
  end;
A7: inf F1 in REAL & inf F2 = +infty implies -infty <inf F1 + inf F2 by
XXREAL_0:7,XXREAL_3:def 2;
A8: inf F1 = +infty & inf F2 = +infty implies -infty <inf F1 + inf F2 by
XXREAL_0:7,XXREAL_3:def 2;
A9: inf F1 = +infty & inf F2 in REAL implies -infty <inf F1 + inf F2 by
XXREAL_0:7,XXREAL_3:def 2;
A10: not inf F1 = -infty by A1,Def6;
  -infty <inf(F1 + F2)
  proof
    assume inf(F1 + F2) <= -infty;
    then not -infty <= inf(F1 + F2) or inf(F1 + F2) = -infty by XXREAL_0:1;
    hence thesis by A10,A3,A4,A7,A9,A8,Th18,XXREAL_0:6,XXREAL_3:def 1;
  end;
  hence thesis by Def6;
end;

theorem
  for X being non empty set, Y,Z being non empty Subset of ExtREAL holds
for F1 being Function of X,Y, F2 being Function of X,Z st F1 is bounded & F2 is
  bounded holds F1 + F2 is bounded
proof
  let X be non empty set, Y,Z be non empty Subset of ExtREAL;
  let F1 be Function of X,Y, F2 be Function of X,Z;
  assume that
A1: F1 is bounded and
A2: F2 is bounded;
A3: F1 + F2 is bounded_below by A1,A2,Th32;
  F1 + F2 is bounded_above by A1,A2,Th31;
  hence thesis by A3;
end;

theorem Th34:
  incl NAT is Function of NAT,ExtREAL &
  incl NAT is one-to-one & NAT = rng incl NAT &
  rng incl NAT is non empty Subset of ExtREAL
proof
  reconsider F = incl NAT as Function of NAT,ExtREAL by FUNCT_2:7,NUMBERS:31;
  rng F c= ExtREAL;
  hence thesis;
end;

::
::       Series of Elements of ExtREAL numbers
::

definition
  let D be non empty set, IT be Subset of D;
  redefine attr IT is countable means
  :Def8:
  IT is empty or ex F being Function of NAT,D st IT = rng F;
  compatibility
  proof
    thus IT is countable implies IT is empty or ex F being Function of NAT,D
    st IT = rng F
    proof
      assume that
A1:   IT is countable and
A2:   IT is not empty;
      consider f being Function such that
A3:   dom f = NAT and
A4:   IT c= rng f by A1,CARD_3:93;
      consider x being Element of D such that
A5:   x in IT by A2,SUBSET_1:4;
      set F = f|(f"IT) +* (NAT \ f"IT --> x);
A6:   rng F = IT & dom F = NAT
      proof
A7:     f"IT c= NAT by A3,RELAT_1:132;
A8:     dom(f|(f"IT)) = NAT /\ (f"IT) by A3,RELAT_1:61;
        per cases;
        suppose
A9:       NAT = f"IT;
          then
A10:      NAT \ f"IT = {} by XBOOLE_1:37;
          then dom(NAT \ f"IT --> x) = {};
          then dom(f|(f"IT)) /\ dom(NAT \ f"IT --> x) = {};
          then dom(f|(f"IT)) misses dom(NAT \ f"IT --> x) by XBOOLE_0:def 7;
          then F = (f|(f"IT)) \/ (NAT \ f"IT --> x) by FUNCT_4:31;
          hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:12
            .= rng(f|(f"IT)) \/ {} by A10
            .= f.:(f"IT) by RELAT_1:115
            .= IT by A4,FUNCT_1:77;
          thus dom F = dom(f|(f"IT)) \/ dom(NAT \ f"IT --> x) by FUNCT_4:def 1
            .= dom(f|(f"IT)) \/ {} by A10
            .= NAT by A8,A9;
        end;
        suppose
A11:      NAT <> f"IT;
A12:      now
            assume NAT \ f"IT is empty;
            then NAT c= f"IT by XBOOLE_1:37;
            hence contradiction by A7,A11,XBOOLE_0:def 10;
          end;
          dom(NAT \ f"IT --> x) = NAT \ f"IT by FUNCOP_1:13;
          then F = (f|(f"IT)) \/ (NAT \ f"IT --> x) by A8,FUNCT_4:31
,XBOOLE_1:89;
          hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:12
            .= rng(f|(f"IT)) \/ {x} by A12,FUNCOP_1:8
            .= f.:(f"IT) \/ {x} by RELAT_1:115
            .= IT \/ {x} by A4,FUNCT_1:77
            .= IT by A5,ZFMISC_1:40;
          thus dom F = dom(f|(f"IT)) \/ dom(NAT \ f"IT --> x) by FUNCT_4:def 1
            .= NAT /\ (f"IT) \/ (NAT \ f"IT) by A8,FUNCOP_1:13
            .= NAT by XBOOLE_1:51;
        end;
      end;
      then reconsider F as Function of NAT, D by FUNCT_2:def 1,RELSET_1:4;
      take F;
      thus thesis by A6;
    end;
    assume
A13: IT is empty or ex F being Function of NAT,D st IT = rng F;
    per cases;
    suppose
      IT is empty;
      hence thesis by CARD_4:1;
    end;
    suppose
      IT is not empty;
      then consider F being Function of NAT,D such that
A14:  IT = rng F by A13;
      dom F = NAT by FUNCT_2:def 1;
      hence thesis by A14,CARD_3:93;
    end;
  end;
end;

registration
  cluster countable for non empty Subset of ExtREAL;
  existence
  proof
    set F = the Function of NAT,ExtREAL;
    reconsider A = rng F as non empty Subset of ExtREAL;
    take A;
    assume A is non empty;
    thus thesis;
  end;
end;

definition
  mode Denum_Set_of_R_EAL is countable non empty Subset of ExtREAL;
end;

definition
  let IT be set;
  attr IT is nonnegative means
  :Def9:
  for x being R_eal holds x in IT implies 0. <= x;
end;

registration
  cluster nonnegative for Denum_Set_of_R_EAL;
  existence
  proof
    reconsider N = NAT as Denum_Set_of_R_EAL by Def8,Th34;
    take N;
    thus for x being R_eal holds x in N implies 0. <= x by NAT_1:2;
  end;
end;

definition
  mode Pos_Denum_Set_of_R_EAL is nonnegative Denum_Set_of_R_EAL;
end;

definition
  let D be Denum_Set_of_R_EAL;
  mode Num of D -> Function of NAT,ExtREAL means
    :Def10:
    D = rng it;
  existence by Def8;
end;

definition
  let D be Denum_Set_of_R_EAL;
  let N be Num of D;
  func Ser(D,N) -> Function of NAT,ExtREAL means
  :Def11:
  it.0 = N.0 &
  for n being Element of NAT for y being R_eal st y = it.n holds
  it.(n + 1) = y + N.(n + 1);
  existence
proof
  defpred P[set,set,set] means for a,b being R_eal,s being Element of NAT
  holds (s = $1 & a = $2 & b = $3 implies b = a + N.(s+1));
  reconsider A = N.0 as R_eal;
A1: for n being Element of NAT for x being Element of ExtREAL ex y being
  Element of ExtREAL st P[n,x,y]
  proof
    let n be Element of NAT;
    let x be Element of ExtREAL;
    reconsider y = x + N.(n+1) as R_eal;
    take y;
    thus thesis;
  end;
  consider F being Function of NAT,ExtREAL such that
A2: F.0 = A & for n being Element of NAT holds P[n,F.n,F.(n+1)] from
  RECDEF_1:sch 2(A1);
  take F;
  thus thesis by A2;
end;
  uniqueness
  proof
    let S1,S2 be Function of NAT,ExtREAL such that
A3: S1.0 = N.0 and
A4: for n being Element of NAT holds for y being R_eal st y = S1.n
    holds S1.(n + 1) = y + N.(n + 1) and
A5: S2.0 = N.0 and
A6: for n being Element of NAT holds for y being R_eal st y = S2.n
    holds S2.(n + 1) = y + N.(n + 1);
    defpred P[set] means S1.$1 = S2.$1;
    for n being set holds n in NAT implies P[n]
    proof
      let n be set;
      assume
A7:   n in NAT;
      then reconsider n as Element of REAL;
      reconsider n as Element of NAT by A7;
A8:   for k being Element of NAT st P[k] holds P[k+1]
      proof
        let k be Element of NAT;
        reconsider y2 = S2.k as R_eal;
        assume S1.k = S2.k;
        hence S1.(k + 1) = y2 + N.(k + 1) by A4
          .= S2.(k + 1) by A6;
      end;
A9:   P[0] by A3,A5;
      for k being Element of NAT holds P[k] from NAT_1:sch 1(A9, A8);
      then S1.n = S2.n;
      hence thesis;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem Th35:
  for D being Pos_Denum_Set_of_R_EAL, N being Num of D, n being
  Element of NAT holds 0. <= N.n
proof
  let D be Pos_Denum_Set_of_R_EAL, N be Num of D, n be Element of NAT;
  D = rng N by Def10;
  then N.n in D by FUNCT_2:4;
  hence thesis by Def9;
end;

theorem Th36:
  for D being Pos_Denum_Set_of_R_EAL, N being Num of D, n being
  Element of NAT holds Ser(D,N).n <= Ser(D,N).(n + 1) & 0. <= Ser(D,N).n
proof
  let D be Pos_Denum_Set_of_R_EAL, N be Num of D, n be Element of NAT;
  set F = Ser(D,N);
  defpred P[Element of NAT] means F.$1 <= F.($1 + 1) & 0. <= F.$1;
A1: F.(0 + 1) = F.0 + N.(1) by Def11;
A2: for k being Element of NAT st P[k] holds P[k + 1]
  proof
    let k be Element of NAT;
    assume that
A3: F.k <= F.(k + 1) and
A4: 0. <= F.k;
A5: 0. <= N.((k+1) + 1) by Th35;
    F.((k+1) + 1) = F.(k + 1) + N.((k+1) + 1) by Def11;
    hence thesis by A3,A4,A5,XXREAL_0:2,XXREAL_3:39;
  end;
  F.0 = N.0 by Def11;
  then
A6: P[0] by A1,Th35,XXREAL_3:39;
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A6,A2);
  hence thesis;
end;

theorem Th37:
  for D being Pos_Denum_Set_of_R_EAL, N being Num of D, n,m being
  Element of NAT holds Ser(D,N).n <= Ser(D,N).(n + m)
proof
  let D be Pos_Denum_Set_of_R_EAL, N be Num of D, n,m be Element of NAT;
  defpred P[Element of NAT] means Ser(D,N).n <= Ser(D,N).(n + $1);
A1: for k being Element of NAT st P[k] holds P[k + 1]
  proof
    let k be Element of NAT;
    Ser(D,N).(n + (k+1)) = Ser(D,N).((n + k) + 1);
    then
A2: Ser(D,N).(n + k) <= Ser(D,N).(n + (k+1)) by Th36;
    assume Ser(D,N).n <= Ser(D,N).(n + k);
    hence thesis by A2,XXREAL_0:2;
  end;
A3: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A3,A1);
  hence thesis;
end;

definition
  let D be Denum_Set_of_R_EAL;
  mode Set_of_Series of D -> non empty Subset of ExtREAL means
    ex N being Num of D st it = rng Ser(D,N);
  existence
  proof
    take rng Ser(D,the Num of D);
    thus thesis;
  end;
end;

definition
  let D be Pos_Denum_Set_of_R_EAL;
  let N be Num of D;
  func SUM(D,N) -> R_eal equals
  sup(rng Ser(D,N));
  coherence;
end;

definition
  let D be Pos_Denum_Set_of_R_EAL;
  let N be Num of D;
  pred D is_sumable N means
  SUM(D,N) in REAL;
end;

theorem Th38:
  for F being Function of NAT,ExtREAL holds rng F is Denum_Set_of_R_EAL
  by Def8;

definition
  let F be Function of NAT,ExtREAL;
  redefine func rng F -> Denum_Set_of_R_EAL;
  coherence by Th38;
end;

definition
  let F be Function of NAT,ExtREAL;
  func Ser(F) -> Function of NAT,ExtREAL means
  :Def15:
  for N being Num of rng F st N = F holds it = Ser(rng F,N);
  existence
  proof
    reconsider N = F as Num of rng F by Def10;
    take Ser(rng F,N);
    thus thesis;
  end;
  uniqueness
  proof
    reconsider N = F as Num of rng F by Def10;
    let S1,S2 be Function of NAT,ExtREAL such that
A1: for N being Num of rng F st N = F holds S1 = Ser(rng F,N) and
A2: for N being Num of rng F st N = F holds S2 = Ser(rng F,N);
    thus S1 = Ser(rng F,N) by A1
      .= S2 by A2;
  end;
end;

definition
  let R be Relation;
  attr R is nonnegative means
  :Def16:
  rng R is nonnegative;
end;

definition
  let F be Function of NAT,ExtREAL;
  func SUM(F) -> R_eal equals
  sup rng Ser(F);
  coherence;
end;

theorem Th39:
  for X being set, F being PartFunc of X,ExtREAL holds F is
  nonnegative iff for n being Element of X holds 0. <= F.n
proof
  let X be set, F be PartFunc of X,ExtREAL;
  hereby
    assume F is nonnegative;
    then
A1: rng F is nonnegative by Def16;
    let n be Element of X;
    per cases;
    suppose
      n in dom F;
      then F.n in rng F by FUNCT_1:def 3;
      hence 0. <= F.n by A1,Def9;
    end;
    suppose
      not n in dom F;
      hence 0. <= F.n by FUNCT_1:def 2;
    end;
  end;
  assume
A2: for n being Element of X holds 0. <= F.n;
  let y be R_eal;
  assume y in rng F;
  then ex x being set st x in dom F & y = F.x by FUNCT_1:def 3;
  hence thesis by A2;
end;

theorem Th40:
  for F being Function of NAT,ExtREAL, n being Element of NAT st F
  is nonnegative holds (Ser F).n <= (Ser F).(n + 1) & 0. <= (Ser F).n
proof
  let F be Function of NAT,ExtREAL, n be Element of NAT;
  reconsider N = F as Num of rng F by Def10;
  assume F is nonnegative;
  then
A1: rng F is Pos_Denum_Set_of_R_EAL by Def16;
  Ser F = Ser(rng F,N) by Def15;
  hence thesis by A1,Th36;
end;

theorem Th41:
  for F being Function of NAT,ExtREAL st F is nonnegative holds
  for n,m being Element of NAT holds Ser(F).n <= Ser(F).(n + m)
proof
  let F be Function of NAT,ExtREAL;
  reconsider N = F as Num of rng F by Def10;
  assume F is nonnegative;
  then
A1: rng F is Pos_Denum_Set_of_R_EAL by Def16;
  let n,m be Element of NAT;
  Ser(F) = Ser(rng F,N) by Def15;
  hence thesis by A1,Th37;
end;

theorem Th42:
  for F1,F2 being Function of NAT,ExtREAL st (for n being Element
of NAT holds F1.n <= F2.n) holds for n being Element of NAT holds Ser(F1).n <=
  Ser(F2).n
proof
  let F1,F2 be Function of NAT,ExtREAL;
  reconsider N2 = F2 as Num of rng F2 by Def10;
  defpred P[Element of NAT] means Ser(F1).$1 <= Ser(F2).$1;
  reconsider N1 = F1 as Num of rng F1 by Def10;
  assume
A1: for n being Element of NAT holds F1.n <= F2.n;
  let n be Element of NAT;
A2: Ser(F2) = Ser(rng F2,N2) by Def15;
  then
A3: Ser(F2).0 = F2.0 by Def11;
A4: Ser(F1) = Ser(rng F1,N1) by Def15;
A5: for k being Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT;
    assume
A6: Ser(F1).k <= Ser(F2).k;
A7: F1.(k+1) <= F2.(k+1) by A1;
A8: Ser(F2).(k+1) = Ser(F2).k + F2.(k+1) by A2,Def11;
    Ser(F1).(k+1) = Ser(F1).k + F1.(k+1) by A4,Def11;
    hence thesis by A6,A8,A7,XXREAL_3:36;
  end;
  Ser(F1).0 = F1.0 by A4,Def11;
  then
A9: P[0] by A1,A3;
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A9,A5);
  hence thesis;
end;

theorem Th43:
  for F1,F2 being Function of NAT,ExtREAL st (for n being Element
  of NAT holds F1.n <= F2.n) holds SUM(F1) <= SUM(F2)
proof
  let F1,F2 be Function of NAT,ExtREAL;
  assume
A1: for n being Element of NAT holds F1.n <= F2.n;
  for x being ext-real number st x in rng Ser(F1) holds ex y being
  ext-real number st y in rng Ser(F2) & x <= y
  proof
    let x be ext-real number;
A2: dom Ser(F1) = NAT by FUNCT_2:def 1;
    assume x in rng Ser(F1);
    then consider n being set such that
A3: n in NAT and
A4: x = Ser(F1).n by A2,FUNCT_1:def 3;
    reconsider n as Element of NAT by A3;
    reconsider y = Ser(F2).n as R_eal;
    take y;
    dom Ser(F2) = NAT by FUNCT_2:def 1;
    hence thesis by A1,A4,Th42,FUNCT_1:def 3;
  end;
  hence thesis by XXREAL_2:63;
end;

theorem Th44:
  for F being Function of NAT,ExtREAL holds Ser(F).0 = F.0 & for n
being Element of NAT, y being R_eal st y = Ser(F).n holds Ser(F).(n + 1) = y +
  F.(n + 1)
proof
  let F be Function of NAT,ExtREAL;
  reconsider N = F as Num of rng F by Def10;
  Ser F = Ser(rng F,N) by Def15;
  hence thesis by Def11;
end;

theorem Th45:
  for F being Function of NAT,ExtREAL st F is nonnegative holds (
  ex n being Element of NAT st F.n = +infty) implies SUM(F) = +infty
proof
  let F be Function of NAT,ExtREAL;
  assume
A1: F is nonnegative;
  given n being Element of NAT such that
A2: F.n = +infty;
A3: (ex k being Nat st n = k + 1) implies SUM(F) = +infty
  proof
    given k being Nat such that
A4: n = k + 1;
    reconsider k as Element of NAT by ORDINAL1:def 12;
    reconsider y = Ser(F).k as R_eal;
    reconsider x = Ser(F).(k + 1) as R_eal;
A5: Ser(F).(k + 1) = y + F.(k + 1) by Th44;
    Ser(F).k <> -infty by A1,Th40,XXREAL_0:6;
    then
A6: x = +infty by A2,A4,A5,XXREAL_3:def 2;
    then x is UpperBound of rng Ser(F) by XXREAL_2:41;
    hence thesis by A6,FUNCT_2:4,XXREAL_2:55;
  end;
  n = 0 implies SUM(F) = +infty
  proof
    reconsider x = Ser(F).0 as R_eal;
    assume n = 0;
    then
A7: Ser(F).0 = +infty by A2,Th44;
    then x is UpperBound of rng Ser(F) by XXREAL_2:41;
    hence thesis by A7,FUNCT_2:4,XXREAL_2:55;
  end;
  hence thesis by A3,NAT_1:6;
end;

definition
  let F be Function of NAT,ExtREAL;
  attr F is summable means
  :Def18:
  SUM(F) in REAL;
end;

theorem
  for F being Function of NAT,ExtREAL st F is nonnegative holds (ex n
  being Element of NAT st F.n = +infty) implies F is not summable
proof
  let F be Function of NAT,ExtREAL;
  assume
A1: F is nonnegative;
  assume ex n being Element of NAT st F.n = +infty;
  then not SUM(F) in REAL by A1,Th45;
  hence thesis by Def18;
end;

theorem
  for F1,F2 being Function of NAT,ExtREAL st F1 is nonnegative & (for n
  being Element of NAT holds F1.n <= F2.n) holds (F2 is summable implies F1 is
  summable)
proof
  let F1,F2 be Function of NAT,ExtREAL;
  assume F1 is nonnegative;
  then
A1: 0. <= Ser(F1).0 by Th40;
  Ser(F1).0 <= sup(rng Ser(F1)) by FUNCT_2:4,XXREAL_2:4;
  then
A2: SUM(F1) <> -infty by A1,XXREAL_0:2,6;
  assume
A3: for n being Element of NAT holds F1.n <= F2.n;
  assume F2 is summable;
  then SUM(F2) in REAL by Def18;
  then
A4: not SUM(F1) = +infty by A3,Th43,XXREAL_0:9;
  SUM(F1) in REAL or SUM(F1) in {-infty,+infty} by XBOOLE_0:def 3;
  hence thesis by A4,A2,Def18,TARSKI:def 2;
end;

theorem Th48:
  for F being Function of NAT,ExtREAL st F is nonnegative holds
for n being Nat st (for r being Element of NAT st n <= r holds F.r = 0.) holds
  SUM(F) = Ser(F).n
proof
  let F be Function of NAT,ExtREAL;
  assume
A1: F is nonnegative;
  let n be Nat;
  reconsider n9=n as Element of NAT by ORDINAL1:def 12;
  assume
A2: for r being Element of NAT st n <= r holds F.r = 0.;
A3: for r being Element of NAT st n <= r holds Ser(F).r <= Ser(F).n
  proof
    defpred P[Nat] means Ser(F).(n + $1) <= Ser(F).n;
    let r be Element of NAT;
    assume n <= r;
    then
A4: ex m being Nat st r = n + m by NAT_1:10;
A5: for s being Nat st P[s] holds P[s+1]
    proof
      let s be Nat;
      reconsider s9=s as Element of NAT by ORDINAL1:def 12;
      reconsider y = Ser(F).(n + s) as R_eal;
      n9 + (s9 + 1) = (n9 + s9) + 1;
      then
A6:   Ser(F).(n9 + (s9 + 1)) = y + F.(n9 + (s9 + 1)) by Th44;
      0 <= s+1 by NAT_1:2;
      then n + 0 <= n + (s+1) by XREAL_1:7;
      then
A7:   F.(n9 + (s9+1)) = 0. by A2;
      assume Ser(F).(n + s) <= Ser(F).n;
      hence thesis by A6,A7,XXREAL_3:4;
    end;
A8: P[0];
    for m being Nat holds P[m] from NAT_1:sch 2(A8,A5);
    hence thesis by A4;
  end;
A9: for r being Element of NAT st r <= n holds Ser(F).r <= Ser(F).n
  proof
    let r be Element of NAT;
    assume r <= n;
    then consider m being Nat such that
A10: n = r + m by NAT_1:10;
    reconsider m as Element of NAT by ORDINAL1:def 12;
    n = r + m by A10;
    hence thesis by A1,Th41;
  end;
  for y being ext-real number st y in rng Ser(F) holds y <= Ser(F).n
  proof
    let y be ext-real number;
A11: dom Ser(F) = NAT by FUNCT_2:def 1;
    assume y in rng Ser(F);
    then consider m being set such that
A12: m in NAT and
A13: y = Ser(F).m by A11,FUNCT_1:def 3;
    reconsider m as Element of NAT by A12;
    m <= n or n <= m;
    hence thesis by A3,A9,A13;
  end;
  then
A14: Ser(F).n is UpperBound of rng Ser(F) by XXREAL_2:def 1;
  Ser(F).n9 in rng Ser(F) by FUNCT_2:4;
  hence thesis by A14,XXREAL_2:55;
end;

theorem Th49:
  for F being Function of NAT,ExtREAL st (for n being Element of
NAT holds F.n in REAL) holds for n being Element of NAT holds Ser(F).n in REAL
proof
  let F be Function of NAT,ExtREAL;
  defpred P[Element of NAT] means Ser(F).$1 in REAL;
  assume
A1: for n being Element of NAT holds F.n in REAL;
A2: for s being Element of NAT st P[s] holds P[s+1]
  proof
    let s be Element of NAT;
    reconsider b = F.(s+1) as Real by A1;
    reconsider y = Ser(F).s as R_eal;
    assume Ser(F).s in REAL;
    then reconsider a = y as Real;
A3: y + F.(s+1) = a + b by XXREAL_3:def 2;
    Ser(F).(s+1) = y + F.(s+1) by Th44;
    hence thesis by A3;
  end;
  Ser(F).0 = F.0 by Th44;
  then
A4: P[0] by A1;
  thus for s being Element of NAT holds P[s] from NAT_1:sch 1(A4,A2);
end;

theorem
  for F being Function of NAT,ExtREAL st F is nonnegative & (ex n being
Element of NAT st (for k being Element of NAT st n <= k holds F.k = 0.) & (for
  k being Element of NAT st k <= n holds F.k <> +infty)) holds F is summable
proof
  let F be Function of NAT,ExtREAL;
  assume
A1: F is nonnegative;
  given n being Element of NAT such that
A2: for k being Element of NAT st n <= k holds F.k = 0. and
A3: for k being Element of NAT st k <= n holds F.k <> +infty;
  for s being Element of NAT holds F.s in REAL
  proof
    let s be Element of NAT;
A4: s <= n implies F.s in REAL
    proof
      0. <= F.s by A1,Th39;
      then
A5:   F.s <> -infty by XXREAL_0:6;
      assume s <= n;
      then
A6:   not F.s = +infty by A3;
      F.s in REAL or F.s in {-infty,+infty} by XBOOLE_0:def 3;
      hence thesis by A6,A5,TARSKI:def 2;
    end;
    n <= s implies F.s in REAL
    proof
      assume n <= s;
      then F.s = 0. by A2;
      hence thesis;
    end;
    hence thesis by A4;
  end;
  then
A7: Ser(F).n in REAL by Th49;
  SUM(F) = Ser(F).n by A1,A2,Th48;
  hence thesis by A7,Def18;
end;

:: Added by AK, 2006.02.06

theorem
  for X being set, F being PartFunc of X,ExtREAL holds F is nonnegative
  iff for n being set holds 0. <= F.n
proof
  let X be set, F be PartFunc of X,ExtREAL;
  hereby
    assume F is nonnegative;
    then
A1: rng F is nonnegative by Def16;
    let n be set;
    per cases;
    suppose
      n in dom F;
      then F.n in rng F by FUNCT_1:def 3;
      hence 0. <= F.n by A1,Def9;
    end;
    suppose
      not n in dom F;
      hence 0. <= F.n by FUNCT_1:def 2;
    end;
  end;
  assume
A2: for n being set holds 0. <= F.n;
  let y be R_eal;
  assume y in rng F;
  then ex x being set st x in dom F & y = F.x by FUNCT_1:def 3;
  hence thesis by A2;
end;

theorem
  for X being set, F being PartFunc of X,ExtREAL st for n being set st n
  in dom F holds 0. <= F.n holds F is nonnegative
proof
  let X be set, F be PartFunc of X,ExtREAL such that
A1: for n being set st n in dom F holds 0. <= F.n;
  let y be R_eal;
  assume y in rng F;
  then ex x being set st x in dom F & y = F.x by FUNCT_1:def 3;
  hence thesis by A1;
end;