The Mizar article:

Series of Positive Real Numbers. Measure Theory

by
Jozef Bialas

Received September 27, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: SUPINF_2
[ MML identifier index ]


environ

 vocabulary SUPINF_1, ARYTM_1, ARYTM_3, RLVECT_1, BOOLE, ORDINAL2, SEQ_2,
      FUNCT_1, RELAT_1, LATTICES, CARD_4, FUNCT_4, FUNCOP_1, SUPINF_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, SUPINF_1,
      RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_4, NAT_1, CARD_4;
 constructors REAL_1, SUPINF_1, NAT_1, CARD_4, FUNCOP_1, FUNCT_4, MEMBERED,
      XBOOLE_0;
 clusters SUPINF_1, RELSET_1, FUNCOP_1, FUNCT_1, ARYTM_3, FINSET_1, MEMBERED,
      ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, SUPINF_1, XBOOLE_0;
 theorems AXIOMS, TARSKI, REAL_1, SUPINF_1, FUNCT_1, FUNCT_2, NAT_1, RELSET_1,
      CARD_4, SUBSET_1, FUNCT_4, FUNCOP_1, RELAT_1, ZFMISC_1, XBOOLE_0,
      XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes SUPINF_1, FUNCT_2, RECDEF_1, NAT_1;

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

definition
   func 0. -> R_eal equals
:Def1: 0;
correctness by SUPINF_1:10;
end;

definition
  let x,y be R_eal;
func x + y -> R_eal means
:Def2:
  ex a,b being Real st x = a & y = b & it = a + b if x in REAL & y in REAL,
  it = +infty if x = +infty & y <> -infty or y = +infty & x <> -infty,
  it = -infty if x = -infty & y <> +infty or y = -infty & x <> +infty
  otherwise it = 0.;
existence
proof
 thus x in REAL & y in REAL implies
    ex IT being R_eal, a,b being Real st x = a & y = b & IT = a + b
  proof assume x in REAL & y in REAL;
    then reconsider a = x, b = y as Real;
      a+b is R_eal by SUPINF_1:10;
   hence thesis;
  end;
 thus thesis;
end;
uniqueness;
consistency by SUPINF_1:2,6;
 commutativity;
end;

theorem Th1:
   for x,y being R_eal holds
   for a,b being Real holds
   (x = a & y = b) implies (x + y = a + b)
proof let x,y be R_eal, a,b be Real;
 assume
A1:x = a & y = b;
  then ex a,b being Real st x = a & y = b & x + y = a + b by Def2;
 hence thesis by A1;
end;

theorem Th2:
 for x being R_eal holds
  x in REAL or x = +infty or x = -infty
proof let x be R_eal;
    x in REAL or x in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
 hence x in REAL or x = +infty or x = -infty by TARSKI:def 2;
end;

definition
   let x be R_eal;
   func - x -> R_eal means
:Def3: ex a being Real st x = a & it = - a if x in REAL,
     it = -infty if x = +infty
     otherwise it = +infty;
existence
proof
     x in REAL implies ex Z being R_eal st
      (ex a being Real st (x = a & Z = - a))
      proof
         assume x in REAL;
         then reconsider x as Real;
         reconsider Z = - x as R_eal by SUPINF_1:10;
         take Z;
         thus thesis;
      end;
      hence thesis;
end;
uniqueness;
 consistency by SUPINF_1:2;
 involutiveness
  proof let y,x be R_eal such that
A1: x in REAL implies ex a being Real st x = a & y = - a and
A2: x = +infty implies y = -infty and
A3: not x in REAL & x <> +infty implies y = +infty;
   thus y in REAL implies ex a being Real st y = a & x = - a
    proof assume y in REAL;
      then consider a being Real such that
A4:    x = a and
A5:    y = - a by A1,A2,A3,SUPINF_1:2,6;
     take -a;
     thus thesis by A4,A5;
    end;
   thus y = +infty implies x = -infty by A1,A2,Th2,SUPINF_1:2;
   thus thesis by A1,A3;
  end;
end;

definition
  let x,y be R_eal;
func x - y -> R_eal equals
:Def4: x + -y;
 coherence;
end;

theorem Th3:
   for x being R_eal, a being Real st x = a holds - x = - a
proof
   let x be R_eal, a be Real;
   assume
A1: x = a;
    then ex a being Real st x = a & - x = - a by Def3;
  hence thesis by A1;
end;

theorem Th4:
 - -infty = +infty
proof
 thus thesis by Def3,SUPINF_1:6,14;
end;

theorem Th5:
   for x,y being R_eal holds
   for a,b being Real holds
   (x = a & y = b) implies (x - y = a - b)
proof
   let x,y be R_eal;
   let a,b be Real;
   assume
A1: x = a;
 assume y = b;
  then A2: -y = -b by Th3;
 thus x - y = x + -y by Def4
        .= a + -b by A1,A2,Th1
        .= a - b by XCMPLX_0:def 8;
end;

theorem Th6:
   for x being R_eal holds
    x <> +infty implies +infty - x = +infty & x - +infty = -infty
proof
   let x be R_eal;
   assume
A1: x <> +infty;
then A2: -x <> -infty by Th4;
 thus +infty - x = +infty + -x by Def4
      .= +infty by A2,Def2;
    - +infty = -infty by Def3;
 hence x - +infty = x + -infty by Def4
      .= -infty by A1,Def2;
end;

theorem Th7:
   for x being R_eal holds
    x <> -infty implies -infty - x = -infty & x - -infty = +infty
proof
   let x be R_eal;
   assume
A1: x <> -infty;
A2: now assume -x = +infty;
      then --x = -infty by Def3;
     hence contradiction by A1;
    end;
 thus -infty - x = -infty + -x by Def4
      .= -infty by A2,Def2;
 thus x - -infty = x + +infty by Def4,Th4
      .= +infty by A1,Def2;
end;

theorem Th8:
   for x,s being R_eal holds
   x + s = +infty implies x = +infty or s = +infty
proof
   let x,s be R_eal;
   assume
A1:x + s = +infty;
   assume
A2:not (x = +infty or s = +infty);
     (x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(x in REAL & s in REAL) or (x in REAL & s = -infty) or
   (x = -infty & s in REAL) or (x = -infty & s = -infty) by A2,TARSKI:def 2;
    not(x in REAL & s in REAL)
   proof
      assume x in REAL & s in REAL;
      then reconsider a = x, b = s as Real;
         x + s = a + b by Th1;
      hence thesis by A1,SUPINF_1:2;
   end;
   hence thesis by A1,A2,A3,Def2;
end;

theorem Th9:
   for x,s being R_eal holds
   x + s = -infty implies (x = -infty or s = -infty)
proof
   let x,s be R_eal;
   assume
A1:x + s = -infty;
   assume
A2:not (x = -infty or s = -infty);
     (x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
   then A3:(x in REAL & s in REAL) or (x in REAL & s = +infty) or
   (x = +infty & s in REAL) or (x = +infty & s = +infty) by A2,TARSKI:def 2;
    not(x in REAL & s in REAL)
   proof
      assume x in REAL & s in REAL;
      then reconsider a = x, b = s as Real;
     x + s = a + b by Th1;
      hence thesis by A1,SUPINF_1:6;
   end;
   hence thesis by A1,A2,A3,Def2;
end;

theorem Th10:
   for x,s being R_eal holds
   x - s = +infty implies (x = +infty or s = -infty)
proof
   let x,s be R_eal;
   assume
A1:x - s = +infty;
   assume
A2:not (x = +infty or s = -infty);
     (x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
   then A3:(x in REAL & s in REAL) or (x in REAL & s = +infty) or
   (x = -infty & s in REAL) or (x = -infty & s = +infty) by A2,TARSKI:def 2;
    not (x in REAL & s in REAL)
   proof
      assume x in REAL & s in REAL;
      then consider a,b being Real such that
   A4:a = x & b = s;
     x - s = a - b by A4,Th5;
      hence thesis by A1,SUPINF_1:2;
   end;
   hence thesis by A1,A2,A3,Th6,Th7;
end;

theorem Th11:
   for x,s being R_eal holds
   x - s = -infty implies (x = -infty or s = +infty)
proof
   let x,s be R_eal;
   assume
A1:x - s = -infty;
   assume
A2:not (x = -infty or s = +infty);
     (x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(x in REAL & s in REAL) or (x in REAL & s = -infty) or
   (x = +infty & s in REAL) or (x = +infty & s = -infty) by A2,TARSKI:def 2;
    not(x in REAL & s in REAL)
   proof
      assume
     x in REAL & s in REAL;
      then consider a,b being Real such that
   A4:a = x & b = s;
     x - s = a - b by A4,Th5;
      hence thesis by A1,SUPINF_1:6;
   end;
   hence thesis by A1,A2,A3,Th6,Th7;
end;

theorem Th12:
   for x,s being R_eal holds
   (not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
   x + s in REAL) implies (x in REAL & s in REAL)
proof
   let x,s be R_eal;
   assume
A1:(not ((x = +infty & s = -infty) or (x = -infty & s = +infty
)) & x + s in REAL);
   assume
A2:not (x in REAL & s in REAL);
     (x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
   then (x in REAL or x = -infty or x = +infty) &
        (s in REAL or s = -infty or s = +infty) by TARSKI:def 2;

   hence thesis by A1,A2,Def2;
end;

theorem Th13:
   for x,s being R_eal holds
   (not ((x = +infty & s = +infty) or (x = -infty & s = -infty)) &
   x - s in REAL) implies (x in REAL & s in REAL)
proof
   let x,s be R_eal;
   assume
A1:(not ((x = +infty & s = +infty) or (x = -infty & s = -infty
)) & x - s in REAL);
   assume
A2:not (x in REAL & s in REAL);
     (x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then (x in REAL or x = -infty or x = +infty) &
   (s in REAL or s = -infty or s = +infty) by TARSKI:def 2;
   hence thesis by A1,A2,Th6,Th7,SUPINF_1:2,6;
end;

theorem Th14:
   for x,y,s,t being R_eal holds
   not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
   not ((y = +infty & t = -infty) or (y = -infty & t = +infty
)) & x <=' y & s <=' t implies
   x + s <=' y + t
proof
   let x,y,s,t be R_eal;
   assume
A1:not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
   not ((y = +infty & t = -infty) or (y = -infty & t = +infty
)) & x <=' y & s <=' t;
   consider a,b being R_eal such that
A2:a = x + s & b = y + t;
     (a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(a in REAL & b in REAL) or (a in REAL & b = +infty) or
(a in REAL & b = -infty) or
   (a = +infty & b in REAL) or (a = +infty & b = +infty) or (a = +infty & b =
-infty) or
   (a = -infty & b in REAL) or (a = -infty & b = +infty) or (a = -infty & b =
-infty) by TARSKI:def 2;
A4:(a in REAL & b in REAL) implies a <=' b
   proof
      assume a in REAL & b in REAL;
   then A5:x is Real & y is Real & s is Real & t is Real by A1,A2,Th12;
   then A6:ex Ox,Oy being Real st (Ox = x & Oy = y & Ox <= Oy) by A1,SUPINF_1:
16;
     ex Os,Ot being Real st (Os = s & Ot = t & Os <= Ot) by A1,A5,SUPINF_1:16;
      then consider Ox,Oy,Os,Ot being Real such that
   A7:Ox = x & Oy = y & Os = s & Ot = t & Ox <= Oy & Os <= Ot by A6;
   A8:Ox + Os <= Os + Oy by A7,AXIOMS:24;
     Os + Oy <= Ot + Oy by A7,AXIOMS:24;
   then A9:Ox + Os <= Oy + Ot by A8,AXIOMS:22;
        x + s = Ox + Os & y + t = Oy + Ot by A7,Th1;
      hence thesis by A2,A9,SUPINF_1:16;
   end;
A10:(a in REAL & b = -infty) implies a <=' b
   proof
      assume a in REAL & b = -infty;
   then y = -infty or t = -infty by A2,Th9;
   then x = -infty or s = -infty by A1,SUPINF_1:23;
      then a = -infty by A1,A2,Def2;
      hence thesis by SUPINF_1:21;
   end;
A11:(a = +infty & b in REAL) implies a <=' b
   proof
      assume a = +infty & b in REAL;
   then x = +infty or s = +infty by A2,Th8;
   then y = +infty or t = +infty by A1,SUPINF_1:24;
      then b = +infty by A1,A2,Def2;
      hence thesis by SUPINF_1:20;
   end;
    not(a = +infty & b = -infty)
   proof
      assume
   A12:a = +infty & b = -infty;
   then A13:y = -infty or t = -infty by A2,Th9;
     x = +infty or s = +infty by A2,A12,Th8;
      hence thesis by A1,A13,SUPINF_1:14,24;
   end;
   hence thesis by A2,A3,A4,A10,A11,SUPINF_1:20,21;
end;

theorem
     for x,y,s,t being R_eal holds
   not ((x = +infty & t = +infty) or (x = -infty & t = -infty)) &
   not ((y = +infty & s = +infty) or (y = -infty & s = -infty
)) & x <=' y & s <=' t implies
   x - t <=' y - s
proof
   let x,y,s,t be R_eal;
   assume
A1:not ((x = +infty & t = +infty) or (x = -infty & t = -infty)) &
   not ((y = +infty & s = +infty) or (y = -infty & s = -infty
)) & x <=' y & s <=' t;
   consider a,b being R_eal such that
A2:a = x - t & b = y - s;
     (a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(a in REAL & b in REAL) or (a in REAL & b = +infty) or
(a in REAL & b = -infty) or
   (a = +infty & b in REAL) or (a = +infty & b = +infty) or (a = +infty & b =
-infty) or
   (a = -infty & b in REAL) or (a = -infty & b = +infty) or (a = -infty & b =
-infty) by TARSKI:def 2;
A4:(a in REAL & b in REAL) implies a <=' b
   proof
      assume a in REAL & b in REAL;
   then A5:x is Real & y is Real & s is Real & t is Real by A1,A2,Th13;
   then A6:ex Ox,Oy being Real st (Ox = x & Oy = y & Ox <= Oy) by A1,SUPINF_1:
16;
     ex Os,Ot being Real st (Os = s & Ot = t & Os <= Ot) by A1,A5,SUPINF_1:16;
      then consider Ox,Oy,Os,Ot being Real such that
   A7:Ox = x & Oy = y & Os = s & Ot = t & Ox <= Oy & Os <= Ot by A6;
A8:   - Ot <= - Os by A7,REAL_1:50;
        Ox + (- Ot) = Ox - Ot & Oy + (- Os) = Oy - Os by XCMPLX_0:def 8;
      then A9:Ox - Ot <= Oy - Os by A7,A8,REAL_1:55;
         x - t = Ox - Ot & y - s = Oy - Os by A7,Th5;
       hence thesis by A2,A9,SUPINF_1:16;
   end;
A10:(a in REAL & b = -infty) implies a <=' b
   proof
      assume
   A11:a in REAL & b = -infty;
   then A12:x in REAL & t in REAL by A1,A2,Th13;
     y = -infty or s = +infty by A2,A11,Th11;
      hence thesis by A1,A12,SUPINF_1:2,6,23,24;
   end;
A13:(a = +infty & b in REAL) implies a <=' b
   proof
      assume
   A14:a = +infty & b in REAL;
   then A15:y in REAL & s in REAL by A1,A2,Th13;
     x = +infty or t = -infty by A2,A14,Th10;
      hence thesis by A1,A15,SUPINF_1:2,6,23,24;
   end;
    not(a = +infty & b = -infty)
   proof
      assume
   A16:a = +infty & b = -infty;
   then A17:y = -infty or s = +infty by A2,Th11;
     x = +infty or t = -infty by A2,A16,Th10;
      hence thesis by A1,A17,SUPINF_1:14,23,24;
   end;
   hence thesis by A2,A3,A4,A10,A13,SUPINF_1:20,21;
end;

Lm1:
 for x being R_eal holds
  -x in REAL iff x in REAL
  proof let x be R_eal;
   hereby assume -x in REAL;
     then reconsider a = -x as Real;
       -a in REAL;
     then --x in REAL by Th3;
    hence x in REAL;
   end;
   assume x in REAL;
    then reconsider a = x as Real;
      -x = -a by Th3;
   hence thesis;
  end;

Lm2:
   for x,y being R_eal holds
   x <=' y implies - y <=' - x
proof
   let x,y be R_eal;
   assume
A1:   x <=' y;
 per cases;
 case that
A2: -y in REAL and
A3: -x in REAL;
A4: y in REAL by A2,Lm1;
  then consider b being Real such that
A5: y = b and
A6: -y = - b by Def3;
A7: x in REAL by A3,Lm1;
  then consider a being Real such that
A8: x = a and
A9: -x = - a by Def3;
 take -b,-a;
 thus -b = -y & -a = -x by A6,A9;
    ex p,q being Real st p = x & q = y & p <= q by A1,A4,A7,SUPINF_1:def 7;
 hence -b <= -a by A5,A8,REAL_1:50;
 case not(-y in REAL & -x in REAL);
  then not(y in REAL & x in REAL) by Lm1;
  then x = -infty or y = +infty by A1,SUPINF_1:def 7;
 hence -y = -infty or -x = +infty by Th4;
end;

theorem Th16:
   for x,y being R_eal holds
   x <=' y iff - y <=' - x
proof let x,y be R_eal;
 thus x <=' y implies - y <=' - x by Lm2;
     - y <=' - x implies --x <=' --y by Lm2;
 hence thesis;
end;

theorem
    for x,y being R_eal holds
   x <' y iff - y <' - x by Th16;

theorem Th18:
   for x being R_eal holds x + 0. = x & 0. + x = x
proof
   let x be R_eal;
A1:x in REAL or x = -infty or x = +infty by Th2;
A2:x in REAL implies x + 0. =x & 0. + x = x
   proof
      assume x in REAL;
      then reconsider a = x as Real;
       x + 0. = a + 0 by Def1,Def2
           .= x;
    hence thesis;
   end;
     not 0. = -infty & not 0. = +infty by Def1,SUPINF_1:2,6;
   hence thesis by A1,A2,Def2;
end;

theorem
     -infty <'0. & 0. <'+infty
proof
A1:-infty <=' 0. & 0. <=' +infty by SUPINF_1:20,21;
     not 0. = +infty & not 0. = -infty by Def1,SUPINF_1:2,6;
   hence thesis by A1,SUPINF_1:22;
end;

theorem Th20:
   for x,y,z being R_eal holds
   0. <=' z & 0. <=' x & y = x + z implies x <=' y
proof
   let x,y,z be R_eal;
   assume
A1:0. <=' z & 0. <=' x & y = x + z;
  not 0. = -infty & not 0. = +infty by Def1,SUPINF_1:2,6;
   then A2:not z = -infty & not x = -infty by A1,SUPINF_1:23;
     x in REAL \/ {-infty,+infty} & z in REAL \/
 {-infty,+infty} by SUPINF_1:def 5;
   then A3: (x in REAL or x in {-infty,+infty}) & (z in REAL or
   z in {-infty,+infty}) by XBOOLE_0:def 2;
A4:z in REAL implies x <=' y
   proof
      assume
   A5:z in REAL;
   A6:x in REAL implies x <=' y
      proof
         assume
      A7:x in REAL;
         consider c,b being Real such that
     A8:c = 0. & b = z & c <= b by A1,A5,Def1,SUPINF_1:16;
         consider a being Real such that
     A9:a = x by A7;
     A10:y = a + b by A1,A8,A9,Th1;
         then consider d being Real such that
     A11:d = y;
           -b <= 0 by A8,Def1,REAL_1:26,50;
         then d + (-b) <= 0 + d by AXIOMS:24;
         then a + (b + (-b)) <= d by A10,A11,XCMPLX_1:1;
         then a + 0 <= d by XCMPLX_0:def 6;
         hence thesis by A9,A11,SUPINF_1:16;
      end;
        x = +infty implies x <=' y by A1,A2,Def2;
      hence thesis by A2,A3,A6,TARSKI:def 2;
   end;
     z = +infty implies x <=' y
   proof
      assume z = +infty;
      then y = +infty by A1,A2,Def2;
      hence thesis by SUPINF_1:20;
   end;
   hence thesis by A2,A3,A4,TARSKI:def 2;
end;

Lm3:
   for x,y,s,t being R_eal holds
   0. <=' x & 0. <=' s & x <=' y & s <=' t implies
   x + s <=' y + t
proof
   let x,y,s,t be R_eal;
   assume
A1:0. <=' x & 0. <=' s & x <=' y & s <=' t;
     not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
   not ((y = +infty & t = -infty) or (y = -infty & t = +infty))
   proof
        0. <=' y & 0. <=' t by A1,SUPINF_1:29;
      hence thesis by A1,Def1,SUPINF_1:17;
   end;
   hence thesis by A1,Th14;
end;

theorem Th21:
   for x being R_eal holds x in NAT implies 0. <=' x
proof
   let x be R_eal;
   assume
  x in NAT;
   then reconsider x as Nat;
     0 <= x by NAT_1:18;
   hence thesis by Def1,SUPINF_1:16;
end;

::
::       operations " + "," - " in SUBDOMAIN of ExtREAL
::

definition
   let X,Y be non empty Subset of ExtREAL;
   func X + Y -> Subset of ExtREAL means
:Def5:for z being R_eal holds
         z in it iff ex x,y being R_eal st (x in X & y in Y & z = x + y);
existence
proof
 defpred P[R_eal] means
   ex x,y being R_eal st x in X & y in Y & $1 = x + y;
   consider Z being Subset of REAL \/ {-infty,+infty} such that
A1:for z being R_eal holds z in Z iff P[z] from SepR_eal;
   reconsider Z as Subset of ExtREAL by SUPINF_1:def 6;
   consider x being Element of X;
   consider y being Element of Y;
   reconsider x,y as R_eal;
     x + y = x + y;
   then reconsider Z as non empty set by A1;
   reconsider Z as non empty Subset of ExtREAL;
   take Z;
   thus thesis by A1;
end;
uniqueness
proof
   let Z1,Z2 be Subset of ExtREAL such that
A2:for z being R_eal holds
   z in Z1 iff ex x,y being R_eal st (x in X & y in Y & z = x + y) and
A3:for z being R_eal holds
   z in Z2 iff ex x,y being R_eal st (x in X & y in Y & z = x + y);
     for z being set holds
   z in Z1 iff z in Z2
   proof
      let z be set;
      hereby assume
      A4:z in Z1;
         then reconsider z' = z as R_eal;
           ex x,y being R_eal st (x in X & y in Y & z' = x + y) by A2,A4;
         hence z in Z2 by A3;
      end;
         assume
      A5:z in Z2;
         then reconsider z as R_eal;
           ex x,y being R_eal st (x in X & y in Y & z = x + y) by A3,A5;
         hence thesis by A2;
   end;
   hence thesis by TARSKI:2;
end;
end;

definition
   let X,Y be non empty Subset of ExtREAL;
   cluster X + Y -> non empty;
coherence
proof
   consider x being Element of X;
   consider y being Element of Y;
   reconsider x,y as R_eal;
     x + y = x + y;
   hence thesis by Def5;
end;
end;

definition
   let X be non empty Subset of ExtREAL;
   func - X -> Subset of ExtREAL means
:Def6:for z being R_eal holds
         z in it iff ex x being R_eal st (x in X & z = - x);
existence
proof
  defpred P[R_eal] means
   ex x being R_eal st x in X & $1 = - x;
   consider Z being Subset of REAL \/ {-infty,+infty} such that
A1:for z being R_eal holds z in Z iff P[z] from SepR_eal;
   reconsider Z as Subset of ExtREAL by SUPINF_1:def 6;
   consider x being Element of X;
   reconsider x as R_eal;
     -x = -x;
   then reconsider Z as non empty set by A1;
   reconsider Z as non empty Subset of ExtREAL;
   take Z;
   thus thesis by A1;
end;
uniqueness
proof
   let Z1,Z2 be Subset of ExtREAL such that
A2:for z being R_eal holds z in Z1 iff
   ex x being R_eal st (x in X & z = - x) and
A3:for z being R_eal holds z in Z2 iff
   ex x being R_eal st (x in X & z = - x);
     for z being set holds z in Z1 iff z in Z2
   proof
      let z be set;
   A4:z in Z1 implies z in Z2
      proof
         assume
      A5:z in Z1;
         then reconsider z as R_eal;
           ex x being R_eal st (x in X & z = - x) by A2,A5;
         hence thesis by A3;
      end;
        z in Z2 implies z in Z1
      proof
         assume
      A6:z in Z2;
         then reconsider z as R_eal;
           ex x being R_eal st (x in X & z = - x) by A3,A6;
         hence thesis by A2;
      end;
      hence thesis by A4;
   end;
   hence thesis by TARSKI:2;
end;
end;

definition
   let X be non empty Subset of ExtREAL;
   cluster - X -> non empty;
coherence
proof
   consider x being Element of X;
   reconsider x as R_eal;
     - x = - x;
   hence thesis by Def6;
end;
end;

theorem Th22:
   for X being non empty Subset of ExtREAL holds
   - (- X) = X
proof
   let X be non empty Subset of ExtREAL;
  for z being R_eal holds
   z in X iff ex x being R_eal st (x in - X & z = - x)
   proof
      let z be R_eal;
   A1:z in X implies ex x being R_eal st (x in - X & z = - x)
      proof
         assume
      A2:z in X;
         set x = - z;
      A3:z = - x;
           x in - X by A2,Def6;
         hence thesis by A3;
      end;
        (ex x being R_eal st (x in - X & z = - x)) implies z in X
      proof
         given x being R_eal such that
      A4:x in - X & z = - x;
            ex a being R_eal st a in X & x = - a by A4,Def6;
         hence thesis by A4;
      end;
      hence thesis by A1;
   end;
   hence thesis by Def6;
end;

theorem Th23:
   for X being non empty Subset of ExtREAL holds
   for z being R_eal holds
   z in X iff - z in - X
proof
   let X be non empty Subset of ExtREAL;
   let z be R_eal;
     - z in - X implies z in X
   proof
     assume - z in - X;
      then consider x being R_eal such that
   A1:x in X & - z = - x by Def6;
        - (- z) = z & - (- x) = x;
      hence thesis by A1;
   end;
   hence thesis by Def6;
end;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y iff - X c= - Y
proof
   let X,Y be non empty Subset of ExtREAL;
   hereby assume
   A1:X c= Y;
     thus - X c= - Y
     proof
      let x be set;
      assume
   A2:x in - X;
      then reconsider x as R_eal;
        - x in - (- X) by A2,Th23;
      then - x in X by Th22;
      then - (- x) in - Y by A1,Th23;
      hence thesis;
     end;
   end;
   assume
A3:- X c= - Y;
   let x be set;
   assume
A4:x in X;
   then reconsider x as R_eal;
     - x in - X by A4,Th23;
   hence thesis by A3,Th23;
end;

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;
      assume
   A2:z in REAL;
        - z in REAL \/ {-infty,+infty} by SUPINF_1:def 5;
      then - z in REAL or - z in {-infty,+infty} by XBOOLE_0:def 2;
      then - z in REAL or - z = -infty or - z = +infty by TARSKI:def 2;
      then - z in REAL or - (- z) = +infty or - (- z) = -infty by Th4;
      hence - z in REAL by A2,SUPINF_1:2,6;
   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;

theorem Th26:
   for X,Y being non empty Subset of ExtREAL holds
   (not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
   not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty
)) implies
   sup (X + Y) <=' sup X + sup Y
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
   not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty);
     for z being R_eal holds
   z in X + Y implies z <=' sup X + sup Y
   proof
      let z be R_eal;
      assume
     z in X + Y;
      then consider x,y being R_eal such that
   A2:x in X & y in Y & z = x + y by Def5;
        x <=' sup X & y <=' sup Y by A2,SUPINF_1:76;
      hence thesis by A1,A2,Th14;
   end;
   then sup X + sup Y is majorant of X + Y by SUPINF_1:def 9;
   hence thesis by SUPINF_1:def 16;
end;

theorem Th27:
   for X,Y being non empty Subset of ExtREAL holds
   (not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
    not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty
)) implies
   inf X + inf Y <=' inf (X + Y)
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
   not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty);
     for z being R_eal holds
   z in X + Y implies inf X + inf Y <=' z
   proof
      let z be R_eal;
      assume z in X + Y;
      then consider x,y being R_eal such that
   A2:x in X & y in Y & z = x + y by Def5;
        inf X <=' x & inf Y <=' y by A2,SUPINF_1:79;
      hence thesis by A1,A2,Th14;
   end;
   then inf X + inf Y is minorant of X + Y by SUPINF_1:def 10;
   hence thesis by SUPINF_1:def 17;
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
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X is bounded_above & Y is bounded_above;
     not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
   not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty)
   proof
      consider UBx being majorant of X such that
   A2:UBx in REAL by A1,SUPINF_1:def 11;
      consider UBy being majorant of Y such that
   A3:UBy in REAL by A1,SUPINF_1:def 11;
   A4:not +infty in X
      proof
         assume +infty in X;
         then +infty <=' UBx by SUPINF_1:def 9;
         hence contradiction by A2,SUPINF_1:2,24;
      end;
   A5:not +infty in Y
      proof
         assume +infty in Y;
         then +infty <=' UBy by SUPINF_1:def 9;
         hence contradiction by A3,SUPINF_1:2,24;
      end;
   A6:not sup X = +infty
      proof
         assume sup X = +infty;
         then +infty <=' UBx by SUPINF_1:def 16;
         hence contradiction by A2,SUPINF_1:2,24;
      end;
     not sup Y = +infty
      proof
         assume sup Y = +infty;
         then +infty <=' UBy by SUPINF_1:def 16;
         hence contradiction by A3,SUPINF_1:2,24;
      end;
      hence thesis by A4,A5,A6;
   end;
   hence thesis by Th26;
end;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   X is bounded_below & Y is bounded_below implies
   inf X + inf Y <=' inf (X + Y)
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X is bounded_below & Y is bounded_below;
     not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
   not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty)
   proof
      consider LBx being minorant of X such that
   A2:LBx in REAL by A1,SUPINF_1:def 12;
      consider LBy being minorant of Y such that
   A3:LBy in REAL by A1,SUPINF_1:def 12;
   A4:not -infty in X
      proof
         assume -infty in X;
         then LBx <=' -infty by SUPINF_1:def 10;
         hence contradiction by A2,SUPINF_1:6,23;
      end;
   A5:not -infty in Y
      proof
         assume -infty in Y;
         then LBy <=' -infty by SUPINF_1:def 10;
         hence contradiction by A3,SUPINF_1:6,23;
      end;
   A6:not inf X = -infty
      proof
         assume inf X = -infty;
         then LBx <=' -infty by SUPINF_1:def 17;
         hence contradiction by A2,SUPINF_1:6,23;
      end;
     not inf Y = -infty
      proof
         assume inf Y = -infty;
         then LBy <=' -infty by SUPINF_1:def 17;
         hence contradiction by A3,SUPINF_1:6,23;
      end;
      hence thesis by A4,A5,A6;
   end;
   hence thesis by Th27;
end;

theorem Th30:
   for X being non empty Subset of ExtREAL holds
   for a being R_eal holds
   a is majorant of X iff - a is minorant of - X
proof
   let X be non empty Subset of ExtREAL;
   let a be R_eal;
    hereby assume
   A1:a is majorant of X;
        - a is minorant of - X
      proof
           for x being R_eal holds (x in - X implies -a <=' x)
         proof
            let x be R_eal;
            assume x in - X;
            then - x in - (- X) by Th23;
            then - x in X by Th22;
            then - x <=' a by A1,SUPINF_1:def 9;
            then - a <=' - (- x) by Th16;
            hence thesis;
         end;
         hence thesis by SUPINF_1:def 10;
      end;
      hence - a is minorant of - X;
   end;
      assume
   A2:- a is minorant of - X;
           for x being R_eal holds (x in X implies x <='a)
         proof
            let x be R_eal;
            assume x in X;
            then - x in - X by Th23;
            then - a <=' - x by A2,SUPINF_1:def 10;
            hence thesis by Th16;
         end;
         hence thesis by SUPINF_1:def 9;
end;

theorem Th31:
   for X being non empty Subset of ExtREAL holds
   for a being R_eal holds
   a is minorant of X iff - a is majorant of - X
proof
   let X be non empty Subset of ExtREAL;
   let a be R_eal;
   hereby assume
   A1:a is minorant of X;
        - a is majorant of - X
      proof
           for x being R_eal holds (x in - X implies x <=' - a)
         proof
            let x be R_eal;
            assume x in - X;
            then - x in - (- X) by Th23;
            then - x in X by Th22;
            then a <=' - x by A1,SUPINF_1:def 10;
            then - (- x) <=' - a by Th16;
            hence thesis;
         end;
         hence thesis by SUPINF_1:def 9;
      end;
      hence - a is majorant of - X;
   end;
      assume
   A2:- a is majorant of - X;
        for x being R_eal holds (x in X implies a <=' x)
      proof
         let x be R_eal;
         assume x in X;
         then - x in - X by Th23;
         then - x <=' - a by A2,SUPINF_1:def 9;
         hence thesis by Th16;
      end;
      hence thesis by SUPINF_1:def 10;
end;

theorem Th32:
   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;
A1:a is minorant of - X &
   for y being R_eal holds
   (y is minorant of - X implies y <=' a) by SUPINF_1:def 17;
A2:b is majorant of X &
   for y being R_eal holds
   (y is majorant of X implies b <=' y) by SUPINF_1:def 16;
A3:a <=' - b
   proof
        - a is majorant of - (- X) by A1,Th31;
      then - a is majorant of X by Th22;
      then b <=' - a by SUPINF_1:def 16;
      then - (- a) <=' - b by Th16;
      hence thesis;
   end;
     - b <=' a
   proof
        - b is minorant of - X by A2,Th30;
      hence thesis by SUPINF_1:def 17;
   end;
   hence thesis by A3,SUPINF_1:22;
end;

theorem Th33:
   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;
A1:a is majorant of - X &
   for y being R_eal holds
   (y is majorant of - X implies a <=' y) by SUPINF_1:def 16;
A2:b is minorant of X &
   for y being R_eal holds
   (y is minorant of X implies y <=' b) by SUPINF_1:def 17;
A3:a <=' - b
   proof
        - b is majorant of - X by A2,Th31;
      hence thesis by SUPINF_1:def 16;
   end;
     - b <=' a
   proof
        - a is minorant of - (- X) by A1,Th30;
      then - a is minorant of X by Th22;
      then - a <=' b by SUPINF_1:def 17;
      then - b <=' - (-a) by Th16;
      hence thesis;
   end;
   hence thesis by A3,SUPINF_1:22;
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
   consider x being Element of X;
A1:F.x in rng F by FUNCT_2:6;
     rng F c= Y by RELSET_1:12;
   hence thesis by A1,XBOOLE_1:1;
end;
end;

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

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   func sup F -> R_eal equals
:Def7: sup(rng F);
correctness;
end;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   func inf F -> R_eal equals
:Def8: inf(rng F);
correctness;
end;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   let x be Element of X;
   redefine func F.x -> R_eal;
coherence
proof
     F.x in ExtREAL by TARSKI:def 3;
   hence thesis;
end;
end;

scheme FunctR_ealEx{X()->non empty set,Y()->set,F(set)->set}:
   ex f being Function of X(),Y() st
   for x being Element of X() holds f.x = F(x)
   provided
A1:for x being Element of X() holds F(x) in Y()
proof defpred P[set,set] means $2 = F($1);
A2:for x being set st x in X() ex y being set st y in Y() & P[x,y]
   proof
      let x be set;
      assume x in X();
      then reconsider x as Element of X();
      take F(x);
      thus thesis by A1;
     end;
  ex f being Function of X(),Y() st
   for x being set st x in X() holds P[x,f.x] from FuncEx1(A2);
   then consider f being Function of X(),Y() such that
A3:for x being set st x in X() holds f.x = F(x);
     for x being Element of X() holds f.x = F (x) by A3;
   hence thesis;
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
:Def9: 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;
        F.x in Y & G.x in Z by FUNCT_2:7;
      hence thesis by Def5;
   end;
     ex H being Function of X,Y + Z st
   for x being Element of X holds H.x = F(x) from FunctR_ealEx(A1);
   then consider H being Function of X,Y + Z such that
A2:for x being Element of X holds H.x = F.x + G.x;
   take H;
   thus thesis by A2;
end;
uniqueness
proof
   let H1,H2 be Function of X,Y + Z such that
A3:for x being Element of X holds H1.x = F.x + G.x and
A4: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 A3
          .= H2.x by A4;
      hence thesis;
   end;
   hence thesis by FUNCT_2:18;
end;
end;

theorem Th34:
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL holds
   for F being Function of X,Y for G being Function of X,Z holds
   rng(F + G) c= rng F + rng 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;
     F + G is Function of X,rng F + rng G
      proof
      A1:dom (F + G) = X by FUNCT_2:def 1;
           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;
            consider a,b being R_eal such that
         A2:a = F.x & b = G.x;
        A3:(F + G).x = a + b by A2,Def9;
        A4:a in rng F by A2,FUNCT_2:6;
              b in rng G by A2,FUNCT_2:6;
            hence thesis by A3,A4,Def5;
         end;
         hence thesis by A1,FUNCT_2:5;
      end;
      hence thesis by RELSET_1:12;
end;

theorem Th35:
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st
   not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds
   for F being Function of X,Y for G being Function of X,Z st
   not(sup F = +infty & sup G = -infty or sup F = -infty & sup G = +infty
) holds
   sup(F + G) <=' sup F + sup G
proof
   let X be non empty set;
   let Y,Z be non empty Subset of ExtREAL;
   assume
A1:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z);
      let F be Function of X,Y;
      let G be Function of X,Z;
      assume
   A2:not(sup F = +infty & sup G = -infty or sup F = -infty & sup G = +infty);
      A3:sup(F + G) = sup(rng(F + G)) by Def7;
           rng(F + G) c= rng F + rng G by Th34;
      then A4:sup(F + G) <=' sup(rng F + rng G) by A3,SUPINF_1:91;
           (not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
 in rng G) &
          not(sup(rng F) = +infty & sup(rng G) = -infty or
              sup(rng F) = -infty & sup(rng G) = +infty))
         proof
           not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
 in rng G)
            proof
               assume
            A5:-infty in rng F & +infty in rng G or +infty in rng F & -infty
 in rng G;
            A6:rng F c= Y by RELSET_1:12;
              rng G c= Z by RELSET_1:12;
               hence contradiction by A1,A5,A6;
            end;
            hence thesis by A2,Def7;
         end;
         then A7: sup(rng F + rng G) <=' sup(rng F) + sup(rng G) by Th26;
           sup F = sup(rng F) & sup G = sup(rng G) by Def7;
         hence thesis by A4,A7,SUPINF_1:29;
end;

theorem Th36:
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st
   not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds
   for F being Function of X,Y for G being Function of X,Z st
   not(inf F = +infty & inf G = -infty or inf F = -infty & inf G = +infty
) holds
   inf F + inf G <=' inf(F + G)
proof
   let X be non empty set;
   let Y,Z be non empty Subset of ExtREAL;
   assume
A1:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z);
      let F be Function of X,Y;
      let G be Function of X,Z;
      assume
   A2:not(inf F = +infty & inf G = -infty or inf F = -infty & inf G = +infty);
      A3:inf(F + G) = inf(rng(F + G)) by Def8;
           rng(F + G) c= rng F + rng G by Th34;
      then A4:inf(rng F + rng G) <=' inf(F + G) by A3,SUPINF_1:94;
           (not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
 in rng G) &
          not(inf(rng F) = +infty & inf(rng G) = -infty or
              inf(rng F) = -infty & inf(rng G) = +infty))
         proof
           not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
 in rng G)
            proof
               assume
            A5:-infty in rng F & +infty in rng G or +infty in rng F & -infty
 in rng G;
            A6:rng F c= Y by RELSET_1:12;
              rng G c= Z by RELSET_1:12;
               hence contradiction by A1,A5,A6;
            end;
            hence thesis by A2,Def8;
         end;
         then A7: inf(rng F) + inf(rng G) <=' inf(rng F + rng G) by Th27;
           inf F = inf(rng F) & inf G = inf(rng G) by Def8;
         hence thesis by A4,A7,SUPINF_1:29;
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
:Def10: 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:7;
      hence thesis by Th23;
   end;
     ex H being Function of X,- Y st
   for x being Element of X holds H.x = F(x) from FunctR_ealEx(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:18;
end;
end;

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

theorem Th38:
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   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 Def8
           .= inf(- rng F) by Th37
           .= - sup(rng F) by Th32
           .= - sup F by Def7;
   thus sup(- F) = sup(rng(- F)) by Def7
           .= sup(- rng F) by Th37
           .= - inf(rng F) by Th33
           .= - inf F by Def8;
end;

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

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   attr F is bounded_above means
:Def11:sup F <'+infty;
end;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   attr F is bounded_below means
:Def12:-infty <'inf F;
end;

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

definition let X be non empty set;
           let Y be non empty Subset of ExtREAL;
  cluster bounded -> bounded_above bounded_below Function of X, Y;
  coherence by Def13;
  cluster bounded_above bounded_below -> bounded Function of X, Y;
  coherence by Def13;
end;

theorem
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded iff sup F <'+infty & -infty <'inf F
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   hereby assume F is bounded;
      then F is bounded_above & F is bounded_below by Def13;
      hence sup F <'+infty & -infty <'inf F by Def11,Def12;
   end;
      assume sup F <'+infty & -infty <'inf F;
      then F is bounded_above & F is bounded_below by Def11,Def12;
      hence thesis by Def13;
end;

theorem Th40:
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded_above iff - F is bounded_below
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
    hereby assume F is bounded_above;
      then sup F <'+infty by Def11;
      then A1:- (+infty) <'- sup F by Th16;
        - (+infty) = -infty by Def3;
      then -infty <'inf(- F) by A1,Th38;
      hence - F is bounded_below by Def12;
   end;
    assume - F is bounded_below;
      then -infty <'inf(- F) by Def12;
      then - inf(- F) <'- (-infty) by Th16;
      then - (- sup F) <'- (-infty) by Th38;
      hence thesis by Def11,Th4;
end;

theorem Th41:
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded_below iff - F is bounded_above
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
    hereby assume F is bounded_below;
      then -infty <'inf F by Def12;
      then - inf F <'- (-infty) by Th16;
      then sup(- F) <'+infty by Th4,Th38;
      hence - F is bounded_above by Def11;
   end;
      assume - F is bounded_above;
      then sup(- F) <'+infty by Def11;
      then - inf F <'+infty by Th38;
   then A1:- (+infty) <'- (- inf F) by Th16;
        - (+infty) = -infty & - (- inf F) = inf F by Def3;
      hence thesis by A1,Def12;
end;

theorem
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded iff - F is bounded
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   hereby assume F is bounded;
      then F is bounded_above & F is bounded_below by Def13;
      then - F is bounded_above & - F is bounded_below by Th40,Th41;
      hence - F is bounded by Def13;
   end;
      assume - F is bounded;
      then - F is bounded_above & - F is bounded_below by Def13;
      then F is bounded_above & F is bounded_below by Th40,Th41;
      hence thesis by Def13;
end;

theorem
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   for x being Element of X holds
   -infty <=' F.x & F.x <=' +infty by SUPINF_1:20,21;

theorem
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   for x being Element of X holds
   Y c= REAL implies -infty <'F.x & F.x <'+infty
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   let x be Element of X;
   assume
A1:Y c= REAL;
A2:X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
   then F.x in rng F by FUNCT_1:def 5;
   then F.x in Y by A2;
then A3:not F.x = -infty & not F.x = +infty by A1,SUPINF_1:2,6;
     -infty <=' F.x & F.x <=' +infty by SUPINF_1:20,21;
   hence thesis by A3,SUPINF_1:22;
end;

theorem Th45:
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   for x being Element of X holds
   inf F <=' F.x & F.x <=' sup F
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   let x be Element of X;
     X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
then A1:F.x in rng F by FUNCT_1:def 5;
A2:   inf F = inf(rng F) by Def8;
     sup F = sup(rng F) by Def7;
   hence thesis by A1,A2,SUPINF_1:76,79;
end;

theorem Th46:
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for 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;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   assume
A1:Y c= REAL;
   hereby assume F is bounded_above;
      then A2: sup F <'+infty by Def11;
      consider x being Element of X;
   A3:X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
      then F.x in rng F by FUNCT_1:def 5;
      then A4: F.x in Y by A3;
        F.x <=' sup F by Th45;
   then A5:not sup F = -infty by A1,A4,SUPINF_1:17;
        sup F in REAL or sup F in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:
def 2;
      hence sup F in REAL by A2,A5,TARSKI:def 2;
   end;
      assume sup F in REAL;
      then sup F <'+infty by SUPINF_1:31;
      hence thesis by Def11;
end;

theorem Th47:
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   Y c= REAL implies (F is bounded_below iff inf F in REAL)
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   assume
A1:Y c= REAL;
A2:F is bounded_below implies inf F in REAL
   proof
      assume F is bounded_below;
      then A3: -infty <'inf F by Def12;
      consider x being Element of X;
   A4:X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
      then F.x in rng F by FUNCT_1:def 5;
      then A5:F.x in Y by A4;
        inf F <=' F.x by Th45;
   then A6:not inf F = +infty by A1,A5,SUPINF_1:18;
        inf F in REAL or inf F in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:
def 2;
      hence thesis by A3,A6,TARSKI:def 2;
   end;
     inf F in REAL implies F is bounded_below
   proof
      assume inf F in REAL;
      then -infty <'inf F by SUPINF_1:31;
      hence thesis by Def12;
   end;
   hence thesis by A2;
end;

theorem
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   Y c= REAL implies (F is bounded iff inf F in REAL & sup F in REAL)
proof
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   assume
A1:Y c= REAL;
A2:F is bounded implies inf F in REAL & sup F in REAL
   proof
      assume F is bounded;
      then F is bounded_above & F is bounded_below by Def13;
      hence thesis by A1,Th46,Th47;
   end;
     inf F in REAL & sup F in REAL implies F is bounded
   proof
      assume inf F in REAL & sup F in REAL;
      then F is bounded_above & F is bounded_below by A1,Th46,Th47;
      hence thesis by Def13;
   end;
   hence thesis by A2;
end;

theorem Th49:
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
   for F1 being Function of X,Y holds
   for F2 being Function of X,Z holds
   F1 is bounded_above & F2 is bounded_above implies F1 + F2 is bounded_above
proof
   let X be non empty set;
   let Y,Z be non empty Subset of ExtREAL;
   assume
A1:Y c= REAL & Z c= REAL;
   let F1 be Function of X,Y;
   let F2 be Function of X,Z;
   assume
A2:F1 is bounded_above & F2 is bounded_above;
A3:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z)
 by A1,SUPINF_1:2;
   A4:not sup F1 = +infty & not sup F2 = +infty by A2,Def11;
A5:sup F1 in REAL & sup F2 in REAL implies sup F1 + sup F2 <'+infty
   proof
      assume
   A6:sup F1 in REAL & sup F2 in REAL;
      consider a,b being R_eal such that
   A7:a = sup F1 & b = sup F2;
      reconsider a,b as Real by A6,A7;
    sup F1 + sup F2 = a + b by A7,Th1;
      hence thesis by SUPINF_1:31;
   end;
A8:sup F1 in REAL & sup F2 = -infty implies sup F1 + sup F2 <'+infty
   proof
      assume sup F1 in REAL & sup F2 = -infty;
      hence thesis by Def2,SUPINF_1:2,19;
   end;
A9:sup F1 = -infty & sup F2 in REAL implies sup F1 + sup F2 <'+infty
   proof
      assume
    sup F1 = -infty & sup F2 in REAL;
      hence thesis by Def2,SUPINF_1:2,19;
   end;
A10:sup F1 = -infty & sup F2 = -infty implies sup F1 + sup F2 <'+infty
      by Def2,SUPINF_1:19;
     sup(F1 + F2) <'+infty
   proof
      assume not sup(F1 + F2) <'+infty;
      then not(sup(F1 + F2) <=' +infty) or sup(F1 + F2) = +infty by SUPINF_1:22
;
      hence thesis by A3,A4,A5,A8,A9,A10,Th35,SUPINF_1:24,def 7;
   end;
   hence thesis by Def11;
end;

theorem Th50:
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
   for F1 being Function of X,Y holds
   for F2 being Function of X,Z holds
   F1 is bounded_below & F2 is bounded_below implies F1 + F2 is bounded_below
proof
   let X be non empty set;
   let Y,Z be non empty Subset of ExtREAL;
   assume
A1:Y c= REAL & Z c= REAL;
   let F1 be Function of X,Y;
   let F2 be Function of X,Z;
   assume
A2:F1 is bounded_below & F2 is bounded_below;
A3:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z)
by A1,SUPINF_1:2;
   A4:not inf F1 = -infty & not inf F2 = -infty by A2,Def12;
A5:inf F1 in REAL & inf F2 in REAL implies -infty <'inf F1 + inf F2
   proof
      assume
   A6:inf F1 in REAL & inf F2 in REAL;
      consider a,b being R_eal such that
   A7:a = inf F1 & b = inf F2;
      reconsider a,b as Real by A6,A7;
    inf F1 + inf F2 = a + b by A7,Th1;
      hence thesis by SUPINF_1:31;
   end;
A8:inf F1 in REAL & inf F2 = +infty implies -infty <'inf F1 + inf F2
   proof
      assume
     inf F1 in REAL & inf F2 = +infty;
      hence thesis by Def2,SUPINF_1:6,19;
   end;
A9:inf F1 = +infty & inf F2 in REAL implies -infty <'inf F1 + inf F2
   proof
      assume
    inf F1 = +infty & inf F2 in REAL;
      hence thesis by Def2,SUPINF_1:6,19;
   end;
A10:inf F1 = +infty & inf F2 = +infty implies -infty <'inf F1 + inf F2
     by Def2,SUPINF_1:19;
     -infty <'inf(F1 + F2)
   proof
      assume not -infty <'inf(F1 + F2);
      then not(-infty <=' inf(F1 + F2)) or inf(F1 + F2) = -infty by SUPINF_1:22
;
      hence thesis by A3,A4,A5,A8,A9,A10,Th36,SUPINF_1:23,def 7;
   end;
   hence thesis by Def12;
end;

theorem
     for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
   for F1 being Function of X,Y holds
   for F2 being Function of X,Z holds
   F1 is bounded & F2 is bounded implies F1 + F2 is bounded
proof
   let X be non empty set;
   let Y,Z be non empty Subset of ExtREAL;
   assume
A1:Y c= REAL & Z c= REAL;
   let F1 be Function of X,Y;
   let F2 be Function of X,Z;
   assume
  F1 is bounded & F2 is bounded;
   then F1 is bounded_above & F1 is bounded_below &
   F2 is bounded_above & F2 is bounded_below by Def13;
   then F1 + F2 is bounded_above & F1 + F2 is bounded_below by A1,Th49,Th50;
   hence thesis by Def13;
end;

theorem Th52:
   ex F being Function of NAT,ExtREAL st (F is one-to-one & NAT = rng F &
   rng F is non empty Subset of ExtREAL)
proof
   deffunc F(set) = $1;
A1:now let x be set;
      assume x in NAT;
      then x is R_eal by SUPINF_1:10;
      hence F(x) in ExtREAL;
   end;
     ex F being Function of NAT,ExtREAL st for n being set st n in NAT holds
   F.n = F(n) from Lambda1(A1);
   then consider F being Function of NAT,ExtREAL such that
A2:for n being set st n in NAT holds F.n = n;
A3:rng F is non empty Subset
 of ExtREAL & dom F = NAT & F is one-to-one & rng F = NAT
   proof
  A4:dom F = NAT & rng F c= ExtREAL by FUNCT_2:def 1,RELSET_1:12;
A5: for x1,x2 being set st x1 in NAT & x2 in NAT & F.x1 = F.x2 holds x1 = x2
      proof
         let x1,x2 be set;
         assume
     A6:x1 in NAT & x2 in NAT & F.x1 = F.x2;
         then F.x1 = x1 & F.x2 = x2 by A2;
         hence thesis by A6;
      end;
        for y being set holds y in NAT iff ex x being set st x in dom F & y = F
.
x
      proof
         let y be set;
           y in NAT implies ex x being set st (x in dom F & y = F.x)
         proof
          assume
         A7:y in NAT;
            take y;
            thus thesis by A2,A7,FUNCT_2:def 1;
         end;
         hence thesis by A2,A4;
      end;
      hence thesis by A5,FUNCT_1:def 5,FUNCT_2:25,def 1,RELSET_1:12;
   end;
   take F;
   thus thesis by A3;
end;

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

definition let D be non empty set; let IT be Subset of D;
 redefine attr IT is countable means
:Def14: 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_4:45;
      consider x being Element of D such that
A5:    x in IT by A2,SUBSET_1:10;
      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:167;
A8:        dom(f|(f"IT)) = NAT /\ (f"IT) by A3,RELAT_1:90;
        per cases;
        suppose
A9:        NAT = f"IT;
          then A10:         NAT \ f"IT = {} by XBOOLE_1:37;
          then dom(NAT \ f"IT --> x) = {} by FUNCOP_1:16;
          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:32;
        hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:26
             .= rng(f|(f"IT)) \/ {} by A10,FUNCOP_1:16
             .= f.:(f"IT) by RELAT_1:148
             .= IT by A4,FUNCT_1:147;
         thus dom F = dom(f|(f"IT)) \/ dom(NAT \ f"IT --> x) by FUNCT_4:def 1
          .= dom(f|(f"IT)) \/ {} by A10,FUNCOP_1:16
          .= NAT by A8,A9;
        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:19;
          then dom(f|(f"IT)) misses dom(NAT \ f"IT --> x) by A8,XBOOLE_1:89;
          then F = (f|(f"IT)) \/ (NAT \ f"IT --> x) by FUNCT_4:32;
         hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:26
             .= rng(f|(f"IT)) \/ {x} by A12,FUNCOP_1:14
             .= f.:(f"IT) \/ {x} by RELAT_1:148
             .= IT \/ {x} by A4,FUNCT_1:147
             .= IT by A5,ZFMISC_1:46;
         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:19
          .= NAT by XBOOLE_1:51;
       end;
      then reconsider F as Function of NAT, D by FUNCT_2:def 1,RELSET_1:11;
     take F;
     thus IT = rng F 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;
     then IT = {};
     hence thesis by CARD_4:43;
   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 IT is countable by A14,CARD_4:45;
  end;
 synonym IT is denumerable;
end;

definition
 cluster denumerable (non empty Subset of ExtREAL);
existence
 proof
   consider F being Function of NAT,ExtREAL such that
       F is one-to-one & NAT = rng F and
A1:  rng F is non empty Subset of ExtREAL by Th52;
   reconsider A = rng F as non empty Subset of ExtREAL by A1;
  take A;
  assume A is non empty;
  thus thesis;
 end;
end;

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

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

definition
   cluster nonnegative Denum_Set_of_R_EAL;
existence
 proof
   reconsider N = NAT as Denum_Set_of_R_EAL by Def14,Th52;
  take N;
  thus for x being R_eal holds x in N implies 0. <=' x by Th21;
 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
:Def16:D = rng it;
existence by Def14;
end;

definition
   let N be Function of NAT,ExtREAL;
   let n be Nat;
redefine func N.n -> R_eal;
coherence
proof
     N.n is R_eal;
   hence thesis;
end;
end;

theorem Th53:
   for D being Denum_Set_of_R_EAL holds
   for N being Num of D holds
   ex F being Function of NAT,ExtREAL st
   F.0 = N.0 &
   for n being Nat,
   y being R_eal st y = F.n holds
   F.(n + 1) = y + N.(n+1)
proof
   let D be Denum_Set_of_R_EAL;
   let N be Num of D;
   defpred P[set,set,set] means
   for a,b being R_eal,s being Nat holds (s = $1 & a = $2 & b = $3 implies
   b = a + N.(s+1));
A1:for n being Nat for x being Element of ExtREAL
      ex y being Element of ExtREAL st P[n,x,y]
   proof
      let n be Nat;
      let x be Element of ExtREAL;
         consider y being R_eal such that
      A2:y = x + N.(n+1);
         take y;
         thus thesis by A2;
   end;
   consider A being R_eal such that
A3:A = N.0;
   consider F being Function of NAT,ExtREAL such that
A4:(F.0 = A & for n being Element of NAT holds P[n,F.n,F.(n+1)])
   from RecExD(A1);
   take F;
   thus thesis by A3,A4;
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
:Def17:it.0 = N.0 &
   for n being Nat holds
   for y being R_eal st y = it.n holds
   it.(n + 1) = y + N.(n + 1);
existence by Th53;
uniqueness
proof
   let S1,S2 be Function of NAT,ExtREAL such that
A1:S1.0 = N.0 &
   for n being Nat holds
   for y being R_eal st y = S1.n holds
   S1.(n + 1) = y + N.(n + 1) and
A2:S2.0 = N.0 &
   for n being 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
   A3:n in NAT;
      then reconsider n as Element of REAL;
      reconsider n as Nat by A3;
        for n being Nat holds S1.n = S2.n
      proof
      A4: P[0] by A1,A2;
      A5: for k being Nat st P[k] holds P[k+1]
         proof
            let k be Nat;
            assume
         A6:S1.k = S2.k;
            consider y1,y2 being R_eal such that
         A7:y1 = S1.k & y2 = S2.k;
            thus S1.(k + 1) = y2 + N.(k + 1) by A1,A6,A7
                      .= S2.(k + 1) by A2,A7;
         end;
         thus for k being Nat holds P[k] from Ind(A4,A5);
      end;
      then S1.n = S2.n;
      hence thesis;
   end;
   hence thesis by FUNCT_2:18;
end;
end;

theorem Th54:
   for D being Pos_Denum_Set_of_R_EAL holds
   for N being Num of D holds
   for n being Nat holds 0. <=' N.n
proof
   let D be Pos_Denum_Set_of_R_EAL;
   let N be Num of D;
   let n be Nat;
     D = rng N by Def16;
      then N.n in D by FUNCT_2:6;
      hence thesis by Def15;
end;

theorem Th55:
   for D being Pos_Denum_Set_of_R_EAL holds
   for N being Num of D holds
   for n being 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;
   let N be Num of D;
   let n be Nat;
   set F = Ser(D,N);
A1:F.0 = N.0 &
   for n being Nat holds
   for y being R_eal st y = F.n holds
   F.(n + 1) = y + N.(n + 1) by Def17;
   defpred P[Nat] means F.$1 <=' F.($1 + 1) & 0. <=' F.$1;
A2: P[0]
   proof
      A3:F.(0 + 1) = F.0 + N.(1) by Def17;
      A4:0. <=' F.0 by A1,Th54;
           0. <=' N.(1) by Th54;
         hence thesis by A3,A4,Th20;
   end;
A5: for k being Nat st P[k] holds P[k + 1]
   proof
      let k be Nat;
         assume
      A6:F.k <=' F.(k + 1) & 0. <=' F.k;
      A7:F.((k+1) + 1) = F.(k + 1) + N.((k+1) + 1) by Def17;
      A8:0. <=' N.((k+1) + 1) by Th54;
        0. <=' F.(k+1) by A6,SUPINF_1:29;
         hence thesis by A7,A8,Th20;
   end;
     for n being Nat holds P[n] from Ind(A2,A5);
   hence thesis;
end;

theorem Th56:
   for D being Pos_Denum_Set_of_R_EAL holds
   for N being Num of D holds
   for n,m being Nat holds
   Ser(D,N).n <=' Ser(D,N).(n + m)
proof
   let D be Pos_Denum_Set_of_R_EAL;
   let N be Num of D;
   let n,m be Nat;
   defpred P[Nat] means Ser(D,N).n <=' Ser(D,N).(n + $1);
A1: P[0];
A2: for k being Nat st P[k] holds P[k + 1]
   proof
      let k be Nat;
         assume
      A3:Ser(D,N).n <=' Ser(D,N).(n + k);
        Ser(D,N).(n + (k+1)) = Ser(D,N).((n + k) + 1) by XCMPLX_1:1;
         then Ser(D,N).(n + k) <=' Ser(D,N).(n + (k+1)) by Th55;
         hence thesis by A3,SUPINF_1:29;
   end;
     for n being Nat holds P[n] from Ind(A1,A2);
   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
   consider N being Num of D;
   set S = Ser(D,N);
     0 in NAT;
   then rng S is non empty Subset of ExtREAL by FUNCT_2:6,RELSET_1:12;
   then consider SER being non empty Subset of ExtREAL such that
A1:SER = rng S;
   take SER;
   thus thesis by A1;
end;
end;

Lm4:
   for F being Function of NAT,ExtREAL holds
   rng F is non empty Subset of ExtREAL
proof
   let F be Function of NAT,ExtREAL;
   consider n being Element of NAT;
     n in NAT;
   hence thesis by FUNCT_2:6,RELSET_1:12;
end;

definition
   let F be Function of NAT,ExtREAL;
redefine func rng F -> non empty Subset of ExtREAL;
coherence by Lm4;
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 Th57:
   for F being Function of NAT,ExtREAL holds
   rng F is Denum_Set_of_R_EAL by Def14;

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

definition
   let F be Function of NAT,ExtREAL;
   func Ser(F) -> Function of NAT,ExtREAL means
:Def21: for N being Num of rng F st N = F holds it = Ser(rng F,N);
existence
proof
     F is Num of rng F by Def16;
   then consider N being Num of rng F such that
A1:N = F;
   take Ser(rng F,N);
   thus thesis by A1;
end;
uniqueness
proof
   let S1,S2 be Function of NAT,ExtREAL such that
A2:for N being Num of rng F st N = F holds S1 = Ser(rng F,N) and
A3:for N being Num of rng F st N = F holds S2 = Ser(rng F,N);
     F is Num of rng F by Def16;
   then consider N being Num of rng F such that
A4:N = F;
   thus S1 = Ser(rng F,N) by A2,A4
     .= S2 by A3,A4;
end;
end;

definition let X be set;
   let F be Function of X,ExtREAL;
   attr F is nonnegative means
:Def22:rng F is nonnegative;
end;

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

theorem Th58:
   for X being non empty set
   for F being Function of X,ExtREAL holds
   F is nonnegative iff for n being Element of X holds 0. <=' F.n
proof let X be non empty set;
   let F be Function of X,ExtREAL;
      hereby assume F is nonnegative;
   then A1:rng F is nonnegative by Def22;
      let n be Element of X;
         F.n in rng F by FUNCT_2:6;
      hence 0. <=' F.n by A1,Def15;
   end;
      assume
   A2:for n being Element of X holds 0. <=' F.n;
        for y being R_eal holds y in rng F implies 0. <=' y
      proof
         let y be R_eal;
         assume y in rng F;
         then consider x being set such that
      A3:x in dom F & y = F.x by FUNCT_1:def 5;
         reconsider x as Element of X by A3,FUNCT_2:def 1;
           0. <=' F.x by A2;
         hence thesis by A3;
      end;
      then rng F is nonnegative by Def15;
      hence thesis by Def22;
end;

theorem Th59:
   for F being Function of NAT,ExtREAL holds
   for n being Nat holds
   F is nonnegative implies (Ser(F)).n <=' (Ser(F)).(n + 1) & 0. <=' (Ser(F)).n
proof
   let F be Function of NAT,ExtREAL;
   let n be Nat;
   assume
A1:F is nonnegative;
     F is Num of rng F by Def16;
   then consider N being Num of rng F such that
A2:N = F;
A3:Ser(F) = Ser(rng F,N) by A2,Def21;
     rng F is Pos_Denum_Set_of_R_EAL by A1,Def22;
   hence thesis by A3,Th55;
end;

theorem Th60:
   for F being Function of NAT,ExtREAL holds
   F is nonnegative implies
   for n,m being Nat holds Ser(F).n <=' Ser(F).(n + m)
proof
   let F be Function of NAT,ExtREAL;
   assume
A1:F is nonnegative;
   let n,m be Nat;
     F is Num of rng F by Def16;
   then consider N being Num of rng F such that
A2:N = F;
A3:Ser(F) = Ser(rng F,N) by A2,Def21;
     rng F is Pos_Denum_Set_of_R_EAL by A1,Def22;
   hence thesis by A3,Th56;
end;

theorem Th61:
   for F1,F2 being Function of NAT,ExtREAL st
   F1 is nonnegative holds
   ((for n being Nat holds F1.n <=' F2.n) implies
   (for n being Nat holds Ser(F1).n <=' Ser(F2).n))
proof
   let F1,F2 be Function of NAT,ExtREAL;
   assume
A1:F1 is nonnegative;
      assume
   A2:for n being Nat holds F1.n <=' F2.n;
        F1 is Num of rng F1 by Def16;
      then consider N1 being Num of rng F1 such that
   A3:N1 = F1;
   A4:Ser(F1) = Ser(rng F1,N1) by A3,Def21;
        F2 is Num of rng F2 by Def16;
      then consider N2 being Num of rng F2 such that
   A5:N2 = F2;
   A6:Ser(F2) = Ser(rng F2,N2) by A5,Def21;
         let n be Nat;
     defpred P[Nat] means Ser(F1).$1 <=' Ser(F2).$1;
         A7: P[0]
            proof
            A8:Ser(F1).0 = F1.0 by A3,A4,Def17;
              Ser(F2).0 = F2.0 by A5,A6,Def17;
               hence thesis by A2,A8;
            end;
         A9: for k being Nat st P[k] holds P[k+1]
            proof
               let k be Nat;
               assume
            A10:Ser(F1).k <=' Ser(F2).k;
              A11:Ser(F1).(k+1) = Ser(F1).k + F1.(k+1) by A3,A4,Def17;
              A12:Ser(F2).(k+1) = Ser(F2).k + F2.(k+1) by A5,A6,Def17;
              A13:F1.(k+1) <=' F2.(k+1) by A2;
              A14:0. <=' Ser(F1).k by A1,Th59;
                0. <=' F1.(k+1) by A1,Th58;
                  hence thesis by A10,A11,A12,A13,A14,Lm3;
            end;
              for n being Nat holds P[n] from Ind(A7,A9);
            hence thesis;
end;

theorem Th62:
   for F1,F2 being Function of NAT,ExtREAL st
   F1 is nonnegative holds
   ((for n being Nat holds F1.n <=' F2.n) implies (SUM(F1) <=' SUM(F2)))
proof
   let F1,F2 be Function of NAT,ExtREAL;
   assume
A1:F1 is nonnegative;
      assume
   A2:for n being Nat holds F1.n <=' F2.n;
   A3:SUM(F1) = sup(rng Ser(F1)) by Def23;
   A4:SUM(F2) = sup(rng Ser(F2)) by Def23;
        for x being R_eal st x in rng Ser(F1) holds
      (ex y being R_eal st y in rng Ser(F2) & x <=' y)
      proof
         let x be R_eal;
         assume
      A5:x in rng Ser(F1);
     A6:dom Ser(F1) = NAT & dom Ser(F2) = NAT & rng Ser(F2) c= ExtREAL
         by FUNCT_2:def 1;
            then consider n being set such that
        A7:n in NAT & x = Ser(F1).n by A5,FUNCT_1:def 5;
            reconsider n as Nat by A7;
            consider y being set such that
        A8:y = Ser(F2).n;
            reconsider y as R_eal by A8;
            take y;
            thus thesis by A1,A2,A6,A7,A8,Th61,FUNCT_1:def 5;
      end;
      hence thesis by A3,A4,SUPINF_1:99;
end;

theorem Th63:
   for F being Function of NAT,ExtREAL holds
   Ser(F).0 = F.0 &
   for n being Nat holds
   for 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;
     F is Num of rng F by Def16;
   then consider N being Num of rng F such that
A1:N = F;
  Ser(F) = Ser(rng F,N) by A1,Def21;
   hence thesis by A1,Def17;
end;

theorem Th64:
   for F being Function of NAT,ExtREAL st F is nonnegative holds
   (ex n being 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 Nat such that
   A2:F.n = +infty;
      A3:n = 0 implies SUM(F) = +infty
         proof
            assume n = 0;
         then A4:Ser(F).0 = +infty by A2,Th63;
            consider x being R_eal such that
        A5:x = Ser(F).0;
        A6:x in rng Ser(F) by A5,FUNCT_2:6;
              x is majorant of rng Ser(F) by A4,A5,SUPINF_1:33;
            then sup(rng Ser(F)) = +infty by A4,A5,A6,SUPINF_1:80;
            hence thesis by Def23;
         end;
           (ex k being Nat st n = k + 1) implies SUM(F) = +infty
         proof
            given k being Nat such that
         A7:n = k + 1;
        A8:not Ser(F).k = -infty
            proof
            A9:0. <=' Ser(F).k by A1,Th59;
                  not 0. = -infty by Def1,SUPINF_1:6;
                hence thesis by A9,SUPINF_1:23;
            end;
            consider y being R_eal such that
        A10:y = Ser(F).k;
A11:        Ser(F).(k + 1) = y + F.(k + 1) by A10,Th63;
            consider x being R_eal such that
        A12:x = Ser(F).(k + 1);
        A13:x = +infty by A2,A7,A8,A10,A11,A12,Def2;
        A14:x in rng Ser(F) by A12,FUNCT_2:6;
              x is majorant of rng Ser(F) by A13,SUPINF_1:33;
            then sup(rng Ser(F)) = +infty by A13,A14,SUPINF_1:80;
            hence thesis by Def23;
         end;
         hence thesis by A3,NAT_1:22;
end;

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

theorem
  for F being Function of NAT,ExtREAL st F is nonnegative holds
   ((ex n being 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 Nat st F.n = +infty;
   then not SUM(F) in REAL by A1,Th64,SUPINF_1:2;
   hence thesis by Def24;
end;

theorem
     for F1,F2 being Function of NAT,ExtREAL st
   F1 is nonnegative holds
   ((for n being Nat holds F1.n <=' F2.n) implies
   (F2 is summable implies F1 is summable))
proof
   let F1,F2 be Function of NAT,ExtREAL;
   assume
A1:F1 is nonnegative;
      assume
   A2:for n being Nat holds F1.n <=' F2.n;
         assume F2 is summable;
      then A3:SUM(F2) in REAL by Def24;
           SUM(F1) <=' SUM(F2) by A1,A2,Th62;
      then A4:not SUM(F1) = +infty by A3,SUPINF_1:18;
      A5:SUM(F1) = sup(rng Ser(F1)) by Def23;
      A6:0. <=' Ser(F1).0 by A1,Th59;
           Ser(F1).0 in rng Ser(F1) by FUNCT_2:6;
         then Ser(F1).0 <=' sup(rng Ser(F1)) by SUPINF_1:76;
      then A7:0. <=' SUM(F1) by A5,A6,SUPINF_1:29;
     A8:not SUM(F1) = -infty
            proof
                 not 0. = -infty by Def1,SUPINF_1:6;
               hence thesis by A7,SUPINF_1:23;
            end;
           SUM(F1) in REAL \/ {-infty,+infty} by SUPINF_1:def 5;
         then SUM(F1) in REAL or SUM(F1) in {-infty,+infty} by XBOOLE_0:def 2;
         hence thesis by A4,A8,Def24,TARSKI:def 2;
end;

theorem Th67:
   for F being Function of NAT,ExtREAL st F is nonnegative holds
   for n being Nat st (for r being Nat holds (n <= r implies 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;
      assume
   A2:for r being Nat holds (n <= r implies F.r = 0.);
   A3:for r being Nat holds (n <= r implies Ser(F).r <=' Ser(F).n)
      proof
         let r be Nat;
         assume n <= r;
         then A4: ex m being Nat st r = n + m by NAT_1:28;
       defpred P[Nat] means Ser(F).(n + $1) <=' Ser(F).n;
           for m being Nat holds P[m]
         proof
         A5: P[0];
         A6: for s being Nat st P[s] holds P[s+1]
            proof
               let s be Nat;
               assume
            A7:Ser(F).(n + s) <=' Ser(F).n;
           A8:n + (s + 1) = (n + s) + 1 by XCMPLX_1:1;
               consider y being R_eal such that
           A9:y = Ser(F).(n + s);
           A10:Ser(F).(n + (s + 1)) = y + F.(n + (s + 1)) by A8,A9,Th63;
                 0 <= s+1 by NAT_1:18;
               then n + 0 <= n + (s+1) by REAL_1:55;
               then F.(n + (s+1)) = 0. by A2;
               hence thesis by A7,A9,A10,Th18;
            end;
            thus for m being Nat holds P[m] from Ind(A5,A6);
         end;
         hence thesis by A4;
      end;
   A11:for r being Nat holds (r <= n implies Ser(F).r <=' Ser(F).n)
      proof
        let r be Nat;
         assume r <= n;
         then ex m being Nat st n = r + m by NAT_1:28;
         hence thesis by A1,Th60;
      end;
        for y being R_eal holds y in rng Ser(F) implies y <=' Ser(F).n
      proof
         let y be R_eal;
         assume
      A12:y in rng Ser(F);
           dom Ser(F) = NAT & rng Ser(F) c= ExtREAL by FUNCT_2:def 1;
         then consider m being set such that
      A13:m in NAT & y = Ser(F).m by A12,FUNCT_1:def 5;
         reconsider m as Nat by A13;
        m <= n or n <= m;
         hence thesis by A3,A11,A13;
      end;
   then A14:Ser(F).n is majorant of rng Ser(F) by SUPINF_1:def 9;
        Ser(F).n in rng Ser(F) by FUNCT_2:6;
      then sup(rng Ser(F)) = Ser(F).n by A14,SUPINF_1:80;
      hence thesis by Def23;
end;

theorem Th68:
   for F being Function of NAT,ExtREAL st
   (for n being Nat holds F.n in REAL ) holds
   (for n being Nat holds Ser(F).n in REAL)
proof
   let F be Function of NAT,ExtREAL;
   assume
A1:for n being Nat holds F.n in REAL;
    defpred P[Element of NAT] means Ser(F).$1 in REAL;
        Ser(F).0 = F.0 by Th63;
   then A2: P[0] by A1;
   A3: for s being Nat st P[s] holds P[s+1]
      proof
         let s be Nat;
         assume
      A4:Ser(F).s in REAL;
         consider y being R_eal such that
      A5:y = Ser(F).s;
      A6:Ser(F).(s+1) = y + F.(s+1) by A5,Th63;
         consider b being set such that
      A7:b = F.(s+1);
         reconsider b as Real by A1,A7;
         consider a being set such that
      A8:a = y;
         reconsider a as Real by A4,A5,A8;
        y + F.(s+1) = a + b by A7,A8,Th1;
         hence thesis by A6;
      end;
      thus  for s being Nat holds P[s] from Ind(A2,A3);
end;

theorem
     for F being Function of NAT,ExtREAL st F is nonnegative holds
   (ex n being Nat st (for k being Nat holds (n <= k implies F.k = 0.)) &
   (for k being Nat holds (k <= n implies not F.k = +infty)))
   implies F is summable
proof
   let F be Function of NAT,ExtREAL;
   assume
A1:F is nonnegative;
      given n being Nat such that
   A2:for k being Nat holds (n <= k implies F.k = 0.) and
   A3:for k being Nat holds (k <= n implies not F.k = +infty);
   A4:SUM(F) = Ser(F).n by A1,A2,Th67;
        for s being Nat holds F.s in REAL
      proof
         let s be Nat;
      A5:s <= n implies F.s in REAL
         proof
            assume s <= n;
        then A6:not F.s = +infty by A3;
        A7:0. <=' F.s by A1,Th58;
        A8:not F.s = -infty
            proof
                 not 0. = -infty by Def1,SUPINF_1:6;
               hence thesis by A7,SUPINF_1:23;
            end;
              F.s in REAL \/ {-infty,+infty} by SUPINF_1:def 5;
            then F.s in REAL or F.s in {-infty,+infty} by XBOOLE_0:def 2;
            hence thesis by A6,A8,TARSKI:def 2;
         end;
           n <= s implies F.s in REAL
         proof
            assume n <= s;
        then F.s = 0. by A2;
            hence thesis by Def1;
         end;
         hence thesis by A5;
      end;
      then Ser(F).n in REAL by Th68;
      hence thesis by A4,Def24;
end;

Back to top