:: MESFUNC8 semantic presentation

REAL is non empty V33() V57() V58() V59() V63() non with_non-empty_elements set

NAT is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() non with_non-empty_elements Element of bool REAL

bool REAL is non empty set

ExtREAL is non empty V58() set

[:NAT,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:NAT,ExtREAL:] is non empty set

bool ExtREAL is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() non with_non-empty_elements set

bool omega is non empty set

bool NAT is non empty set

COMPLEX is non empty V33() V57() V63() set

[:NAT,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is non empty set

RAT is non empty V33() V57() V58() V59() V60() V63() set

INT is non empty V33() V57() V58() V59() V60() V61() V63() set

bool (bool REAL) is non empty set

bool RAT is non empty set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-zero empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

{{},1} is non empty V57() V58() V59() V60() V61() V62() set

[:COMPLEX,COMPLEX:] is non empty Relation-like complex-valued set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set

bool [:COMPLEX,REAL:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like complex-valued set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is non empty Relation-like RAT -valued complex-valued ext-real-valued real-valued set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued complex-valued ext-real-valued real-valued set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:[:NAT,NAT:],NAT:] is non empty set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-zero empty-yielding RAT -valued Function-like one-to-one constant functional V44() V46() complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() Element of NAT

0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-zero empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() Element of ExtREAL

K533() is non empty non real ext-real positive non negative Element of ExtREAL

{K533()} is non empty V58() set

K534() is non empty non real ext-real non positive negative Element of ExtREAL

{K534()} is non empty V58() set

+infty is non empty non real ext-real positive non negative set

-infty is non empty non real ext-real non positive negative set

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

S is non empty compl-closed sigma-multiplicative Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:S,ExtREAL:] is non empty set

[:NAT,S:] is non empty Relation-like set

bool [:NAT,S:] is non empty set

f is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

{ b

( not g <= b

LN is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]

MRLN is set

rng LN is non empty Element of bool S

bool S is non empty set

e0 is set

e is set

LN . e is set

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

g + G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . (g + G) is Element of S

L is Element of X

meet (rng LN) is set

MRLN is set

e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

e0 - g is V11() real ext-real set

- g is V11() real ext-real non positive set

e0 + (- g) is V11() real ext-real set

e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

LN . e is Element of S

g + e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . (g + e) is Element of S

f . e0 is Element of S

X is non empty set

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

[:NAT,(bool X):] is non empty Relation-like set

bool [:NAT,(bool X):] is non empty set

S is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

superior_setsequence S is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]

inferior_setsequence S is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]

M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

(superior_setsequence S) . M is Element of bool X

S ^\ M is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

rng (S ^\ M) is non empty Element of bool (bool X)

bool (bool X) is non empty set

union (rng (S ^\ M)) is Element of bool X

(inferior_setsequence S) . M is Element of bool X

meet (rng (S ^\ M)) is Element of bool X

{ (S . b

meet { (S . b

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty Relation-like set

bool [:NAT,(bool X):] is non empty set

S is non empty compl-closed sigma-multiplicative Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:S,ExtREAL:] is non empty set

[:NAT,S:] is non empty Relation-like set

bool [:NAT,S:] is non empty set

M is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of bool [:S,ExtREAL:]

f is non empty Relation-like NAT -defined bool X -valued S -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

inferior_setsequence f is non empty Relation-like NAT -defined S -valued bool X -valued Function-like total V30( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]

lim_inf f is Element of bool X

inferior_setsequence f is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]

Union (inferior_setsequence f) is Element of bool X

rng (inferior_setsequence f) is non empty set

union (rng (inferior_setsequence f)) is set

M . (lim_inf f) is ext-real Element of ExtREAL

rng (inferior_setsequence f) is non empty Element of bool S

bool S is non empty set

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

g is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]

g . E is Element of S

g . (E + 1) is Element of S

rng g is non empty Element of bool S

union (rng g) is set

M . (union (rng g)) is ext-real Element of ExtREAL

M * g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (M * g) is non empty V58() countable Element of bool ExtREAL

sup (rng (M * g)) is ext-real Element of ExtREAL

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty Relation-like set

bool [:NAT,(bool X):] is non empty set

S is non empty compl-closed sigma-multiplicative Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:S,ExtREAL:] is non empty set

[:NAT,S:] is non empty Relation-like set

bool [:NAT,S:] is non empty set

M is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of bool [:S,ExtREAL:]

f is non empty Relation-like NAT -defined bool X -valued S -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

Union f is set

rng f is non empty set

union (rng f) is set

M . (Union f) is ext-real Element of ExtREAL

superior_setsequence f is non empty Relation-like NAT -defined S -valued bool X -valued Function-like total V30( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]

lim_sup f is Element of bool X

superior_setsequence f is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]

K320(X,(superior_setsequence f)) is Element of bool X

M . (lim_sup f) is ext-real Element of ExtREAL

rng (superior_setsequence f) is non empty Element of bool S

bool S is non empty set

g is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]

MRLN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

MRLN + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

g . (MRLN + 1) is Element of S

g . MRLN is Element of S

g . 0 is Element of S

{ (f . b

union { (f . b

rng f is non empty Element of bool S

union (rng f) is set

E is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

lim_sup E is Element of bool X

superior_setsequence E is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]

K320(X,(superior_setsequence E)) is Element of bool X

MRLN is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

meet MRLN is Element of bool X

rng MRLN is non empty set

meet (rng MRLN) is set

e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

MRLN . e0 is Element of bool X

E ^\ e0 is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

Union (E ^\ e0) is set

rng (E ^\ e0) is non empty set

union (rng (E ^\ e0)) is set

LN is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

LN . e0 is Element of bool X

rng g is non empty Element of bool S

meet (rng g) is set

M . (meet (rng g)) is ext-real Element of ExtREAL

M * g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (M * g) is non empty V58() countable Element of bool ExtREAL

inf (rng (M * g)) is ext-real Element of ExtREAL

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty Relation-like set

bool [:NAT,(bool X):] is non empty set

S is non empty compl-closed sigma-multiplicative Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:S,ExtREAL:] is non empty set

[:NAT,S:] is non empty Relation-like set

bool [:NAT,S:] is non empty set

M is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of bool [:S,ExtREAL:]

f is non empty Relation-like NAT -defined bool X -valued S -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

inferior_setsequence f is non empty Relation-like NAT -defined S -valued bool X -valued Function-like total V30( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]

lim_sup f is Element of bool X

superior_setsequence f is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]

K320(X,(superior_setsequence f)) is Element of bool X

M . (lim_sup f) is ext-real Element of ExtREAL

lim_inf f is Element of bool X

inferior_setsequence f is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]

Union (inferior_setsequence f) is Element of bool X

rng (inferior_setsequence f) is non empty set

union (rng (inferior_setsequence f)) is set

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

S is non empty compl-closed sigma-multiplicative Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:S,ExtREAL:] is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty Relation-like set

bool [:NAT,(bool X):] is non empty set

f is non empty Relation-like NAT -defined S -valued bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]

M is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of bool [:S,ExtREAL:]

Union f is set

rng f is non empty set

union (rng f) is set

M . (Union f) is ext-real Element of ExtREAL

[:NAT,S:] is non empty Relation-like set

bool [:NAT,S:] is non empty set

superior_setsequence f is non empty Relation-like NAT -defined S -valued bool X -valued Function-like total V30( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]

lim_sup f is Element of bool X

superior_setsequence f is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]

K320(X,(superior_setsequence f)) is Element of bool X

M . (lim_sup f) is ext-real Element of ExtREAL

X is set

S is set

PFuncs (X,S) is non empty functional set

[:NAT,(PFuncs (X,S)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,S)):] is non empty set

X is set

S is set

PFuncs (X,S) is non empty functional set

[:NAT,(PFuncs (X,S)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,S)):] is non empty set

