:: SUPINF_2 semantic presentation

K19(REAL) is set
{} is set

{{},1} is V23() set
ExtREAL is non empty ext-real-membered set
+infty is V36() set
-infty is V36() set

is set
is V23() set

is V23() V27() set
is V23() set

COMPLEX is non empty V12() V23() complex-membered V46() set

K19(omega) is set

- X is ext-real set

X + F is ext-real set
X - F is ext-real set
- F is ext-real set
X + (- F) is ext-real set

y is V35() V36() ext-real Element of REAL

y is V35() V36() ext-real Element of REAL
(X,F) is ext-real Element of ExtREAL
y + y is V35() V36() ext-real Element of REAL

F is V35() V36() ext-real Element of REAL
(X) is ext-real Element of ExtREAL
- F is V35() V36() ext-real Element of REAL

(X,F) is ext-real Element of ExtREAL
- F is ext-real set
X + (- F) is ext-real set
y is V35() V36() ext-real Element of REAL
y is V35() V36() ext-real Element of REAL
y - y is V35() V36() ext-real Element of REAL
- y is V35() V36() ext-real set
y + (- y) is V35() V36() ext-real set
(F) is ext-real Element of ExtREAL
- y is V35() V36() ext-real Element of REAL
K19(ExtREAL) is set
K19(ExtREAL) is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in X & b2 in F ) } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set

X is non empty ext-real-membered Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
(X) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set

(y) is ext-real Element of ExtREAL
y is non empty ext-real-membered Element of K19(ExtREAL)
(y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in y } is set
X is non empty ext-real-membered Element of K19(ExtREAL)
F is non empty ext-real-membered Element of K19(ExtREAL)
(X) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set
(F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in F } is set
y is non empty ext-real-membered Element of K19(ExtREAL)
(y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in y } is set
y is non empty ext-real-membered Element of K19(ExtREAL)
(y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in y } is set

(X) is ext-real Element of ExtREAL

(F) is ext-real Element of ExtREAL

((X)) is ext-real Element of ExtREAL

X is non empty ext-real-membered Element of K19(ExtREAL)
F is non empty ext-real-membered Element of K19(ExtREAL)
(X,F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in X & b2 in F ) } is set
((X,F)) is ext-real Element of ExtREAL
(X) is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
((X),(F)) is ext-real Element of ExtREAL
y is ext-real set

(y,a) is ext-real Element of ExtREAL
X is non empty ext-real-membered Element of K19(ExtREAL)
(X) is ext-real Element of ExtREAL
F is non empty ext-real-membered Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
((X),(F)) is ext-real Element of ExtREAL
(X,F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in X & b2 in F ) } is set
((X,F)) is ext-real Element of ExtREAL
y is ext-real set

(y,a) is ext-real Element of ExtREAL
X is non empty ext-real-membered Element of K19(ExtREAL)
F is non empty ext-real-membered Element of K19(ExtREAL)
(X,F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in X & b2 in F ) } is set
((X,F)) is ext-real Element of ExtREAL
(X) is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
((X),(F)) is ext-real Element of ExtREAL
X is non empty ext-real-membered Element of K19(ExtREAL)
F is non empty ext-real-membered Element of K19(ExtREAL)
(X) is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
((X),(F)) is ext-real Element of ExtREAL
(X,F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in X & b2 in F ) } is set
((X,F)) is ext-real Element of ExtREAL
X is non empty ext-real-membered Element of K19(ExtREAL)
(X) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set

(F) is ext-real Element of ExtREAL
y is ext-real set

(y) is ext-real Element of ExtREAL
((X)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (X) } is set
((y)) is ext-real Element of ExtREAL
y is ext-real set

(y) is ext-real Element of ExtREAL
X is non empty ext-real-membered Element of K19(ExtREAL)
(X) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set

(F) is ext-real Element of ExtREAL
y is ext-real set

(y) is ext-real Element of ExtREAL
((X)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (X) } is set
((y)) is ext-real Element of ExtREAL
y is ext-real set

