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
{ b1 where b1 is Element of X : for b2 being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set holds
( not g <= b2 or b1 in f . b2 ) } is set
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 . b1) where b1 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 <= b1 } is set
meet { (S . b1) where b1 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 <= b1 } is set
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 . b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT : 0 <= b1 } is set
union { (f . b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT : 0 <= b1 } is set
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 [: