:: SUPINF_2 semantic presentation

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

{ (b

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

-- X is ext-real-membered set

{ (- b

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)

{ (- b

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)

{ (- b

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)

{ (- b

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

{ (- b

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

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

{ (- b

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

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

{ (- b

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)

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (- b

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)

{ (- b

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

{ (- b

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)

{ (- b

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

{ (- b

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

{ (- b

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

{ (- b

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

{ (- b

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

{ (b

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)

{ (b

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)

{ (b

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)

{ (b

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)

{ (b

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

{ (b

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)

{ (b

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

{ (- b

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)

{ (- b

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)

{ (- b

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)

{ (- b

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)

{ (- b

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)

{ (- b

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

{ (- b

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)

{ (- b

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)

{ (- b

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)

{ (b

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)

{ (b

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)

{ (b

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