(y) is ext-real Element of ExtREAL
X is non empty ext-real-membered Element of K19(ExtREAL)
(X) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set
((X)) is ext-real Element of ExtREAL
(X) is ext-real Element of ExtREAL
((X)) is ext-real Element of ExtREAL
(((X))) is ext-real Element of ExtREAL
((X)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (X) } is set
((((X)))) is ext-real Element of ExtREAL
X is non empty ext-real-membered Element of K19(ExtREAL)
(X) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set
((X)) is ext-real Element of ExtREAL
(X) is ext-real Element of ExtREAL
((X)) is ext-real Element of ExtREAL
(((X))) is ext-real Element of ExtREAL
((X)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (X) } is set
((((X)))) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
rng y is non empty ext-real-membered set
the Element of X is Element of X
y . the Element of X is ext-real Element of F
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set

K19(X) is set
F is set
y is ext-real-membered Element of K19(X)

K19(K20(F,y)) is set

rng y is ext-real-membered Element of K19(y)
K19(y) is set
((rng y)) is ext-real Element of ExtREAL
((rng y)) is ext-real Element of ExtREAL

F is set
X . F is ext-real set
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,y)) is set
(F,y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in F & b2 in y ) } is set
K20(X,(F,y)) is Relation-like ext-real-valued set
K19(K20(X,(F,y))) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
a is Relation-like X -defined y -valued Function-like non empty total V18(X,y) ext-real-valued Element of K19(K20(X,y))
m is Element of X
(y,m) is ext-real Element of ExtREAL
(a,m) is ext-real Element of ExtREAL
((y,m),(a,m)) is ext-real Element of ExtREAL
m is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
m is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
y is Element of X
(m,y) is ext-real Element of ExtREAL
(y,y) is ext-real Element of ExtREAL
(a,y) is ext-real Element of ExtREAL
((y,y),(a,y)) is ext-real Element of ExtREAL
m is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
y is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
k is set
(m,k) is ext-real Element of ExtREAL
(y,k) is ext-real Element of ExtREAL
y2 is Element of X
(m,y2) is ext-real Element of ExtREAL
(y,y2) is ext-real Element of ExtREAL
(a,y2) is ext-real Element of ExtREAL
((y,y2),(a,y2)) is ext-real Element of ExtREAL
(y,y2) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,y)) is set
(F,y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in F & b2 in y ) } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)
a is Relation-like X -defined y -valued Function-like non empty total V18(X,y) ext-real-valued Element of K19(K20(X,y))
(X,F,y,y,a) is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
K20(X,(F,y)) is Relation-like ext-real-valued set
K19(K20(X,(F,y))) is set
(X,(F,y),(X,F,y,y,a)) is non empty ext-real-membered Element of K19(ExtREAL)
(X,y,a) is non empty ext-real-membered Element of K19(ExtREAL)
((X,F,y),(X,y,a)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in (X,F,y) & b2 in (X,y,a) ) } is set
m is set
((X,F,y,y,a),m) is ext-real Element of ExtREAL
y is Element of X
(y,y) is ext-real Element of ExtREAL
(a,y) is ext-real Element of ExtREAL

