:: SUPINF_2 semantic presentation

begin

notation
synonym  0. for  0 ;
end;

definition
:: original: 0.
redefine func 0.  ->  R_eal;
coherence
 0. is R_eal by XXREAL_0:def_1;
let x be R_eal;
:: original: -
redefine func - x ->  R_eal;
coherence
 - x is R_eal by XXREAL_0:def_1;
let y be R_eal;
:: original: +
redefine funcx + y ->  R_eal;
coherence
 x + y is R_eal by XXREAL_0:def_1;
:: original: -
redefine funcx - y ->  R_eal;
coherence
 x - y is R_eal by XXREAL_0:def_1;
end;

theorem :: SUPINF_2:1
for x, y being R_eal
for a, b being Real st x = a & y = b holds
x + y = a + b by XXREAL_3:def_2;

theorem :: SUPINF_2:2
for x being R_eal
for a being Real st x = a holds
- x = - a by XXREAL_3:def_3;

theorem :: SUPINF_2:3
for x, y being R_eal
for a, b being Real st x = a & y = b holds
x - y = a - b
proof
let x, y be R_eal; ::_thesis: for a, b being Real st x = a & y = b holds
x - y = a - b
let a, b be Real; ::_thesis: ( x = a & y = b implies x - y = a - b )
assume A1: x = a ; ::_thesis: ( not y = b or x - y = a - b )
assume  y = b ; ::_thesis: x - y = a - b
then  - y = - b by XXREAL_3:def_3;
hence  x - y = a - b by A1, XXREAL_3:def_2; ::_thesis: verum
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 funcX + Y ->  Subset of ExtREAL;
coherence
 X + Y is Subset of ExtREAL 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
 - X is Subset of ExtREAL by MEMBERED:2;
end;

theorem :: SUPINF_2:4
canceled;

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

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

theorem :: SUPINF_2:7
for z being R_eal holds
( z in REAL iff - z in REAL )
proof
let z be R_eal; ::_thesis: ( z in REAL iff - z in REAL )
A1: for z being R_eal st z in REAL holds
- z in REAL
proof
let z be R_eal; ::_thesis: ( z in REAL implies - z in REAL )
A2: ( - z in REAL or - z in {-infty,+infty} ) by XBOOLE_0:def_3;
assume  z in REAL ; ::_thesis: - z in REAL
hence  - z in REAL by A2, TARSKI:def_2; ::_thesis: verum
end;
 ( - z in REAL implies z in REAL )
proof
assume  - z in REAL ; ::_thesis: z in REAL
then  - (- z) in REAL by A1;
hence  z in REAL ; ::_thesis: verum
end;
hence  ( z in REAL iff - z in REAL ) by A1; ::_thesis: verum
end;

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

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

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

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

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

theorem Th12: :: SUPINF_2:12
for X being non empty Subset of ExtREAL
for a being R_eal holds
( a is UpperBound of X iff - a is LowerBound of - X )
proof
let X be non empty Subset of ExtREAL; ::_thesis: for a being R_eal holds
( a is UpperBound of X iff - a is LowerBound of - X )
let a be R_eal; ::_thesis: ( a is UpperBound of X iff - a is LowerBound of - X )
hereby  ::_thesis: ( - a is LowerBound of - X implies a is UpperBound of X )
assume A1: a is UpperBound of X ; ::_thesis: - a is LowerBound of - X
 for x being ext-real number st x in - X holds
- a <= x
proof
let x be ext-real number ; ::_thesis: ( x in - X implies - a <= x )
assume A2: x in - X ; ::_thesis: - a <= x
reconsider x = x as Element of ExtREAL by XXREAL_0:def_1;
 - x in - (- X) by A2;
then  - x <= a by A1, XXREAL_2:def_1;
then  - a <= - (- x) by XXREAL_3:38;
hence  - a <= x ; ::_thesis: verum
end;
hence  - a is LowerBound of - X by XXREAL_2:def_2; ::_thesis: verum
end;
assume A3: - a is LowerBound of - X ; ::_thesis: a is UpperBound of X
 for x being ext-real number st x in X holds
x <= a
proof
let x be ext-real number ; ::_thesis: ( x in X implies x <= a )
assume A4: x in X ; ::_thesis: x <= a
reconsider x = x as Element of ExtREAL by XXREAL_0:def_1;
 - x in - X by A4;
then  - a <= - x by A3, XXREAL_2:def_2;
hence  x <= a by XXREAL_3:38; ::_thesis: verum
end;
hence  a is UpperBound of X by XXREAL_2:def_1; ::_thesis: verum
end;

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

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

theorem Th15: :: SUPINF_2:15
for X being non empty Subset of ExtREAL holds sup (- X) = - (inf X)
proof
let X be non empty Subset of ExtREAL; ::_thesis: sup (- X) = - (inf X)
set a = sup (- X);
set b = inf X;
 sup (- X) is UpperBound of - X by XXREAL_2:def_3;
then  - (sup (- X)) is LowerBound of - (- X) by Th12;
then  - (sup (- X)) <= inf X by XXREAL_2:def_4;
then A1: - (inf X) <= - (- (sup (- X))) by XXREAL_3:38;
 inf X is LowerBound of X by XXREAL_2:def_4;
then  - (inf X) is UpperBound of - X by Th13;
then  sup (- X) <= - (inf X) by XXREAL_2:def_3;
hence  sup (- X) = - (inf X) by A1, XXREAL_0:1; ::_thesis: verum
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
 rng F is non empty Subset of ExtREAL
proof
set x = the Element of X;
 F . the Element of X in rng F by FUNCT_2:4;
hence  rng F is non empty Subset of ExtREAL by XBOOLE_1:1; ::_thesis: verum
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;
func sup F ->  Element of ExtREAL  equals :: SUPINF_2:def 1
 sup (rng F);
coherence
 sup (rng F) is Element of ExtREAL ;
func inf F ->  Element of ExtREAL  equals :: SUPINF_2:def 2
 inf (rng F);
coherence
 inf (rng F) is Element of ExtREAL ;
end;

:: deftheorem  defines sup SUPINF_2:def_1_:_
 for D being ext-real-membered set
for X being set
for Y being Subset of D
for F being PartFunc of X,Y holds sup F = sup (rng F);

:: deftheorem  defines inf SUPINF_2:def_2_:_
 for D being ext-real-membered set
for X being set
for Y being Subset of D
for F being PartFunc of X,Y holds inf F = inf (rng F);

definition
let F be ext-real-valued Function;
let x be set ;
:: original: .
redefine funcF . x ->  R_eal;
coherence
 F . x is R_eal 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;
funcF + G ->  Function of X,(Y + Z) means :Def3: :: SUPINF_2:def 3
 for x being Element of X holds it . x = (F . x) + (G . x);
existence
 ex b1 being Function of X,(Y + Z) st
for x being Element of X holds b1 . x = (F . x) + (G . x)
proof
deffunc H1( Element of X) ->  R_eal = (F . $1) + (G . $1);
A1: for x being Element of X holds H1(x) in Y + Z
proof
let x be Element of X; ::_thesis: H1(x) in Y + Z
A2: G . x in Z by FUNCT_2:5;
 F . x in Y by FUNCT_2:5;
hence  H1(x) in Y + Z by A2; ::_thesis: verum
end;
 ex H being Function of X,(Y + Z) st
for x being Element of X holds H . x = H1(x) from FUNCT_2:sch_8(A1);
then consider H being Function of X,(Y + Z) such that
A3: for x being Element of X holds H . x = (F . x) + (G . x) ;
take  H ; ::_thesis: for x being Element of X holds H . x = (F . x) + (G . x)
thus  for x being Element of X holds H . x = (F . x) + (G . x) by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of X,(Y + Z) st ( for x being Element of X holds b1 . x = (F . x) + (G . x) ) & ( for x being Element of X holds b2 . x = (F . x) + (G . x) ) holds
b1 = b2
proof
let H1, H2 be Function of X,(Y + Z); ::_thesis: ( ( for x being Element of X holds H1 . x = (F . x) + (G . x) ) & ( for x being Element of X holds H2 . x = (F . x) + (G . x) ) implies H1 = H2 )
assume that
A4: for x being Element of X holds H1 . x = (F . x) + (G . x) and
A5: for x being Element of X holds H2 . x = (F . x) + (G . x) ; ::_thesis: H1 = H2
 for x being set st x in X holds
H1 . x = H2 . x
proof
let x be set ; ::_thesis: ( x in X implies H1 . x = H2 . x )
assume  x in X ; ::_thesis: H1 . x = H2 . x
then reconsider x = x as Element of X ;
H1 . x = (F . x) + (G . x) by A4
.= H2 . x by A5 ;
hence  H1 . x = H2 . x ; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines + SUPINF_2:def_3_:_
 for X being non empty set
for Y, Z being non empty Subset of ExtREAL
for F being Function of X,Y
for G being Function of X,Z
for b6 being Function of X,(Y + Z) holds
( b6 = F + G iff for x being Element of X holds b6 . x = (F . x) + (G . x) );

theorem Th16: :: SUPINF_2:16
for X being non empty set
for Y, Z being non empty Subset of ExtREAL
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 ; ::_thesis: for Y, Z being non empty Subset of ExtREAL
for F being Function of X,Y
for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G)
let Y, Z be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y
for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G)
let F be Function of X,Y; ::_thesis: for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G)
let G be Function of X,Z; ::_thesis: rng (F + G) c= (rng F) + (rng G)
A1: for x being set st x in X holds
(F + G) . x in (rng F) + (rng G)
proof
let x be set ; ::_thesis: ( x in X implies (F + G) . x in (rng F) + (rng G) )
assume  x in X ; ::_thesis: (F + G) . x in (rng F) + (rng G)
then reconsider x = 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  (F + G) . x in (rng F) + (rng G) by A2, A3; ::_thesis: verum
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  rng (F + G) c= (rng F) + (rng G) by RELAT_1:def_19; ::_thesis: verum
end;

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

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

definition
let X be non empty set ;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
func - F ->  Function of X,(- Y) means :Def4: :: SUPINF_2:def 4
 for x being Element of X holds it . x = - (F . x);
existence
 ex b1 being Function of X,(- Y) st
for x being Element of X holds b1 . x = - (F . x)
proof
deffunc H1( Element of X) ->  R_eal = - (F . $1);
A1: for x being Element of X holds H1(x) in - Y
proof
let x be Element of X; ::_thesis: H1(x) in - Y
 F . x in Y by FUNCT_2:5;
hence  H1(x) in - Y ; ::_thesis: verum
end;
 ex H being Function of X,(- Y) st
for x being Element of X holds H . x = H1(x) from FUNCT_2:sch_8(A1);
then consider H being Function of X,(- Y) such that
A2: for x being Element of X holds H . x = - (F . x) ;
take  H ; ::_thesis: for x being Element of X holds H . x = - (F . x)
thus  for x being Element of X holds H . x = - (F . x) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of X,(- Y) st ( for x being Element of X holds b1 . x = - (F . x) ) & ( for x being Element of X holds b2 . x = - (F . x) ) holds
b1 = b2
proof
let H1, H2 be Function of X,(- Y); ::_thesis: ( ( for x being Element of X holds H1 . x = - (F . x) ) & ( for x being Element of X holds H2 . x = - (F . x) ) implies H1 = H2 )
assume 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) ; ::_thesis: H1 = H2
 for x being set st x in X holds
H1 . x = H2 . x
proof
let x be set ; ::_thesis: ( x in X implies H1 . x = H2 . x )
assume  x in X ; ::_thesis: H1 . x = H2 . x
then reconsider x = x as Element of X ;
H1 . x = - (F . x) by A3
.= H2 . x by A4 ;
hence  H1 . x = H2 . x ; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines - SUPINF_2:def_4_:_
 for X being non empty set
for Y being non empty Subset of ExtREAL
for F being Function of X,Y
for b4 being Function of X,(- Y) holds
( b4 = - F iff for x being Element of X holds b4 . x = - (F . x) );

theorem Th19: :: SUPINF_2:19
for X being non empty set
for Y being non empty Subset of ExtREAL
for F being Function of X,Y holds rng (- F) = - (rng F)
proof
let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y holds rng (- F) = - (rng F)
let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds rng (- F) = - (rng F)
let F be Function of X,Y; ::_thesis: rng (- F) = - (rng F)
thus  rng (- F) c= - (rng F) :: according to XBOOLE_0:def_10 ::_thesis: - (rng F) c= rng (- F)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (- F) or y in - (rng F) )
A1: dom F = X by FUNCT_2:def_1;
assume A2: y in rng (- F) ; ::_thesis: y in - (rng F)
then reconsider y = y as R_eal ;
 dom (- F) = X by FUNCT_2:def_1;
then consider a being set  such that
A3: a in X and
A4: y = (- F) . a by A2, FUNCT_1:def_3;
reconsider a = 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  y in - (rng F) ; ::_thesis: verum
end;
thus  - (rng F) c= rng (- F) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in - (rng F) or y in rng (- F) )
assume A5: y in - (rng F) ; ::_thesis: y in rng (- F)
then reconsider y = y as R_eal ;
A6: - y in - (- (rng F)) by A5;
 dom F = X by FUNCT_2:def_1;
then consider a being set  such that
A7: a in X and
A8: - y = F . a by A6, FUNCT_1:def_3;
reconsider a = 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  y in rng (- F) by A9, FUNCT_1:def_3; ::_thesis: verum
end;
end;

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

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

:: deftheorem Def5 defines bounded_above SUPINF_2:def_5_:_
 for X being set
for Y being Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded_above iff sup F < +infty );

:: deftheorem Def6 defines bounded_below SUPINF_2:def_6_:_
 for X being set
for Y being Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded_below iff -infty < inf F );

definition
let X be set ;
let Y be Subset of ExtREAL;
let F be Function of X,Y;
attrF is bounded  means :Def7: :: SUPINF_2:def 7
( F is bounded_above & F is bounded_below );
end;

:: deftheorem Def7 defines bounded SUPINF_2:def_7_:_
 for X being set
for Y being Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded iff ( F is bounded_above & F is bounded_below ) );

registration
let X be set ;
let Y be Subset of ExtREAL;
cluster Function-like V18(X,Y) bounded  ->  bounded_above bounded_below for Element of K19(K20(X,Y));
coherence
 for b1 being Function of X,Y st b1 is bounded holds
( b1 is bounded_above & b1 is bounded_below ) by Def7;
cluster Function-like V18(X,Y) bounded_above bounded_below  ->  bounded for Element of K19(K20(X,Y));
coherence
 for b1 being Function of X,Y st b1 is bounded_above & b1 is bounded_below holds
b1 is bounded by Def7;
end;

theorem :: SUPINF_2:21
for X being non empty set
for Y being non empty Subset of ExtREAL
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 ; ::_thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y holds
( F is bounded iff ( sup F < +infty & -infty < inf F ) )
let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds
( F is bounded iff ( sup F < +infty & -infty < inf F ) )
let F be Function of X,Y; ::_thesis: ( F is bounded iff ( sup F < +infty & -infty < inf F ) )
thus  ( F is bounded implies ( sup F < +infty & -infty < inf F ) ) by Def5, Def6; ::_thesis: ( sup F < +infty & -infty < inf F implies F is bounded )
assume that
A1: sup F < +infty and
A2: -infty < inf F ; ::_thesis: F is bounded
A3: F is bounded_below by A2, Def6;
 F is bounded_above by A1, Def5;
hence  F is bounded by A3; ::_thesis: verum
end;

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

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

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

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

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

theorem Th27: :: SUPINF_2:27
for X being non empty set
for Y being non empty Subset of ExtREAL
for F being Function of X,Y
for x being Element of X holds
( inf F <= F . x & F . x <= sup F )
proof
let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y
for x being Element of X holds
( inf F <= F . x & F . x <= sup F )
let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y
for x being Element of X holds
( inf F <= F . x & F . x <= sup F )
let F be Function of X,Y; ::_thesis: for x being Element of X holds
( inf F <= F . x & F . x <= sup F )
let x be Element of X; ::_thesis: ( inf F <= F . x & F . x <= sup F )
 X = dom F by FUNCT_2:def_1;
then  F . x in rng F by FUNCT_1:def_3;
hence  ( inf F <= F . x & F . x <= sup F ) by XXREAL_2:3, XXREAL_2:4; ::_thesis: verum
end;

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

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

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

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

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

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

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

definition
let D be non empty set ;
let IT be Subset of D;
:: original: countable
redefine attrIT is countable  means :Def8: :: SUPINF_2:def 8
( IT is empty or ex F being Function of NAT,D st IT = rng F );
compatibility
 ( IT is countable iff ( IT is empty or ex F being Function of NAT,D st IT = rng F ) )
proof
thus  ( not IT is countable or IT is empty or ex F being Function of NAT,D st IT = rng F ) ::_thesis: ( ( IT is empty or ex F being Function of NAT,D st IT = rng F ) implies IT is countable )
proof
assume that
A1: IT is countable and
A2: not IT is empty ; ::_thesis: ex F being Function of NAT,D st IT = rng F
consider f being Function such that
A3: dom f = NAT and
A4: IT c= rng f by A1, CARD_3:93;
consider x being Element of D such that
A5: x in IT by A2, SUBSET_1:4;
set F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x);
A6: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = 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;
percases ( NAT = f " IT or NAT <> f " IT ) ;
supposeA9: NAT = f " IT ; ::_thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )
then A10: NAT \ (f " IT) = {} by XBOOLE_1:37;
then  dom ((NAT \ (f " IT)) --> x) = {} ;
then  (dom (f | (f " IT))) /\ (dom ((NAT \ (f " IT)) --> x)) = {} ;
then  dom (f | (f " IT)) misses dom ((NAT \ (f " IT)) --> x) by XBOOLE_0:def_7;
then  (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by FUNCT_4:31;
hence  rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (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 ;
::_thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT
thus  dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def_1
.= (dom (f | (f " IT))) \/ {} by A10
.= NAT by A8, A9 ; ::_thesis: verum
end;
supposeA11: NAT <> f " IT ; ::_thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )
A12: now__::_thesis:_not_NAT_\_(f_"_IT)_is_empty
assume  NAT \ (f " IT) is empty ; ::_thesis: contradiction
then  NAT c= f " IT by XBOOLE_1:37;
hence  contradiction by A7, A11, XBOOLE_0:def_10; ::_thesis: verum
end;
 dom ((NAT \ (f " IT)) --> x) = NAT \ (f " IT) by FUNCOP_1:13;
then  (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by A8, FUNCT_4:31, XBOOLE_1:89;
hence  rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12
.= (rng (f | (f " IT))) \/ {x} by A12, FUNCOP_1:8
.= (f .: (f " IT)) \/ {x} by RELAT_1:115
.= IT \/ {x} by A4, FUNCT_1:77
.= IT by A5, ZFMISC_1:40 ;
::_thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT
thus  dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (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 ; ::_thesis: verum
end;
end;
end;
then reconsider F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) as Function of NAT,D by FUNCT_2:def_1, RELSET_1:4;
take  F ; ::_thesis: IT = rng F
thus  IT = rng F by A6; ::_thesis: verum
end;
assume A13: ( IT is empty or ex F being Function of NAT,D st IT = rng F ) ; ::_thesis: IT is countable
percases ( IT is empty or not IT is empty ) ;
suppose IT is empty ; ::_thesis: IT is countable
hence  IT is countable by CARD_4:1; ::_thesis: verum
end;
suppose not IT is empty ; ::_thesis: IT is countable
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_3:93; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def8 defines countable SUPINF_2:def_8_:_
 for D being non empty set
for IT being Subset of D holds
( IT is countable iff ( IT is empty or ex F being Function of NAT,D st IT = rng F ) );

registration
cluster non empty ext-real-membered V78() for Element of K19(ExtREAL);
existence
 not for b1 being non empty Subset of ExtREAL holds b1 is V78()
proof
set F = the Function of NAT,ExtREAL;
reconsider A = rng the Function of NAT,ExtREAL as non empty Subset of ExtREAL ;
take  A ; ::_thesis: A is V78()
assume  not A is empty ; :: according to SUPINF_2:def_8 ::_thesis: ex F being Function of NAT,ExtREAL st A = rng F
thus  ex F being Function of NAT,ExtREAL st A = rng F ; ::_thesis: verum
end;
end;

definition
mode Denum_Set_of_R_EAL is non empty V78() Subset of ExtREAL;
end;

definition
let IT be set ;
attrIT is nonnegative  means :Def9: :: SUPINF_2:def 9
 for x being R_eal st x in IT holds
0. <= x;
end;

:: deftheorem Def9 defines nonnegative SUPINF_2:def_9_:_
 for IT being set holds
( IT is nonnegative iff for x being R_eal st x in IT holds
0. <= x );

registration
cluster non empty ext-real-membered countable nonnegative for Element of K19(ExtREAL);
existence
 ex b1 being Denum_Set_of_R_EAL st b1 is nonnegative
proof
reconsider N = NAT as Denum_Set_of_R_EAL by Def8, Th34;
take  N ; ::_thesis: N is nonnegative
thus  for x being R_eal st x in N holds
0. <= x by NAT_1:2; :: according to SUPINF_2:def_9 ::_thesis: verum
end;
end;

definition
mode Pos_Denum_Set_of_R_EAL is nonnegative Denum_Set_of_R_EAL;
end;

definition
let D be Denum_Set_of_R_EAL;
mode Num of D ->  Function of NAT,ExtREAL means :Def10: :: SUPINF_2:def 10
D = rng it;
existence
 ex b1 being Function of NAT,ExtREAL st D = rng b1 by Def8;
end;

:: deftheorem Def10 defines Num SUPINF_2:def_10_:_
 for D being Denum_Set_of_R_EAL
for b2 being Function of NAT,ExtREAL holds
( b2 is Num of D iff D = rng b2 );

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

:: deftheorem Def11 defines Ser SUPINF_2:def_11_:_
 for D being Denum_Set_of_R_EAL
for N being Num of D
for b3 being Function of NAT,ExtREAL holds
( b3 = Ser (D,N) iff ( b3 . 0 = N . 0 & ( for n being Element of NAT
for y being R_eal st y = b3 . n holds
b3 . (n + 1) = y + (N . (n + 1)) ) ) );

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

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

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

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

:: deftheorem  defines Set_of_Series SUPINF_2:def_12_:_
 for D being Denum_Set_of_R_EAL
for b2 being non empty Subset of ExtREAL holds
( b2 is Set_of_Series of D iff ex N being Num of D st b2 = rng (Ser (D,N)) );

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

:: deftheorem  defines SUM SUPINF_2:def_13_:_
 for D being Pos_Denum_Set_of_R_EAL
for N being Num of D holds SUM (D,N) = sup (rng (Ser (D,N)));

definition
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
predD is_sumable N means :: SUPINF_2:def 14
 SUM (D,N) in REAL ;
end;

:: deftheorem  defines is_sumable SUPINF_2:def_14_:_
 for D being Pos_Denum_Set_of_R_EAL
for N being Num of D holds
( D is_sumable N iff SUM (D,N) in REAL );

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

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

definition
let F be Function of NAT,ExtREAL;
func Ser F ->  Function of NAT,ExtREAL means :Def15: :: SUPINF_2:def 15
 for N being Num of rng F st N = F holds
it = Ser ((rng F),N);
existence
 ex b1 being Function of NAT,ExtREAL st
for N being Num of rng F st N = F holds
b1 = Ser ((rng F),N)
proof
reconsider N = F as Num of rng F by Def10;
take  Ser ((rng F),N) ; ::_thesis: for N being Num of rng F st N = F holds
Ser ((rng F),N) = Ser ((rng F),N)
thus  for N being Num of rng F st N = F holds
Ser ((rng F),N) = Ser ((rng F),N) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for N being Num of rng F st N = F holds
b1 = Ser ((rng F),N) ) & ( for N being Num of rng F st N = F holds
b2 = Ser ((rng F),N) ) holds
b1 = b2
proof
reconsider N = F as Num of rng F by Def10;
let S1, S2 be Function of NAT,ExtREAL; ::_thesis: ( ( for N being Num of rng F st N = F holds
S1 = Ser ((rng F),N) ) & ( for N being Num of rng F st N = F holds
S2 = Ser ((rng F),N) ) implies S1 = S2 )
assume that
A1: for N being Num of rng F st N = F holds
S1 = Ser ((rng F),N) and
A2: for N being Num of rng F st N = F holds
S2 = Ser ((rng F),N) ; ::_thesis: S1 = S2
thus S1 = Ser ((rng F),N) by A1
.= S2 by A2 ; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines Ser SUPINF_2:def_15_:_
 for F, b2 being Function of NAT,ExtREAL holds
( b2 = Ser F iff for N being Num of rng F st N = F holds
b2 = Ser ((rng F),N) );

definition
let R be Relation;
attrR is nonnegative  means :Def16: :: SUPINF_2:def 16
 rng R is nonnegative ;
end;

:: deftheorem Def16 defines nonnegative SUPINF_2:def_16_:_
 for R being Relation holds
( R is nonnegative iff rng R is nonnegative );

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

:: deftheorem  defines SUM SUPINF_2:def_17_:_
 for F being Function of NAT,ExtREAL holds SUM F = sup (rng (Ser F));

theorem Th39: :: SUPINF_2:39
for X being set
for F being PartFunc of X,ExtREAL holds
( F is nonnegative iff for n being Element of X holds 0. <= F . n )
proof
let X be set ; ::_thesis: for F being PartFunc of X,ExtREAL holds
( F is nonnegative iff for n being Element of X holds 0. <= F . n )
let F be PartFunc of X,ExtREAL; ::_thesis: ( F is nonnegative iff for n being Element of X holds 0. <= F . n )
hereby  ::_thesis: ( ( for n being Element of X holds 0. <= F . n ) implies F is nonnegative )
assume  F is nonnegative ; ::_thesis: for n being Element of X holds 0. <= F . b2
then A1: rng F is nonnegative by Def16;
let n be Element of X; ::_thesis: 0. <= F . b1
percases ( n in dom F or not n in dom F ) ;
suppose n in dom F ; ::_thesis: 0. <= F . b1
then  F . n in rng F by FUNCT_1:def_3;
hence  0. <= F . n by A1, Def9; ::_thesis: verum
end;
suppose not n in dom F ; ::_thesis: 0. <= F . b1
hence  0. <= F . n by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for n being Element of X holds 0. <= F . n ; ::_thesis: F is nonnegative
let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( y in rng F implies 0. <= y )
assume  y in rng F ; ::_thesis: 0. <= y
then  ex x being set st
( x in dom F & y = F . x ) by FUNCT_1:def_3;
hence  0. <= y by A2; ::_thesis: verum
end;

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

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

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

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

theorem Th44: :: SUPINF_2:44
for F being Function of NAT,ExtREAL holds
( (Ser F) . 0 = F . 0 & ( for n being Element of NAT
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; ::_thesis: ( (Ser F) . 0 = F . 0 & ( for n being Element of NAT
for y being R_eal st y = (Ser F) . n holds
(Ser F) . (n + 1) = y + (F . (n + 1)) ) )
reconsider N = F as Num of rng F by Def10;
 Ser F = Ser ((rng F),N) by Def15;
hence  ( (Ser F) . 0 = F . 0 & ( for n being Element of NAT
for y being R_eal st y = (Ser F) . n holds
(Ser F) . (n + 1) = y + (F . (n + 1)) ) ) by Def11; ::_thesis: verum
end;

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

definition
let F be Function of NAT,ExtREAL;
attrF is summable  means :Def18: :: SUPINF_2:def 18
 SUM F in REAL ;
end;

:: deftheorem Def18 defines summable SUPINF_2:def_18_:_
 for F being Function of NAT,ExtREAL holds
( F is summable iff SUM F in REAL );

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

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

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

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

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

theorem :: SUPINF_2:51
for X being set
for F being PartFunc of X,ExtREAL holds
( F is nonnegative iff for n being set holds 0. <= F . n )
proof
let X be set ; ::_thesis: for F being PartFunc of X,ExtREAL holds
( F is nonnegative iff for n being set holds 0. <= F . n )
let F be PartFunc of X,ExtREAL; ::_thesis: ( F is nonnegative iff for n being set holds 0. <= F . n )
hereby  ::_thesis: ( ( for n being set holds 0. <= F . n ) implies F is nonnegative )
assume  F is nonnegative ; ::_thesis: for n being set holds 0. <= F . b2
then A1: rng F is nonnegative by Def16;
let n be set ; ::_thesis: 0. <= F . b1
percases ( n in dom F or not n in dom F ) ;
suppose n in dom F ; ::_thesis: 0. <= F . b1
then  F . n in rng F by FUNCT_1:def_3;
hence  0. <= F . n by A1, Def9; ::_thesis: verum
end;
suppose not n in dom F ; ::_thesis: 0. <= F . b1
hence  0. <= F . n by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for n being set holds 0. <= F . n ; ::_thesis: F is nonnegative
let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( y in rng F implies 0. <= y )
assume  y in rng F ; ::_thesis: 0. <= y
then  ex x being set st
( x in dom F & y = F . x ) by FUNCT_1:def_3;
hence  0. <= y by A2; ::_thesis: verum
end;

theorem :: SUPINF_2:52
for X being set
for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds
0. <= F . n ) holds
F is nonnegative
proof
let X be set ; ::_thesis: for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds
0. <= F . n ) holds
F is nonnegative
let F be PartFunc of X,ExtREAL; ::_thesis: ( ( for n being set st n in dom F holds
0. <= F . n ) implies F is nonnegative )
assume A1: for n being set st n in dom F holds
0. <= F . n ; ::_thesis: F is nonnegative
let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( y in rng F implies 0. <= y )
assume  y in rng F ; ::_thesis: 0. <= y
then  ex x being set st
( x in dom F & y = F . x ) by FUNCT_1:def_3;
hence  0. <= y by A1; ::_thesis: verum
end;