M is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V30( NAT , PFuncs (X,S)) Element of bool [:NAT,(PFuncs (X,S)):]

f is Relation-like Function-like set

rng M is non empty functional Element of bool (PFuncs (X,S))

bool (PFuncs (X,S)) is non empty set

g is Relation-like Function-like set

dom M is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT

E is set

M . E is Relation-like Function-like set

LN is set

M . LN is Relation-like Function-like set

MRLN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . MRLN is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

[:X,S:] is Relation-like set

bool [:X,S:] is non empty set

dom (M . MRLN) is Element of bool X

bool X is non empty set

e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . e0 is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (M . e0) is Element of bool X

dom f is set

dom g is set

rng M is non empty functional Element of bool (PFuncs (X,S))

bool (PFuncs (X,S)) is non empty set

dom M is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . g is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

[:X,S:] is Relation-like set

bool [:X,S:] is non empty set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . f is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (M . f) is Element of bool X

bool X is non empty set

dom (M . g) is Element of bool X

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . f is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

[:X,S:] is Relation-like set

bool [:X,S:] is non empty set

dom (M . f) is Element of bool X

bool X is non empty set

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . g is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (M . g) is Element of bool X

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . E is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (M . E) is Element of bool X

LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . LN is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (M . LN) is Element of bool X

X is set

S is set

PFuncs (X,S) is non empty functional set

[:NAT,(PFuncs (X,S)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,S)):] is non empty set

<:{},X,S:> is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

[:X,S:] is Relation-like set

bool [:X,S:] is non empty set

M is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V30( NAT , PFuncs (X,S)) Element of bool [:NAT,(PFuncs (X,S)):]

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . f is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (M . f) is Element of bool X

bool X is non empty set

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . g is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (M . g) is Element of bool X

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . 0) is Element of bool X

bool X is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Element of X