y2 is ext-real Element of ExtREAL
((X,F,y,y,a),y) is ext-real Element of ExtREAL
(k,y2) is ext-real Element of ExtREAL
dom (X,F,y,y,a) is non empty Element of K19(X)
K19(X) is set
K20(X,((X,F,y),(X,y,a))) is Relation-like ext-real-valued set
K19(K20(X,((X,F,y),(X,y,a)))) is set
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,y)) is set
(F,y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in F & b2 in y ) } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
a is Relation-like X -defined y -valued Function-like non empty total V18(X,y) ext-real-valued Element of K19(K20(X,y))
(X,F,y,y,a) is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
K20(X,(F,y)) is Relation-like ext-real-valued set
K19(K20(X,(F,y))) is set
(ExtREAL,X,(F,y),(X,F,y,y,a)) is ext-real Element of ExtREAL
rng (X,F,y,y,a) is non empty ext-real-membered Element of K19((F,y))
K19((F,y)) is set
((rng (X,F,y,y,a))) is ext-real Element of ExtREAL
(ExtREAL,X,y,a) is ext-real Element of ExtREAL
rng a is non empty ext-real-membered Element of K19(y)
K19(y) is set
((rng a)) is ext-real Element of ExtREAL
((ExtREAL,X,F,y),(ExtREAL,X,y,a)) is ext-real Element of ExtREAL
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)
(X,y,a) is non empty ext-real-membered Element of K19(ExtREAL)
((X,F,y),(X,y,a)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in (X,F,y) & b2 in (X,y,a) ) } is set
(((X,F,y),(X,y,a))) is ext-real Element of ExtREAL
((X,F,y)) is ext-real Element of ExtREAL
((X,y,a)) is ext-real Element of ExtREAL
(((X,F,y)),((X,y,a))) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,y)) is set
(F,y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in F & b2 in y ) } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
a is Relation-like X -defined y -valued Function-like non empty total V18(X,y) ext-real-valued Element of K19(K20(X,y))
(ExtREAL,X,y,a) is ext-real Element of ExtREAL
rng a is non empty ext-real-membered Element of K19(y)
K19(y) is set
((rng a)) is ext-real Element of ExtREAL
((ExtREAL,X,F,y),(ExtREAL,X,y,a)) is ext-real Element of ExtREAL
(X,F,y,y,a) is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
K20(X,(F,y)) is Relation-like ext-real-valued set
K19(K20(X,(F,y))) is set
(ExtREAL,X,(F,y),(X,F,y,y,a)) is ext-real Element of ExtREAL
rng (X,F,y,y,a) is non empty ext-real-membered Element of K19((F,y))
K19((F,y)) is set
((rng (X,F,y,y,a))) is ext-real Element of ExtREAL
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)
((X,F,y)) is ext-real Element of ExtREAL
(X,y,a) is non empty ext-real-membered Element of K19(ExtREAL)
((X,y,a)) is ext-real Element of ExtREAL
(((X,F,y)),((X,y,a))) is ext-real Element of ExtREAL
((X,F,y),(X,y,a)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in (X,F,y) & b2 in (X,y,a) ) } is set
(((X,F,y),(X,y,a))) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
(F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in F } is set
K20(X,(F)) is Relation-like ext-real-valued set
K19(K20(X,(F))) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
y is Element of X
(y,y) is ext-real Element of ExtREAL
((y,y)) is ext-real Element of ExtREAL
y is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
y is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
a is Element of X
(y,a) is ext-real Element of ExtREAL
(y,a) is ext-real Element of ExtREAL
((y,a)) is ext-real Element of ExtREAL
y is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
a is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
m is set
(y,m) is ext-real Element of ExtREAL
(a,m) is ext-real Element of ExtREAL
y is Element of X
(y,y) is ext-real Element of ExtREAL
(y,y) is ext-real Element of ExtREAL
((y,y)) is ext-real Element of ExtREAL
(a,y) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
(F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in F } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(X,F,y) is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
K20(X,(F)) is Relation-like ext-real-valued set
K19(K20(X,(F))) is set
(X,(F),(X,F,y)) is non empty ext-real-membered Element of K19(ExtREAL)
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)
((X,F,y)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (X,F,y) } is set
y is set
dom y is non empty Element of K19(X)
K19(X) is set
dom (X,F,y) is non empty Element of K19(X)

m is set
((X,F,y),m) is ext-real Element of ExtREAL
y is Element of X
(y,y) is ext-real Element of ExtREAL
((y,y)) is ext-real Element of ExtREAL
(a) is ext-real Element of ExtREAL
((a)) is ext-real Element of ExtREAL
y is set

(a) is ext-real Element of ExtREAL
(((X,F,y))) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in ((X,F,y)) } is set
dom y is non empty Element of K19(X)
K19(X) is set
m is set
(y,m) is ext-real Element of ExtREAL
y is Element of X
(y,y) is ext-real Element of ExtREAL
((y,y)) is ext-real Element of ExtREAL
((X,F,y),y) is ext-real Element of ExtREAL
dom (X,F,y) is non empty Element of K19(X)
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
(F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in F } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(X,F,y) is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
K20(X,(F)) is Relation-like ext-real-valued set
K19(K20(X,(F))) is set
(ExtREAL,X,(F),(X,F,y)) is ext-real Element of ExtREAL
rng (X,F,y) is non empty ext-real-membered Element of K19((F))
K19((F)) is set
((rng (X,F,y))) is ext-real Element of ExtREAL
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
((ExtREAL,X,F,y)) is ext-real Element of ExtREAL
(ExtREAL,X,(F),(X,F,y)) is ext-real Element of ExtREAL
((rng (X,F,y))) is ext-real Element of ExtREAL
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
((rng y)) is ext-real Element of ExtREAL
((ExtREAL,X,F,y)) is ext-real Element of ExtREAL
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)
((X,F,y)) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (X,F,y) } is set
(((X,F,y))) is ext-real Element of ExtREAL
(((X,F,y))) is ext-real Element of ExtREAL
X is set

K19(K20(X,F)) is set

X is set

K19(K20(X,F)) is set
X is set

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like V18(X,F) ext-real-valued Element of K19(K20(X,F))
y is Relation-like X -defined F -valued Function-like V18(X,F) ext-real-valued Element of K19(K20(X,F))
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
((rng y)) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
(F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in F } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(X,F,y) is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
K20(X,(F)) is Relation-like ext-real-valued set
K19(K20(X,(F))) is set
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
((ExtREAL,X,F,y)) is ext-real Element of ExtREAL
(+infty) is ext-real Element of ExtREAL
(ExtREAL,X,(F),(X,F,y)) is ext-real Element of ExtREAL
rng (X,F,y) is non empty ext-real-membered Element of K19((F))
K19((F)) is set
((rng (X,F,y))) is ext-real Element of ExtREAL
(-infty) is ext-real Element of ExtREAL
((ExtREAL,X,(F),(X,F,y))) is ext-real Element of ExtREAL
(((ExtREAL,X,F,y))) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
(F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in F } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(X,F,y) is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
K20(X,(F)) is Relation-like ext-real-valued set
K19(K20(X,(F))) is set
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
(-infty) is ext-real Element of ExtREAL
((ExtREAL,X,F,y)) is ext-real Element of ExtREAL
(ExtREAL,X,(F),(X,F,y)) is ext-real Element of ExtREAL
rng (X,F,y) is non empty ext-real-membered Element of K19((F))
K19((F)) is set
((rng (X,F,y))) is ext-real Element of ExtREAL
(((ExtREAL,X,F,y))) is ext-real Element of ExtREAL
(+infty) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
(F) is non empty ext-real-membered Element of K19(ExtREAL)
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in F } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(X,F,y) is Relation-like X -defined (F) -valued Function-like non empty total V18(X,(F)) ext-real-valued Element of K19(K20(X,(F)))
K20(X,(F)) is Relation-like ext-real-valued set
K19(K20(X,(F))) is set
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
a is non empty set
m is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(a,m)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
y is Element of X
(y,y) is ext-real Element of ExtREAL
y is Relation-like a -defined m -valued Function-like non empty total V18(a,m) ext-real-valued Element of K19(K20(a,m))
k is Element of a
(y,k) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
y is Element of X
(y,y) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
((rng y)) is ext-real Element of ExtREAL
y is Element of X
(y,y) is ext-real Element of ExtREAL
dom y is non empty Element of K19(X)
K19(X) is set
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
the Element of X is Element of X
dom y is non empty Element of K19(X)
K19(X) is set
(y, the Element of X) is ext-real Element of ExtREAL
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)

X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
the Element of X is Element of X
dom y is non empty Element of K19(X)
K19(X) is set
(y, the Element of X) is ext-real Element of ExtREAL
(X,F,y) is non empty ext-real-membered Element of K19(ExtREAL)

X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
((rng y)) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,y)) is set
(F,y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in F & b2 in y ) } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
a is Relation-like X -defined y -valued Function-like non empty total V18(X,y) ext-real-valued Element of K19(K20(X,y))
(X,F,y,y,a) is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
K20(X,(F,y)) is Relation-like ext-real-valued set
K19(K20(X,(F,y))) is set
(ExtREAL,X,y,a) is ext-real Element of ExtREAL
rng a is non empty ext-real-membered Element of K19(y)
K19(y) is set
((rng a)) is ext-real Element of ExtREAL
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
((ExtREAL,X,F,y),(ExtREAL,X,y,a)) is ext-real Element of ExtREAL

k is V35() V36() ext-real Element of REAL
y2 is V35() V36() ext-real Element of REAL
k + y2 is V35() V36() ext-real Element of REAL
(ExtREAL,X,(F,y),(X,F,y,y,a)) is ext-real Element of ExtREAL
rng (X,F,y,y,a) is non empty ext-real-membered Element of K19((F,y))
K19((F,y)) is set
((rng (X,F,y,y,a))) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,y)) is set
(F,y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in F & b2 in y ) } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
a is Relation-like X -defined y -valued Function-like non empty total V18(X,y) ext-real-valued Element of K19(K20(X,y))
(X,F,y,y,a) is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
K20(X,(F,y)) is Relation-like ext-real-valued set
K19(K20(X,(F,y))) is set
(ExtREAL,X,y,a) is ext-real Element of ExtREAL
rng a is non empty ext-real-membered Element of K19(y)
K19(y) is set
((rng a)) is ext-real Element of ExtREAL
(ExtREAL,X,F,y) is ext-real Element of ExtREAL
rng y is non empty ext-real-membered Element of K19(F)
K19(F) is set
((rng y)) is ext-real Element of ExtREAL
((ExtREAL,X,F,y),(ExtREAL,X,y,a)) is ext-real Element of ExtREAL

k is V35() V36() ext-real Element of REAL
y2 is V35() V36() ext-real Element of REAL
k + y2 is V35() V36() ext-real Element of REAL
(ExtREAL,X,(F,y),(X,F,y,y,a)) is ext-real Element of ExtREAL
rng (X,F,y,y,a) is non empty ext-real-membered Element of K19((F,y))
K19((F,y)) is set
((rng (X,F,y,y,a))) is ext-real Element of ExtREAL
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)

K19(K20(X,y)) is set
(F,y) is non empty ext-real-membered Element of K19(ExtREAL)
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in F & b2 in y ) } is set
y is Relation-like X -defined F -valued Function-like non empty total V18(X,F) ext-real-valued Element of K19(K20(X,F))
a is Relation-like X -defined y -valued Function-like non empty total V18(X,y) ext-real-valued Element of K19(K20(X,y))
(X,F,y,y,a) is Relation-like X -defined (F,y) -valued Function-like non empty total V18(X,(F,y)) ext-real-valued Element of K19(K20(X,(F,y)))
K20(X,(F,y)) is Relation-like ext-real-valued set
K19(K20(X,(F,y))) is set

K19(K20(NAT,REAL)) is set

K19(K20(NAT,ExtREAL)) is set

rng X is non empty ext-real-membered Element of K19(ExtREAL)
X is non empty set
K19(X) is set
F is Element of K19(X)
K20(NAT,X) is Relation-like set
K19(K20(NAT,X)) is set

