REAL is non empty V12() V23() complex-membered ext-real-membered real-membered V46() set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() Element of K19(REAL)
K19(REAL) is set
{} is set
RAT is non empty V12() V23() complex-membered ext-real-membered real-membered rational-membered V46() set
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V23() V24() V27() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() complex-valued ext-real-valued real-valued natural-valued set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V23() V24() V27() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() complex-valued ext-real-valued real-valued natural-valued set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
{{},1} is V23() set
ExtREAL is non empty ext-real-membered set
+infty is V36() set
-infty is V36() set
0 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
[0,REAL] is set
{0,REAL} is V23() set
{0} is V23() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{0,REAL},{0}} is V23() V27() set
{+infty,-infty} is V23() set
REAL \/ {+infty,-infty} is set
COMPLEX is non empty V12() V23() complex-membered V46() set
INT is non empty V12() V23() complex-membered ext-real-membered real-membered rational-membered integer-membered V46() set
omega is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() set
K19(omega) is set
- -infty is ext-real set
X is ext-real Element of ExtREAL
- X is ext-real set
F is ext-real Element of ExtREAL
X + F is ext-real set
X - F is ext-real set
- F is ext-real set
X + (- F) is ext-real set
X is ext-real Element of ExtREAL
y is V35() V36() ext-real Element of REAL
F is ext-real Element of ExtREAL
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
X is ext-real Element of ExtREAL
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 is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
(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
X is ext-real-membered Element of K19(ExtREAL)
F is ext-real-membered Element of K19(ExtREAL)
X ++ F is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in X & b2 in F ) } is set
X is ext-real-membered Element of K19(ExtREAL)
-- X is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in X } is set
F is ext-real Element of ExtREAL
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 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
(X) is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
-infty is V36() ext-real Element of ExtREAL
+infty is V36() ext-real Element of ExtREAL
{-infty,+infty} is V23() ext-real-membered set
((X)) is ext-real Element of ExtREAL
X is ext-real-membered set
inf X is ext-real set
sup X is ext-real set
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 is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
(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 is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
(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
(F) is ext-real Element of ExtREAL
y is ext-real set
y is ext-real Element of ExtREAL
(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
(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
(F) is ext-real Element of ExtREAL
y is ext-real set
y is ext-real Element of ExtREAL
(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
(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)
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))
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
X is ext-real-membered set
K19(X) is set
F is set
y is ext-real-membered Element of K19(X)
K20(F,y) is Relation-like ext-real-valued set
K19(K20(F,y)) is set
y is Relation-like F -defined y -valued Function-like ext-real-valued Element of K19(K20(F,y))
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
X is Relation-like Function-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)
K20(X,y) is Relation-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)
K20(X,y) is Relation-like ext-real-valued set
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
k 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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)
K20(X,y) is Relation-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)
K20(X,y) is Relation-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
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)
a is ext-real Element of ExtREAL
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
(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)
K20(X,F) is Relation-like ext-real-valued set
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
F is ext-real-membered Element of K19(ExtREAL)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
+infty is V36() ext-real Element of ExtREAL
-infty is V36() ext-real Element of ExtREAL
X is set
F is ext-real-membered Element of K19(ExtREAL)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
X is set
F is ext-real-membered Element of K19(ExtREAL)
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 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)
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))
(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)
K20(X,F) is Relation-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
a is non empty set
m is non empty ext-real-membered Element of K19(ExtREAL)
K20(a,m) is Relation-like ext-real-valued set
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)
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
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)
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))
(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)
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))
(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)
{-infty,+infty} is V23() ext-real-membered set
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)
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))
(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)
{-infty,+infty} is V23() ext-real-membered set
X is non empty set
F is non empty ext-real-membered Element of K19(ExtREAL)
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))
(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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)
K20(X,y) is Relation-like ext-real-valued set
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
m is ext-real Element of ExtREAL
y 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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)
K20(X,y) is Relation-like ext-real-valued set
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
m is ext-real Element of ExtREAL
y 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)
K20(X,F) is Relation-like ext-real-valued set
K19(K20(X,F)) is set
y is non empty ext-real-membered Element of K19(ExtREAL)
K20(X,y) is Relation-like ext-real-valued set
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
incl NAT is Relation-like NAT -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like one-to-one non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,REAL))
K20(NAT,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K20(NAT,ExtREAL) is Relation-like ext-real-valued set
K19(K20(NAT,ExtREAL)) is set
rng (incl NAT) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
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
y is Relation-like Function-like 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) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)
(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
NAT /\ (y " F) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)
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
(NAT /\ (y " F)) \/ (NAT \ (y " F)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)
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)
dom y is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
K19(NAT) is set
the Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
rng the Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL)) is non empty ext-real-membered Element of K19(ExtREAL)
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)
F 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)
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)
(F,0) is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
a is ext-real Element of ExtREAL
y + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(F,(y + 1)) is ext-real Element of ExtREAL
(a,(F,(y + 1))) is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
y2 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y is ext-real Element of ExtREAL
k is ext-real Element of ExtREAL
y2 + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(F,(y2 + 1)) is ext-real Element of ExtREAL
(y,(F,(y2 + 1))) is ext-real Element of ExtREAL
y is ext-real Element of ExtREAL
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(y,0) is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(y,a) is ext-real Element of ExtREAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(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 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(y,0) is ext-real Element of ExtREAL
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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
k is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(y,k) is ext-real Element of ExtREAL
(y,k) is ext-real Element of ExtREAL
k + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(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 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(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 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(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)
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)
(X,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),y) is ext-real Element of ExtREAL
y + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),(y + 1)) is ext-real Element of ExtREAL
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((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
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),a) is ext-real Element of ExtREAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),(a + 1)) is ext-real Element of ExtREAL
(a + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((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)
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)
(X,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),y) is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y + y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),(y + y)) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y + a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),(y + a)) is ext-real Element of ExtREAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),(y + (a + 1))) is ext-real Element of ExtREAL
(y + a) + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),((y + a) + 1)) is ext-real Element of ExtREAL
y + 0 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X,F),(y + 0)) is ext-real Element of ExtREAL
X is non empty ext-real-membered countable Element of K19(ExtREAL)
the Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)
(X, the Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
rng (X, the Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)) is non empty ext-real-membered Element of K19(ExtREAL)
X is non empty ext-real-membered countable () Element of K19(ExtREAL)
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued (X)
(X,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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)
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
rng X is non empty ext-real-membered Element of K19(ExtREAL)
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
rng X is non empty ext-real-membered set
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is non empty ext-real-membered countable Element of K19(ExtREAL)
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((X))
((X),F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((X))
((X),y) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((X))
((X),F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
X is set
K20(X,ExtREAL) is Relation-like ext-real-valued set
K19(K20(X,ExtREAL)) is set
F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))
rng F is ext-real-membered Element of K19(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
(F,y) is ext-real Element of ExtREAL
y is Element of X
dom F is Element of K19(X)
K19(X) is set
y is ext-real Element of ExtREAL
rng F is ext-real-membered 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 Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
F is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),F) is ext-real Element of ExtREAL
F + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),(F + 1)) is ext-real Element of ExtREAL
(X) is non empty ext-real-membered countable Element of K19(ExtREAL)
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((X))
((X),y) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is non empty ext-real-membered countable Element of K19(ExtREAL)
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),y) is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y + y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),(y + y)) is ext-real Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((X))
((X),F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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)
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),a) is ext-real Element of ExtREAL
((F),a) is ext-real Element of ExtREAL
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((F))
((F),y) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
((F),0) is ext-real Element of ExtREAL
(F,0) is ext-real Element of ExtREAL
y is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((X))
((X),y) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
m is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),m) is ext-real Element of ExtREAL
((F),m) is ext-real Element of ExtREAL
m + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((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 Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is ext-real Element of ExtREAL
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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 Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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
dom (X) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
K19(NAT) is set
y is set
((X),y) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((F),a) is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
dom (F) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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)
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued ((X))
((X),F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
y is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),y) is ext-real Element of ExtREAL
y + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((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 Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is ext-real Element of ExtREAL
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
F is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(X,F) is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real set
y + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),y) is ext-real Element of ExtREAL
y + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),(y + 1)) is ext-real Element of ExtREAL
a 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
m is ext-real Element of ExtREAL
((X),0) is ext-real Element of ExtREAL
y is ext-real Element of ExtREAL
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is ext-real Element of ExtREAL
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
F is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(X,F) is ext-real Element of ExtREAL
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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 Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
((F)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((F))) is ext-real Element of ExtREAL
{-infty,+infty} is V23() ext-real-membered set
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is ext-real Element of ExtREAL
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
((X)) is non empty ext-real-membered countable Element of K19(ExtREAL)
(((X))) is ext-real Element of ExtREAL
F is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real set
((X),F) is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),y) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real set
F + a is V35() V36() ext-real set
((X),(F + a)) is ext-real Element of ExtREAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
F + (a + 1) is V35() V36() ext-real set
((X),(F + (a + 1))) is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
m + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y + (m + 1) is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y + m is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(y + m) + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),(y + (m + 1))) is ext-real Element of ExtREAL
y 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 epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
F + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
F + 0 is V35() V36() ext-real set
((X),(F + 0)) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real set
F + a is V35() V36() ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),y) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real set
y + a is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y + m is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y is ext-real set
dom (X) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
K19(NAT) is set
a is set
((X),a) is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),y) is ext-real Element of ExtREAL
X is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
F is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),F) is ext-real Element of ExtREAL
F + 1 is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
((X),(F + 1)) is ext-real Element of ExtREAL
(X,(F + 1)) is ext-real Element of ExtREAL
y 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 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,ExtREAL))
F is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() Element of NAT
(X,y) is ext-real Element of ExtREAL
{-infty,+infty} is V23() ext-real-membered set
(X) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) ext-real-valued Element of K19(K20(NAT,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
K20(X,ExtREAL) is Relation-like ext-real-valued set
K19(K20(X,ExtREAL)) is set
F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))
rng F is ext-real-membered Element of K19(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
(F,y) is ext-real Element of ExtREAL
y is set
dom F is Element of K19(X)
K19(X) is set
y is ext-real Element of ExtREAL
rng F is ext-real-membered 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
K20(X,ExtREAL) is Relation-like ext-real-valued set
K19(K20(X,ExtREAL)) is set
F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))
dom F is Element of K19(X)
K19(X) is set
y is ext-real Element of ExtREAL
rng F is ext-real-membered set
rng F is ext-real-membered Element of K19(ExtREAL)
y is set
(F,y) is ext-real Element of ExtREAL