M /. f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inf (S # f) is ext-real Element of ExtREAL

rng (S # f) is non empty V58() countable Element of bool ExtREAL

inf (rng (S # f)) is ext-real Element of ExtREAL

M . f is ext-real Element of ExtREAL

f is set

g is set

f is Element of X

M . f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inf (S # f) is ext-real Element of ExtREAL

rng (S # f) is non empty V58() countable Element of bool ExtREAL

inf (rng (S # f)) is ext-real Element of ExtREAL

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom f is Element of bool X

g is Element of X

M /. g is ext-real Element of ExtREAL

M . g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inf (S # g) is ext-real Element of ExtREAL

rng (S # g) is non empty V58() countable Element of bool ExtREAL

inf (rng (S # g)) is ext-real Element of ExtREAL

f . g is ext-real Element of ExtREAL

f /. g is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . 0) is Element of bool X

bool X is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Element of X

M /. f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup (S # f) is ext-real Element of ExtREAL

rng (S # f) is non empty V58() countable Element of bool ExtREAL

sup (rng (S # f)) is ext-real Element of ExtREAL

M . f is ext-real Element of ExtREAL

f is set

g is set

f is Element of X

M . f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup (S # f) is ext-real Element of ExtREAL

rng (S # f) is non empty V58() countable Element of bool ExtREAL

sup (rng (S # f)) is ext-real Element of ExtREAL

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom f is Element of bool X

g is Element of X

M /. g is ext-real Element of ExtREAL

M . g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup (S # g) is ext-real Element of ExtREAL

rng (S # g) is non empty V58() countable Element of bool ExtREAL

sup (rng (S # g)) is ext-real Element of ExtREAL

f . g is ext-real Element of ExtREAL

f /. g is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

dom (S . 0) is Element of bool X

bool X is non empty set

PFuncs (X,ExtREAL) is non empty functional M21(X, ExtREAL )

M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom f is Element of bool X

dom f is set

g is Element of X

f /. g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inferior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(inferior_realsequence (S # g)) . M is ext-real Element of ExtREAL

f . g is ext-real Element of ExtREAL

g is set

E is set

g is Element of X

f . g is ext-real set

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inferior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(inferior_realsequence (S # g)) . M is ext-real Element of ExtREAL

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . f) is Element of bool X

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

M . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . g) is Element of bool X

E is Element of X

(M . f) . E is ext-real Element of ExtREAL

S # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inferior_realsequence (S # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(inferior_realsequence (S # E)) . f is ext-real Element of ExtREAL

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . LN) is Element of bool X

f . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . g) is Element of bool X

MRLN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . MRLN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . MRLN) is Element of bool X

f . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . E) is Element of bool X

g is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

g . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (g . E) is Element of bool X

MRLN is Element of X

LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

g . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (g . LN) is Element of bool X

(g . LN) . MRLN is ext-real Element of ExtREAL

S # MRLN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inferior_realsequence (S # MRLN) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(inferior_realsequence (S # MRLN)) . LN is ext-real Element of ExtREAL

M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

M . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . g) is Element of bool X

f . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . g) is Element of bool X

E is Element of X

(M . g) /. E is ext-real Element of ExtREAL

(M . g) . E is ext-real Element of ExtREAL

S # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inferior_realsequence (S # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(inferior_realsequence (S # E)) . g is ext-real Element of ExtREAL

(f . g) . E is ext-real Element of ExtREAL

(f . g) /. E is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

dom (S . 0) is Element of bool X

bool X is non empty set

PFuncs (X,ExtREAL) is non empty functional M21(X, ExtREAL )

M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom f is Element of bool X

dom f is set

g is Element of X

f /. g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

superior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(superior_realsequence (S # g)) . M is ext-real Element of ExtREAL

f . g is ext-real Element of ExtREAL

g is set

E is set

g is Element of X

f . g is ext-real set

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

superior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(superior_realsequence (S # g)) . M is ext-real Element of ExtREAL

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . f) is Element of bool X

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

M . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . g) is Element of bool X

E is Element of X

(M . f) . E is ext-real Element of ExtREAL

S # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

superior_realsequence (S # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(superior_realsequence (S # E)) . f is ext-real Element of ExtREAL

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . LN) is Element of bool X

f . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . g) is Element of bool X

MRLN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . MRLN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . MRLN) is Element of bool X

f . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . E) is Element of bool X

g is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

g . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (g . E) is Element of bool X

MRLN is Element of X

LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

g . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (g . LN) is Element of bool X

(g . LN) . MRLN is ext-real Element of ExtREAL

S # MRLN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

superior_realsequence (S # MRLN) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(superior_realsequence (S # MRLN)) . LN is ext-real Element of ExtREAL

M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

M . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . g) is Element of bool X

f . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . g) is Element of bool X

E is Element of X

(M . g) /. E is ext-real Element of ExtREAL

(M . g) . E is ext-real Element of ExtREAL

S # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

superior_realsequence (S # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(superior_realsequence (S # E)) . g is ext-real Element of ExtREAL

(f . g) . E is ext-real Element of ExtREAL

(f . g) /. E is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

dom (S . 0) is Element of bool X

bool X is non empty set

(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

f is Element of X

(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

((X,S) # f) . g is ext-real Element of ExtREAL

(X,S) . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((X,S) . g) . f is ext-real Element of ExtREAL

dom ((X,S) . g) is Element of bool X

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inferior_realsequence (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(inferior_realsequence (S # f)) . g is ext-real Element of ExtREAL

X is set

S is set

PFuncs (X,S) is non empty functional set

[:NAT,(PFuncs (X,S)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,S)):] is non empty set

M is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V30( NAT , PFuncs (X,S)) (X,S) Element of bool [:NAT,(PFuncs (X,S)):]

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

M ^\ f is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V30( NAT , PFuncs (X,S)) Element of bool [:NAT,(PFuncs (X,S)):]

PFuncs (X,S) is non empty functional M21(X,S)

[:NAT,(PFuncs (X,S)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,S)):] is non empty set

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

(M ^\ f) . E is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

[:X,S:] is Relation-like set

bool [:X,S:] is non empty set

dom ((M ^\ f) . E) is Element of bool X

bool X is non empty set

LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

(M ^\ f) . LN is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom ((M ^\ f) . LN) is Element of bool X

g is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V30( NAT , PFuncs (X,S)) Element of bool [:NAT,(PFuncs (X,S)):]

MRLN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f + MRLN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

g . (f + MRLN) is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (g . (f + MRLN)) is Element of bool X

e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f + e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

g . (f + e0) is Relation-like X -defined S -valued Function-like Element of bool [:X,S:]

dom (g . (f + e0)) is Element of bool X

g is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V30( NAT , PFuncs (X,S)) Element of bool [:NAT,(PFuncs (X,S)):]

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

(X,S) . M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

S ^\ M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

(X,(S ^\ M)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

PFuncs (X,ExtREAL) is non empty functional M21(X, ExtREAL )

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

dom (X,(S ^\ M)) is Element of bool X

bool X is non empty set

(S ^\ M) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom ((S ^\ M) . 0) is Element of bool X

f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

M + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . (M + 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . (M + 0)) is Element of bool X

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . 0) is Element of bool X

dom ((X,S) . M) is Element of bool X

g is Element of X

(S ^\ M) # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

((S ^\ M) # g) . E is ext-real Element of ExtREAL

(S ^\ M) . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((S ^\ M) . E) . g is ext-real Element of ExtREAL

M + E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . (M + E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(f . (M + E)) . g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(S # g) . (M + E) is ext-real Element of ExtREAL

(S # g) ^\ M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

((S # g) ^\ M) . E is ext-real Element of ExtREAL

(X,(S ^\ M)) . g is ext-real Element of ExtREAL

inf ((S # g) ^\ M) is ext-real Element of ExtREAL

rng ((S # g) ^\ M) is non empty V58() countable Element of bool ExtREAL

inf (rng ((S # g) ^\ M)) is ext-real Element of ExtREAL

((X,S) . M) . g is ext-real Element of ExtREAL

inferior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(inferior_realsequence (S # g)) . M is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

(X,S) . M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

S ^\ M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

(X,(S ^\ M)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

PFuncs (X,ExtREAL) is non empty functional M21(X, ExtREAL )

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

dom (X,(S ^\ M)) is Element of bool X

bool X is non empty set

(S ^\ M) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom ((S ^\ M) . 0) is Element of bool X

f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

M + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . (M + 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (f . (M + 0)) is Element of bool X

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . 0) is Element of bool X

dom ((X,S) . M) is Element of bool X

g is Element of X

(S ^\ M) # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

((S ^\ M) # g) . E is ext-real Element of ExtREAL

(S ^\ M) . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((S ^\ M) . E) . g is ext-real Element of ExtREAL

M + E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

f . (M + E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(f . (M + E)) . g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(S # g) . (M + E) is ext-real Element of ExtREAL

(S # g) ^\ M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

((S # g) ^\ M) . E is ext-real Element of ExtREAL

(X,(S ^\ M)) . g is ext-real Element of ExtREAL

sup ((S # g) ^\ M) is ext-real Element of ExtREAL

rng ((S # g) ^\ M) is non empty V58() countable Element of bool ExtREAL

sup (rng ((S # g) ^\ M)) is ext-real Element of ExtREAL

((X,S) . M) . g is ext-real Element of ExtREAL

superior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(superior_realsequence (S # g)) . M is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

dom (S . 0) is Element of bool X

bool X is non empty set

(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

M is Element of X

(X,S) # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

S # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

superior_realsequence (S # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT

((X,S) # M) . g is ext-real Element of ExtREAL

(X,S) . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((X,S) . g) . M is ext-real Element of ExtREAL

dom ((X,S) . g) is Element of bool X

(superior_realsequence (S # M)) . g is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . 0) is Element of bool X

bool X is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Element of X

M /. f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

lim_inf (S # f) is ext-real Element of ExtREAL

inferior_realsequence (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup (inferior_realsequence (S # f)) is ext-real Element of ExtREAL

rng (inferior_realsequence (S # f)) is non empty V58() countable Element of bool ExtREAL

sup (rng (inferior_realsequence (S # f))) is ext-real Element of ExtREAL

M . f is ext-real Element of ExtREAL

f is set

g is set

f is Element of X

M . f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

lim_inf (S # f) is ext-real Element of ExtREAL

inferior_realsequence (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup (inferior_realsequence (S # f)) is ext-real Element of ExtREAL

rng (inferior_realsequence (S # f)) is non empty V58() countable Element of bool ExtREAL

sup (rng (inferior_realsequence (S # f))) is ext-real Element of ExtREAL

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom f is Element of bool X

g is Element of X

M /. g is ext-real Element of ExtREAL

M . g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

lim_inf (S # g) is ext-real Element of ExtREAL

inferior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup (inferior_realsequence (S # g)) is ext-real Element of ExtREAL

rng (inferior_realsequence (S # g)) is non empty V58() countable Element of bool ExtREAL

sup (rng (inferior_realsequence (S # g))) is ext-real Element of ExtREAL

f . g is ext-real Element of ExtREAL

f /. g is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . 0) is Element of bool X

bool X is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Element of X

M /. f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

lim_sup (S # f) is ext-real Element of ExtREAL

superior_realsequence (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inf (superior_realsequence (S # f)) is ext-real Element of ExtREAL

rng (superior_realsequence (S # f)) is non empty V58() countable Element of bool ExtREAL

inf (rng (superior_realsequence (S # f))) is ext-real Element of ExtREAL

M . f is ext-real Element of ExtREAL

f is set

g is set

f is Element of X

M . f is ext-real Element of ExtREAL

S # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

lim_sup (S # f) is ext-real Element of ExtREAL

superior_realsequence (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inf (superior_realsequence (S # f)) is ext-real Element of ExtREAL

rng (superior_realsequence (S # f)) is non empty V58() countable Element of bool ExtREAL

inf (rng (superior_realsequence (S # f))) is ext-real Element of ExtREAL

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom M is Element of bool X

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom f is Element of bool X

g is Element of X

M /. g is ext-real Element of ExtREAL

M . g is ext-real Element of ExtREAL

S # g is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

lim_sup (S # g) is ext-real Element of ExtREAL

superior_realsequence (S # g) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inf (superior_realsequence (S # g)) is ext-real Element of ExtREAL

rng (superior_realsequence (S # g)) is non empty V58() countable Element of bool ExtREAL

inf (rng (superior_realsequence (S # g))) is ext-real Element of ExtREAL

f . g is ext-real Element of ExtREAL

f /. g is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

bool [:NAT,(PFuncs (X,ExtREAL)):] is non empty set

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

(X,S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

bool [:X,ExtREAL:] is non empty set

dom (X,S) is Element of bool X

bool X is non empty set

(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

(X,(X,S)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (X,(X,S)) is Element of bool X

(X,S) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom ((X,S) . 0) is Element of bool X

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . 0) is Element of bool X

M is Element of X

(X,S) . M is ext-real Element of ExtREAL

S # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

lim_inf (S # M) is ext-real Element of ExtREAL

inferior_realsequence (S # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup (inferior_realsequence (S # M)) is ext-real Element of ExtREAL

rng (inferior_realsequence (S # M)) is non empty V58() countable Element of bool ExtREAL

sup (rng (inferior_realsequence (S # M))) is ext-real Element of ExtREAL

(X,S) # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

sup ((X,S) # M) is ext-real Element of ExtREAL

rng ((X,S) # M) is non empty V58() countable Element of bool ExtREAL

sup (rng ((X,S) # M)) is ext-real Element of ExtREAL

(X,(X,S)) . M is ext-real Element of ExtREAL

M is Element of X

(X,S) . M is ext-real Element of ExtREAL

(X,(X,S)) . M is ext-real Element of ExtREAL

M is Element of X

(X,S) . M is ext-real Element of ExtREAL

S # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

inferior_realsequence (S # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [: