supinf_2.miz



    begin

    notation

      synonym 0. for 0 ;

    end

    definition

      :: original: 0.

      redefine

      func 0. -> R_eal ;

      coherence by XXREAL_0:def 1;

      let x be R_eal;

      :: original: -

      redefine

      func - x -> R_eal ;

      coherence by XXREAL_0:def 1;

      let y be R_eal;

      :: original: +

      redefine

      func x + y -> R_eal ;

      coherence by XXREAL_0:def 1;

      :: original: -

      redefine

      func x - y -> R_eal ;

      coherence by XXREAL_0:def 1;

    end

    theorem :: SUPINF_2:1

    for x,y be ExtReal, a,b be Real st x = a & y = b holds (x + y) = (a + b) by XXREAL_3:def 2;

    theorem :: SUPINF_2:2

    for x be ExtReal, a be Real st x = a holds ( - x) = ( - a) by XXREAL_3:def 3;

    theorem :: SUPINF_2:3

    for x,y be ExtReal, a,b be Real st x = a & y = b holds (x - y) = (a - b)

    proof

      let x,y be ExtReal, 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;

    notation

      let X,Y be Subset of ExtREAL ;

      synonym X + Y for X ++ Y;

    end

    definition

      let X,Y be Subset of ExtREAL ;

      :: original: +

      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 ;

      :: original: -

      redefine

      func - X -> Subset of ExtREAL ;

      coherence by MEMBERED: 2;

    end

    ::$Canceled

    theorem :: SUPINF_2:5

    for X be non empty Subset of ExtREAL , z be R_eal holds z in X iff ( - z) in ( - X) by MEMBER_1: 1;

    theorem :: SUPINF_2:6

    for X,Y be non empty Subset of ExtREAL holds X c= Y iff ( - X) c= ( - Y) by MEMBER_1: 3;

    theorem :: SUPINF_2:7

    for z be R_eal holds z in REAL iff ( - z) in REAL

    proof

      let z be R_eal;

      

       A1: for z be 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;

      :: original: inf

      redefine

      func inf X -> R_eal ;

      coherence by XXREAL_0:def 1;

      :: original: sup

      redefine

      func sup X -> R_eal ;

      coherence by XXREAL_0:def 1;

    end

    theorem :: SUPINF_2:8

    

     Th7: for X,Y be 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 be ExtReal holds z in (X + Y) implies z <= (( sup X) + ( sup Y))

      proof

        let z be ExtReal;

        assume z in (X + Y);

        then

        consider x,y be 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 :: SUPINF_2:9

    

     Th8: for X,Y be 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 be ExtReal holds z in (X + Y) implies (( inf X) + ( inf Y)) <= z

      proof

        let z be ExtReal;

        assume z in (X + Y);

        then

        consider x,y be 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 :: SUPINF_2:10

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

    theorem :: SUPINF_2:11

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

    theorem :: SUPINF_2:12

    

     Th11: for X be non empty Subset of ExtREAL , a be 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 be ExtReal st x in ( - X) holds ( - a) <= x

        proof

          let x be ExtReal;

          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 XXREAL_3: 38, A1, XXREAL_2:def 1;

          hence thesis;

        end;

        hence ( - a) is LowerBound of ( - X) by XXREAL_2:def 2;

      end;

      assume

       A3: ( - a) is LowerBound of ( - X);

      for x be ExtReal st x in X holds x <= a

      proof

        let x be ExtReal;

        assume

         A4: x in X;

        reconsider x as Element of ExtREAL by XXREAL_0:def 1;

        ( - x) in ( - X) by A4;

        hence thesis by XXREAL_3: 38, A3, XXREAL_2:def 2;

      end;

      hence thesis by XXREAL_2:def 1;

    end;

    theorem :: SUPINF_2:13

    

     Th12: for X be non empty Subset of ExtREAL holds for a be 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 be ExtReal st x in ( - X) holds x <= ( - a)

        proof

          let x be ExtReal;

          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 XXREAL_3: 38, A1, XXREAL_2:def 2;

          hence thesis;

        end;

        hence ( - a) is UpperBound of ( - X) by XXREAL_2:def 1;

      end;

      assume

       A3: ( - a) is UpperBound of ( - X);

      for x be ExtReal st x in X holds a <= x

      proof

        let x be ExtReal;

        assume

         A4: x in X;

        reconsider x as Element of ExtREAL by XXREAL_0:def 1;

        ( - x) in ( - X) by A4;

        hence thesis by XXREAL_3: 38, A3, XXREAL_2:def 1;

      end;

      hence thesis by XXREAL_2:def 2;

    end;

    theorem :: SUPINF_2:14

    

     Th13: for X be 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 Th12;

      then

       A1: ( - ( - a)) <= ( - b) by XXREAL_3: 38, XXREAL_2:def 3;

      b is UpperBound of X by XXREAL_2:def 3;

      then ( - b) is LowerBound of ( - X) by Th11;

      then ( - b) <= a by XXREAL_2:def 4;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: SUPINF_2:15

    

     Th14: 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 Th11;

      then

       A1: ( - b) <= ( - ( - a)) by XXREAL_3: 38, XXREAL_2:def 4;

      b is LowerBound of X by XXREAL_2:def 4;

      then ( - b) is UpperBound of ( - X) by Th12;

      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;

      :: original: rng

      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

    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;

      :: SUPINF_2:def1

      func sup F -> Element of ExtREAL equals ( sup ( rng F));

      coherence ;

      :: SUPINF_2:def2

      func inf F -> Element of ExtREAL equals ( inf ( rng F));

      coherence ;

    end

    definition

      let F be ext-real-valued Function;

      let x be set;

      :: original: .

      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;

      :: SUPINF_2:def3

      func F + G -> Function of X, (Y + Z) means

      : Def3: for x be Element of X holds (it . x) = ((F . x) + (G . x));

      existence

      proof

        deffunc F( Element of X) = ((F . $1) + (G . $1));

        

         A1: for x be 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 be Function of X, (Y + Z) st for x be Element of X holds (H . x) = F(x) from FUNCT_2:sch 8( A1);

        then

        consider H be Function of X, (Y + Z) such that

         A3: for x be 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 be Element of X holds (H1 . x) = ((F . x) + (G . x)) and

         A5: for x be Element of X holds (H2 . x) = ((F . x) + (G . x));

        for x be object st x in X holds (H1 . x) = (H2 . x)

        proof

          let x be object;

          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 :: SUPINF_2:16

    

     Th15: for 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 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 be object st x in X holds ((F + G) . x) in (( rng F) + ( rng G))

      proof

        let x be object;

        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 :: SUPINF_2:17

    

     Th16: for X be non empty set, Y,Z be non empty Subset of ExtREAL holds for F be Function of X, Y holds for G be 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 Th7;

      ( sup (F + G)) <= ( sup (( rng F) + ( rng G))) by Th15, XXREAL_2: 59;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: SUPINF_2:18

    

     Th17: for X be non empty set holds for Y,Z be non empty Subset of ExtREAL holds for F be Function of X, Y holds for G be 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 Th8;

      ( inf (( rng F) + ( rng G))) <= ( inf (F + G)) by Th15, 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;

      :: SUPINF_2:def4

      func - F -> Function of X, ( - Y) means

      : Def4: for x be Element of X holds (it . x) = ( - (F . x));

      existence

      proof

        deffunc F( Element of X) = ( - (F . $1));

        

         A1: for x be 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 be Function of X, ( - Y) st for x be Element of X holds (H . x) = F(x) from FUNCT_2:sch 8( A1);

        then

        consider H be Function of X, ( - Y) such that

         A2: for x be 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 be Element of X holds (H1 . x) = ( - (F . x)) and

         A4: for x be Element of X holds (H2 . x) = ( - (F . x));

        for x be object st x in X holds (H1 . x) = (H2 . x)

        proof

          let x be object;

          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 :: SUPINF_2:19

    

     Th18: for X be non empty set, Y be non empty Subset of ExtREAL , F be 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 object;

        

         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 be object 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;

      let y be object;

      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 be object 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;

    theorem :: SUPINF_2:20

    

     Th19: for X be non empty set, Y be non empty Subset of ExtREAL holds for F be 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 Th18

      .= ( - ( sup F)) by Th13;

      

      thus ( sup ( - F)) = ( sup ( - ( rng F))) by Th18

      .= ( - ( inf F)) by Th14;

    end;

    definition

      let X be set;

      let Y be Subset of ExtREAL ;

      let F be Function of X, Y;

      :: SUPINF_2:def5

      attr F is bounded_above means

      : Def5: ( sup F) < +infty ;

      :: SUPINF_2:def6

      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;

      :: SUPINF_2:def7

      attr F is bounded means 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 ;

      cluster bounded_above bounded_below -> bounded for Function of X, Y;

      coherence ;

    end

    theorem :: SUPINF_2:21

    for X be non empty set, Y be non empty Subset of ExtREAL , F be Function of X, Y holds F is bounded iff ( sup F) < +infty & -infty < ( inf F) by Def5, Def6;

    theorem :: SUPINF_2:22

    

     Th21: for X be non empty set, Y be non empty Subset of ExtREAL , F be 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

         A1: ( - +infty ) < ( - ( sup F)) by XXREAL_3: 38;

        ( - +infty ) = -infty by XXREAL_3:def 3;

        hence ( - F) is bounded_below by A1, Th19;

      end;

      assume ( - F) is bounded_below;

      then ( - ( inf ( - F))) < ( - -infty ) by XXREAL_3: 38;

      then ( - ( - ( sup F))) < ( - -infty ) by Th19;

      hence thesis by XXREAL_3: 5;

    end;

    theorem :: SUPINF_2:23

    

     Th22: for X be non empty set, Y be non empty Subset of ExtREAL , F be 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 ( - ( inf F)) < ( - -infty ) by XXREAL_3: 38;

        hence ( - F) is bounded_above by Th19, XXREAL_3: 5;

      end;

      assume ( - F) is bounded_above;

      then ( - ( inf F)) < +infty by Th19;

      then ( - +infty ) < ( - ( - ( inf F))) by XXREAL_3: 38;

      hence thesis by XXREAL_3:def 3;

    end;

    theorem :: SUPINF_2:24

    for X be non empty set, Y be non empty Subset of ExtREAL , F be Function of X, Y holds F is bounded iff ( - F) is bounded by Th21, Th22;

    theorem :: SUPINF_2:25

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

    theorem :: SUPINF_2:26

    for X be non empty set, Y be non empty Subset of ExtREAL , F be Function of X, Y, x be 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, XXREAL_0: 4;

    end;

    theorem :: SUPINF_2:27

    

     Th26: for X be non empty set, Y be non empty Subset of ExtREAL , F be Function of X, Y, x be 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, XXREAL_2: 4;

    end;

    theorem :: SUPINF_2:28

    

     Th27: for X be non empty set, Y be non empty Subset of ExtREAL , F be 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, Th26, XXREAL_0: 12;

        assume

         a4: F is bounded_above;

        ( 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 ;

      hence thesis by XXREAL_0: 9;

    end;

    theorem :: SUPINF_2:29

    

     Th28: for X be non empty set, Y be non empty Subset of ExtREAL , F be 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, Th26, XXREAL_0: 9;

        assume

         a4: F is bounded_below;

        ( 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 ;

      hence thesis by XXREAL_0: 12;

    end;

    theorem :: SUPINF_2:30

    for X be non empty set, Y be non empty Subset of ExtREAL , F be Function of X, Y st Y c= REAL holds (F is bounded iff ( inf F) in REAL & ( sup F) in REAL ) by Th27, Th28;

    theorem :: SUPINF_2:31

    

     Th30: for X be non empty set, Y,Z be non empty Subset of ExtREAL holds for F1 be Function of X, Y, F2 be 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;

      

       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 Element of 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;

      ( 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 A1, A2, A4, A7, A9, A8, Th16, XXREAL_0: 4, XXREAL_3:def 1;

      end;

      hence thesis;

    end;

    theorem :: SUPINF_2:32

    

     Th31: for X be non empty set, Y,Z be non empty Subset of ExtREAL holds for F1 be Function of X, Y, F2 be 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;

      

       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 Element of 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;

       -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 A1, A2, A4, A7, A9, A8, Th17, XXREAL_0: 6, XXREAL_3:def 1;

      end;

      hence thesis;

    end;

    theorem :: SUPINF_2:33

    for X be non empty set, Y,Z be non empty Subset of ExtREAL holds for F1 be Function of X, Y, F2 be Function of X, Z st F1 is bounded & F2 is bounded holds (F1 + F2) is bounded by Th31, Th30;

    theorem :: SUPINF_2:34

    

     Th33: ( id NAT ) is sequence of ExtREAL & ( id NAT ) is one-to-one & NAT = ( rng ( id NAT )) & ( rng ( id NAT )) is non empty Subset of ExtREAL

    proof

       NAT c= ExtREAL by NUMBERS: 19, NUMBERS: 31;

      then

      reconsider F = ( id NAT ) as sequence of ExtREAL by FUNCT_2: 7;

      ( rng F) c= ExtREAL ;

      hence thesis;

    end;

    definition

      let D be non empty set, IT be Subset of D;

      :: original: countable

      redefine

      :: SUPINF_2:def8

      attr IT is countable means

      : Def8: IT is empty or ex F be sequence of D st IT = ( rng F);

      compatibility

      proof

        thus IT is countable implies IT is empty or ex F be sequence of D st IT = ( rng F)

        proof

          assume that

           A1: IT is countable and

           A2: not IT is empty;

          consider f be Function such that

           A3: ( dom f) = NAT and

           A4: IT c= ( rng f) by A1, CARD_3: 93;

          consider x be Element of D such that

           A5: x in IT by A2;

          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))) misses ( dom (( NAT \ (f " IT)) --> x));

              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 A3, A9;

            end;

              suppose NAT <> (f " IT);

              then

               A11: ( NAT \ (f " IT)) is non empty by A7, XBOOLE_1: 37;

              ( 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 A11, 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 sequence of D by FUNCT_2:def 1, RELSET_1: 4;

          take F;

          thus thesis by A6;

        end;

        assume

         A12: IT is empty or ex F be sequence of D st IT = ( rng F);

        per cases ;

          suppose IT is empty;

          hence thesis by CARD_4: 1;

        end;

          suppose not IT is empty;

          then

          consider F be sequence of D such that

           A13: IT = ( rng F) by A12;

          ( dom F) = NAT by FUNCT_2:def 1;

          hence thesis by A13, CARD_3: 93;

        end;

      end;

    end

    registration

      cluster countable for non empty Subset of ExtREAL ;

      existence

      proof

        set F = the sequence of ExtREAL ;

        reconsider A = ( rng F) as non empty Subset of ExtREAL ;

        take A;

        assume A is non empty;

        thus thesis;

      end;

    end

    definition

      let IT be set;

      :: SUPINF_2:def9

      attr IT is nonnegative means for x be ExtReal holds x in IT implies 0. <= x;

    end

    registration

      cluster nonnegative for countable Subset of ExtREAL ;

      existence

      proof

        reconsider N = NAT as countable Subset of ExtREAL by Def8, Th33;

        take N;

        thus for x be ExtReal holds x in N implies 0. <= x;

      end;

    end

    ::$Canceled

    definition

      let F be sequence of ExtREAL ;

      :: original: rng

      redefine

      func rng F -> non empty Subset of ExtREAL ;

      coherence

      proof

        ( rng F) c= ExtREAL ;

        hence thesis;

      end;

    end

    definition

      let N be sequence of ExtREAL ;

      :: SUPINF_2:def10

      func Ser (N) -> sequence of ExtREAL means

      : Def11: (it . 0 ) = (N . 0 ) & for n be Nat holds for y be R_eal st y = (it . n) holds (it . (n + 1)) = (y + (N . (n + 1)));

      existence

      proof

        set D = ( rng N);

        defpred P[ set, set, set] means for a,b be R_eal, s be 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 be Nat holds for x be Element of ExtREAL holds ex y be Element of ExtREAL st P[n, x, y]

        proof

          let n be Nat;

          let x be Element of ExtREAL ;

          reconsider y = (x + (N . (n + 1))) as R_eal;

          take y;

          thus thesis;

        end;

        consider F be sequence of ExtREAL such that

         A2: (F . 0 ) = A & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

        take F;

        thus (F . 0 ) = (N . 0 ) by A2;

        let n be Nat;

        reconsider n as Element of NAT by ORDINAL1:def 12;

         P[n, (F . n), (F . (n + 1))] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of ExtREAL such that

         A3: (S1 . 0 ) = (N . 0 ) and

         A4: for n be Nat holds for y be R_eal st y = (S1 . n) holds (S1 . (n + 1)) = (y + (N . (n + 1))) and

         A5: (S2 . 0 ) = (N . 0 ) and

         A6: for n be Nat holds for y be R_eal st y = (S2 . n) holds (S2 . (n + 1)) = (y + (N . (n + 1)));

        defpred P[ object] means (S1 . $1) = (S2 . $1);

        for n be object holds n in NAT implies P[n]

        proof

          let n be object;

          assume

           A7: n in NAT ;

          then

          reconsider n as Element of REAL by NUMBERS: 19;

          reconsider n as Element of NAT by A7;

          

           A8: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be 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 be Nat holds P[k] from NAT_1:sch 2( A9, A8);

          then (S1 . n) = (S2 . n);

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    ::$Canceled

    definition

      let R be Relation;

      :: SUPINF_2:def11

      attr R is nonnegative means ( rng R) is nonnegative;

    end

    definition

      let F be sequence of ExtREAL ;

      :: SUPINF_2:def12

      func SUM (F) -> R_eal equals ( sup ( rng ( Ser F)));

      coherence ;

    end

    theorem :: SUPINF_2:39

    

     Th38: for X be set, F be PartFunc of X, ExtREAL holds F is nonnegative iff for n be 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;

        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;

        end;

          suppose not n in ( dom F);

          hence 0. <= (F . n) by FUNCT_1:def 2;

        end;

      end;

      assume

       A2: for n be Element of X holds 0. <= (F . n);

      let y be ExtReal;

      assume y in ( rng F);

      then ex x be object st x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    theorem :: SUPINF_2:40

    

     Th39: for F be sequence of ExtREAL , n be Nat st F is nonnegative holds (( Ser F) . n) <= (( Ser F) . (n + 1)) & 0. <= (( Ser F) . n)

    proof

      let F be sequence of ExtREAL , n be Nat;

      assume

       A0: F is nonnegative;

      set FF = ( Ser F);

      defpred P[ Nat] means (FF . $1) <= (FF . ($1 + 1)) & 0. <= (FF . $1);

      reconsider y = (FF . 0 ) as R_eal;

      

       A1: (FF . ( 0 + 1)) = (y + (F . 1)) by Def11;

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume that

         A3: (FF . k) <= (FF . (k + 1)) and

         A4: 0. <= (FF . k);

        (FF . ((k + 1) + 1)) = ((FF . (k + 1)) + (F . ((k + 1) + 1))) by Def11;

        hence thesis by A3, A4, Th38, A0, XXREAL_3: 39;

      end;

      (FF . 0 ) = (F . 0 ) by Def11;

      then

       A6: P[ 0 ] by A1, XXREAL_3: 39, A0, Th38;

      for n be Nat holds P[n] from NAT_1:sch 2( A6, A2);

      hence thesis;

    end;

    theorem :: SUPINF_2:41

    

     Th40: for F be sequence of ExtREAL st F is nonnegative holds for n,m be Nat holds (( Ser F) . n) <= (( Ser F) . (n + m))

    proof

      let F be sequence of ExtREAL ;

      assume

       A0: F is nonnegative;

      let n,m be Nat;

      defpred P[ Nat] means (( Ser F) . n) <= (( Ser F) . (n + $1));

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        (( Ser F) . (n + (k + 1))) = (( Ser F) . ((n + k) + 1));

        then

         A2: (( Ser F) . (n + k)) <= (( Ser F) . (n + (k + 1))) by Th39, A0;

        assume (( Ser F) . n) <= (( Ser F) . (n + k));

        hence thesis by A2, XXREAL_0: 2;

      end;

      

       A3: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: SUPINF_2:42

    

     Th41: for F1,F2 be sequence of ExtREAL st (for n be Element of NAT holds (F1 . n) <= (F2 . n)) holds for n be Element of NAT holds (( Ser F1) . n) <= (( Ser F2) . n)

    proof

      let F1,F2 be sequence of ExtREAL ;

      defpred P[ Nat] means (( Ser F1) . $1) <= (( Ser F2) . $1);

      assume

       A1: for n be Element of NAT holds (F1 . n) <= (F2 . n);

      let n be Element of NAT ;

      

       A3: (( Ser F2) . 0 ) = (F2 . 0 ) by Def11;

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be 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 Def11;

        (( Ser F1) . (k + 1)) = ((( Ser F1) . k) + (F1 . (k + 1))) by Def11;

        hence thesis by A6, A8, A7, XXREAL_3: 36;

      end;

      (( Ser F1) . 0 ) = (F1 . 0 ) by Def11;

      then

       A9: P[ 0 ] by A1, A3;

      for n be Nat holds P[n] from NAT_1:sch 2( A9, A5);

      hence thesis;

    end;

    theorem :: SUPINF_2:43

    

     Th42: for F1,F2 be sequence of ExtREAL st (for n be Element of NAT holds (F1 . n) <= (F2 . n)) holds ( SUM F1) <= ( SUM F2)

    proof

      let F1,F2 be sequence of ExtREAL ;

      assume

       A1: for n be Element of NAT holds (F1 . n) <= (F2 . n);

      for x be ExtReal st x in ( rng ( Ser F1)) holds ex y be ExtReal st y in ( rng ( Ser F2)) & x <= y

      proof

        let x be ExtReal;

        

         A2: ( dom ( Ser F1)) = NAT by FUNCT_2:def 1;

        assume x in ( rng ( Ser F1));

        then

        consider n be object 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, Th41, FUNCT_1:def 3;

      end;

      hence thesis by XXREAL_2: 63;

    end;

    ::$Canceled

    theorem :: SUPINF_2:45

    

     Th44: for F be sequence of ExtREAL st F is nonnegative holds (ex n be Element of NAT st (F . n) = +infty ) implies ( SUM F) = +infty

    proof

      let F be sequence of ExtREAL ;

      assume

       A1: F is nonnegative;

      given n be Element of NAT such that

       A2: (F . n) = +infty ;

      

       A3: (ex k be Nat st n = (k + 1)) implies ( SUM F) = +infty

      proof

        given k be 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 Def11;

        (( Ser F) . k) <> -infty by A1, Th39, 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, Def11;

        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 sequence of ExtREAL ;

      :: SUPINF_2:def13

      attr F is summable means ( SUM F) in REAL ;

    end

    theorem :: SUPINF_2:46

    for F be sequence of ExtREAL st F is nonnegative holds (ex n be Element of NAT st (F . n) = +infty ) implies not F is summable by Th44;

    theorem :: SUPINF_2:47

    for F1,F2 be sequence of ExtREAL st F1 is nonnegative & (for n be Element of NAT holds (F1 . n) <= (F2 . n)) holds (F2 is summable implies F1 is summable)

    proof

      let F1,F2 be sequence of ExtREAL ;

      assume F1 is nonnegative;

      then

       A1: 0. <= (( Ser F1) . 0 ) by Th39;

      (( Ser F1) . 0 ) <= ( sup ( rng ( Ser F1))) by FUNCT_2: 4, XXREAL_2: 4;

      then

       A2: ( SUM F1) <> -infty by A1, XXREAL_0: 6;

      assume

       A3: for n be Element of NAT holds (F1 . n) <= (F2 . n);

      assume F2 is summable;

      then

       A4: not ( SUM F1) = +infty by A3, Th42, XXREAL_0: 9;

      ( SUM F1) in REAL or ( SUM F1) in { -infty , +infty } by XBOOLE_0:def 3;

      hence thesis by A4, A2, TARSKI:def 2;

    end;

    theorem :: SUPINF_2:48

    

     Th47: for F be sequence of ExtREAL st F is nonnegative holds for n be Nat st (for r be Element of NAT st n <= r holds (F . r) = 0. ) holds ( SUM F) = (( Ser F) . n)

    proof

      let F be sequence of 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 be Element of NAT st n <= r holds (F . r) = 0. ;

      

       A3: for r be 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 be Nat st r = (n + m) by NAT_1: 10;

        

         A5: for s be 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 Def11;

          (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 be Nat holds P[m] from NAT_1:sch 2( A8, A5);

        hence thesis by A4;

      end;

      

       A9: for r be 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 be Nat such that

         A10: n = (r + m) by NAT_1: 10;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        thus thesis by A1, Th40, A10;

      end;

      for y be ExtReal st y in ( rng ( Ser F)) holds y <= (( Ser F) . n)

      proof

        let y be ExtReal;

        

         A11: ( dom ( Ser F)) = NAT by FUNCT_2:def 1;

        assume y in ( rng ( Ser F));

        then

        consider m be object 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 :: SUPINF_2:49

    

     Th48: for F be sequence of ExtREAL st (for n be Element of NAT holds (F . n) in REAL ) holds for n be Nat holds (( Ser F) . n) in REAL

    proof

      let F be sequence of ExtREAL ;

      defpred P[ Nat] means (( Ser F) . $1) in REAL ;

      assume

       A1: for n be Element of NAT holds (F . n) in REAL ;

      

       A2: for s be Nat st P[s] holds P[(s + 1)]

      proof

        let s be Nat;

        reconsider b = (F . (s + 1)) as Element of REAL by A1;

        reconsider y = (( Ser F) . s) as R_eal;

        assume (( Ser F) . s) in REAL ;

        then

        reconsider a = y as Element of REAL ;

        

         A3: (y + (F . (s + 1))) = (a + b) by XXREAL_3:def 2;

        (( Ser F) . (s + 1)) = (y + (F . (s + 1))) by Def11;

        hence thesis by A3;

      end;

      (( Ser F) . 0 ) = (F . 0 ) by Def11;

      then

       A4: P[ 0 ] by A1;

      thus for s be Nat holds P[s] from NAT_1:sch 2( A4, A2);

    end;

    theorem :: SUPINF_2:50

    for F be sequence of ExtREAL st F is nonnegative & (ex n be Element of NAT st (for k be Element of NAT st n <= k holds (F . k) = 0. ) & (for k be Element of NAT st k <= n holds (F . k) <> +infty )) holds F is summable

    proof

      let F be sequence of ExtREAL ;

      assume

       A1: F is nonnegative;

      given n be Element of NAT such that

       A2: for k be Element of NAT st n <= k holds (F . k) = 0. and

       A3: for k be Element of NAT st k <= n holds (F . k) <> +infty ;

      for s be Element of NAT holds (F . s) in REAL

      proof

        let s be Element of NAT ;

        

         A4: s <= n implies (F . s) in REAL

        proof

          

           A5: (F . s) <> -infty by XXREAL_0: 6, A1, Th38;

          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 by XREAL_0:def 1;

        end;

        hence thesis by A4;

      end;

      then (( Ser F) . n) in REAL by Th48;

      hence thesis by A1, A2, Th47;

    end;

    theorem :: SUPINF_2:51

    for X be set, F be PartFunc of X, ExtREAL holds F is nonnegative iff for n be object 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;

        let n be object;

        per cases ;

          suppose n in ( dom F);

          then (F . n) in ( rng F) by FUNCT_1:def 3;

          hence 0. <= (F . n) by A1;

        end;

          suppose not n in ( dom F);

          hence 0. <= (F . n) by FUNCT_1:def 2;

        end;

      end;

      assume

       A2: for n be object holds 0. <= (F . n);

      let y be ExtReal;

      assume y in ( rng F);

      then ex x be object st x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    theorem :: SUPINF_2:52

    for X be set, F be PartFunc of X, ExtREAL st for n be object 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 be object st n in ( dom F) holds 0. <= (F . n);

      let y be ExtReal;

      assume y in ( rng F);

      then ex x be object st x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

      hence thesis by A1;

    end;

    definition

      :: SUPINF_2:def14

      func 1. -> R_eal equals 1;

      coherence by XXREAL_0:def 1;

    end