dom y is set
rng y is set
y is Element of X
y " F is set
y | (y " F) is Relation-like Function-like set

(NAT \ (y " F)) --> y is Relation-like NAT \ (y " F) -defined X -valued Function-like total V18(NAT \ (y " F),X) Element of K19(K20((NAT \ (y " F)),X))
K20((NAT \ (y " F)),X) is Relation-like set
K19(K20((NAT \ (y " F)),X)) is set
(y | (y " F)) +* ((NAT \ (y " F)) --> y) is Relation-like Function-like set
rng ((y | (y " F)) +* ((NAT \ (y " F)) --> y)) is set
dom ((y | (y " F)) +* ((NAT \ (y " F)) --> y)) is set
dom (y | (y " F)) is set

dom ((NAT \ (y " F)) --> y) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19((NAT \ (y " F)))
K19((NAT \ (y " F))) is set
(dom (y | (y " F))) /\ (dom ((NAT \ (y " F)) --> y)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19((NAT \ (y " F)))
(y | (y " F)) \/ ((NAT \ (y " F)) --> y) is Relation-like set
rng (y | (y " F)) is set
rng ((NAT \ (y " F)) --> y) is Element of K19(X)
(rng (y | (y " F))) \/ (rng ((NAT \ (y " F)) --> y)) is set
(rng (y | (y " F))) \/ {} is set
y .: (y " F) is set
(dom (y | (y " F))) \/ (dom ((NAT \ (y " F)) --> y)) is set
(dom (y | (y " F))) \/ {} is set
dom ((NAT \ (y " F)) --> y) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19((NAT \ (y " F)))
K19((NAT \ (y " F))) is set
(y | (y " F)) \/ ((NAT \ (y " F)) --> y) is Relation-like set
rng (y | (y " F)) is set
rng ((NAT \ (y " F)) --> y) is Element of K19(X)
(rng (y | (y " F))) \/ (rng ((NAT \ (y " F)) --> y)) is set
{y} is V23() set
(rng (y | (y " F))) \/ {y} is set
y .: (y " F) is set
(y .: (y " F)) \/ {y} is set
F \/ {y} is set
(dom (y | (y " F))) \/ (dom ((NAT \ (y " F)) --> y)) is set

m is Relation-like NAT -defined X -valued Function-like non empty total V18( NAT ,X) Element of K19(K20(NAT,X))
rng m is non empty Element of K19(X)
y is Relation-like NAT -defined X -valued Function-like non empty total V18( NAT ,X) Element of K19(K20(NAT,X))
rng y is non empty Element of K19(X)
y is Relation-like NAT -defined X -valued Function-like non empty total V18( NAT ,X) Element of K19(K20(NAT,X))
rng y is non empty Element of K19(X)

K19(NAT) is set

F is non empty ext-real-membered Element of K19(ExtREAL)
() is ext-real Element of ExtREAL
X is non empty ext-real-membered countable Element of K19(ExtREAL)

X is non empty ext-real-membered countable Element of K19(ExtREAL)
X is non empty ext-real-membered countable Element of K19(ExtREAL)

(F,0) is ext-real Element of ExtREAL

(F,(y + 1)) is ext-real Element of ExtREAL
(a,(F,(y + 1))) is ext-real Element of ExtREAL

(F,(y2 + 1)) is ext-real Element of ExtREAL
(y,(F,(y2 + 1))) is ext-real Element of ExtREAL

(y,0) is ext-real Element of ExtREAL

(y,a) is ext-real Element of ExtREAL

(y,(a + 1)) is ext-real Element of ExtREAL
(F,(a + 1)) is ext-real Element of ExtREAL
(m,(F,(a + 1))) is ext-real Element of ExtREAL

(y,0) is ext-real Element of ExtREAL

(y,0) is ext-real Element of ExtREAL
a is set
(y,a) is ext-real Element of ExtREAL
(y,a) is ext-real Element of ExtREAL
m is V35() V36() ext-real Element of REAL

(y,k) is ext-real Element of ExtREAL
(y,k) is ext-real Element of ExtREAL

(y,(k + 1)) is ext-real Element of ExtREAL
(y,(k + 1)) is ext-real Element of ExtREAL
y2 is ext-real Element of ExtREAL
(F,(k + 1)) is ext-real Element of ExtREAL
(y2,(F,(k + 1))) is ext-real Element of ExtREAL

(y,y) is ext-real Element of ExtREAL
(y,y) is ext-real Element of ExtREAL
X is non empty ext-real-membered countable () Element of K19(ExtREAL)

(F,y) is ext-real Element of ExtREAL
rng F is non empty ext-real-membered Element of K19(ExtREAL)
X is non empty ext-real-membered countable () Element of K19(ExtREAL)

((X,F),y) is ext-real Element of ExtREAL

((X,F),(y + 1)) is ext-real Element of ExtREAL

((X,F),(0 + 1)) is ext-real Element of ExtREAL
((X,F),0) is ext-real Element of ExtREAL
(F,1) is ext-real Element of ExtREAL
(((X,F),0),(F,1)) is ext-real Element of ExtREAL

((X,F),a) is ext-real Element of ExtREAL

((X,F),(a + 1)) is ext-real Element of ExtREAL

((X,F),((a + 1) + 1)) is ext-real Element of ExtREAL
(F,((a + 1) + 1)) is ext-real Element of ExtREAL
(((X,F),(a + 1)),(F,((a + 1) + 1))) is ext-real Element of ExtREAL
(F,0) is ext-real Element of ExtREAL
X is non empty ext-real-membered countable () Element of K19(ExtREAL)

((X,F),y) is ext-real Element of ExtREAL

((X,F),(y + y)) is ext-real Element of ExtREAL

((X,F),(y + a)) is ext-real Element of ExtREAL

((X,F),(y + (a + 1))) is ext-real Element of ExtREAL

((X,F),((y + a) + 1)) is ext-real Element of ExtREAL

((X,F),(y + 0)) is ext-real Element of ExtREAL
X is non empty ext-real-membered countable Element of K19(ExtREAL)

X is non empty ext-real-membered countable () Element of K19(ExtREAL)

rng (X,F) is non empty ext-real-membered Element of K19(ExtREAL)
((rng (X,F))) is ext-real Element of ExtREAL
X is non empty ext-real-membered countable () Element of K19(ExtREAL)

rng X is non empty ext-real-membered Element of K19(ExtREAL)

rng X is non empty ext-real-membered set

(X) is non empty ext-real-membered countable Element of K19(ExtREAL)

((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
X is set

K19(K20(X,ExtREAL)) is set

y is Element of X
dom F is Element of K19(X)
K19(X) is set
(F,y) is ext-real Element of ExtREAL
y is Element of X
dom F is Element of K19(X)
K19(X) is set
(F,y) is ext-real Element of ExtREAL
y is Element of X
dom F is Element of K19(X)
K19(X) is set

dom F is Element of K19(X)
K19(X) is set
y is set
(F,y) is ext-real Element of ExtREAL

((X),F) is ext-real Element of ExtREAL

((X),(F + 1)) is ext-real Element of ExtREAL
(X) is non empty ext-real-membered countable Element of K19(ExtREAL)

(X) is non empty ext-real-membered countable Element of K19(ExtREAL)

((X),y) is ext-real Element of ExtREAL

((X),(y + y)) is ext-real Element of ExtREAL

(F) is non empty ext-real-membered countable Element of K19(ExtREAL)
(X) is non empty ext-real-membered countable Element of K19(ExtREAL)

((X),a) is ext-real Element of ExtREAL
((F),a) is ext-real Element of ExtREAL

((F),0) is ext-real Element of ExtREAL
(F,0) is ext-real Element of ExtREAL

((X),m) is ext-real Element of ExtREAL
((F),m) is ext-real Element of ExtREAL

((X),(m + 1)) is ext-real Element of ExtREAL
((F),(m + 1)) is ext-real Element of ExtREAL
(X,(m + 1)) is ext-real Element of ExtREAL
(F,(m + 1)) is ext-real Element of ExtREAL
(((F),m),(F,(m + 1))) is ext-real Element of ExtREAL
(((X),m),(X,(m + 1))) is ext-real Element of ExtREAL
((X),0) is ext-real Element of ExtREAL
(X,0) is ext-real Element of ExtREAL

(X) is ext-real Element of ExtREAL

((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL

((F)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((F))) is ext-real Element of ExtREAL
y is ext-real set

K19(NAT) is set
y is set
((X),y) is ext-real Element of ExtREAL

((F),a) is ext-real Element of ExtREAL

((X),0) is ext-real Element of ExtREAL
(X,0) is ext-real Element of ExtREAL
(X) is non empty ext-real-membered countable Element of K19(ExtREAL)

((X),y) is ext-real Element of ExtREAL

((X),(y + 1)) is ext-real Element of ExtREAL
(X,(y + 1)) is ext-real Element of ExtREAL
(y,(X,(y + 1))) is ext-real Element of ExtREAL

(X) is ext-real Element of ExtREAL

((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL

(X,F) is ext-real Element of ExtREAL

((X),y) is ext-real Element of ExtREAL

((X),(y + 1)) is ext-real Element of ExtREAL

(X,(y + 1)) is ext-real Element of ExtREAL
(a,(X,(y + 1))) is ext-real Element of ExtREAL

((X),0) is ext-real Element of ExtREAL

(X) is ext-real Element of ExtREAL

((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL

(X,F) is ext-real Element of ExtREAL

((X),0) is ext-real Element of ExtREAL
((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
(X) is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL

((F)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((F))) is ext-real Element of ExtREAL

(X) is ext-real Element of ExtREAL

((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL

((X),F) is ext-real Element of ExtREAL

((X),y) is ext-real Element of ExtREAL

F + a is V35() V36() ext-real set
((X),(F + a)) is ext-real Element of ExtREAL

F + (a + 1) is V35() V36() ext-real set
((X),(F + (a + 1))) is ext-real Element of ExtREAL

((X),(y + (m + 1))) is ext-real Element of ExtREAL

(X,(y + (m + 1))) is ext-real Element of ExtREAL
(y,(X,(y + (m + 1)))) is ext-real Element of ExtREAL

F + 0 is V35() V36() ext-real set
((X),(F + 0)) is ext-real Element of ExtREAL

F + a is V35() V36() ext-real set

((X),y) is ext-real Element of ExtREAL

y is ext-real set

K19(NAT) is set
a is set
((X),a) is ext-real Element of ExtREAL

((X),y) is ext-real Element of ExtREAL

((X),F) is ext-real Element of ExtREAL

((X),(F + 1)) is ext-real Element of ExtREAL
(X,(F + 1)) is ext-real Element of ExtREAL

(y,(X,(F + 1))) is ext-real Element of ExtREAL
a is V35() V36() ext-real Element of REAL
y is V35() V36() ext-real Element of REAL
a + y is V35() V36() ext-real Element of REAL
((X),0) is ext-real Element of ExtREAL
(X,0) is ext-real Element of ExtREAL

(X,y) is ext-real Element of ExtREAL

((X),F) is ext-real Element of ExtREAL
(X) is ext-real Element of ExtREAL
((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
X is set

K19(K20(X,ExtREAL)) is set

y is set
dom F is Element of K19(X)
K19(X) is set
(F,y) is ext-real Element of ExtREAL
y is set
dom F is Element of K19(X)
K19(X) is set
(F,y) is ext-real Element of ExtREAL
y is set
dom F is Element of K19(X)
K19(X) is set

dom F is Element of K19(X)
K19(X) is set
y is set
(F,y) is ext-real Element of ExtREAL
X is set

K19(K20(X,ExtREAL)) is set

dom F is Element of K19(X)
K19(X) is set

y is set
(F,y) is ext-real Element of ExtREAL