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 [: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
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_sup (S # M) is ext-real Element of 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:]
inf (superior_realsequence (S # M)) is ext-real Element of ExtREAL
rng (superior_realsequence (S # M)) is non empty V58() countable Element of bool ExtREAL
inf (rng (superior_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:]
inf ((X,S) # M) is ext-real Element of ExtREAL
rng ((X,S) # M) is non empty V58() countable Element of bool ExtREAL
inf (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:]
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:]
inf (superior_realsequence (S # M)) is ext-real Element of ExtREAL
rng (superior_realsequence (S # M)) is non empty V58() countable Element of bool ExtREAL
inf (rng (superior_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:]
inf ((X,S) # M) is ext-real Element of ExtREAL
rng ((X,S) # M) is non empty V58() countable Element of bool ExtREAL
inf (rng ((X,S) # M)) is ext-real Element of ExtREAL
(X,(X,S)) . 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 Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
M is Element of 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:]
(X,S) . M is ext-real Element of ExtREAL
(X,S) . M is ext-real Element of ExtREAL
dom (X,S) is Element of bool X
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
dom (X,S) is Element of bool X
lim_sup (S # M) is ext-real Element of 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:]
inf (superior_realsequence (S # M)) is ext-real Element of ExtREAL
rng (superior_realsequence (S # M)) is non empty V58() countable Element of bool ExtREAL
inf (rng (superior_realsequence (S # 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
[: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 (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 (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 (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 Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
M is Element of 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:]
(X,S) . M is ext-real Element of ExtREAL
(X,S) . M is ext-real Element of ExtREAL
(X,S) . M is ext-real Element of ExtREAL
lim (S # M) is ext-real Element of 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
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) is Element of bool X
lim_sup (S # M) is ext-real Element of 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:]
inf (superior_realsequence (S # M)) is ext-real Element of ExtREAL
rng (superior_realsequence (S # M)) is non empty V58() countable Element of bool ExtREAL
inf (rng (superior_realsequence (S # M))) is ext-real Element of ExtREAL
dom (X,S) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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
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)
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)):]
M . 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 (M . 0) is Element of bool X
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,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):]
rng f is non empty Element of bool S
bool S is non empty set
union (rng f) is set
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
great_dom ((X,M),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom ((X,M),(R_EAL g))) is Element of bool X
LN is set
MRLN is Element of X
(X,M) . MRLN is ext-real Element of ExtREAL
M # MRLN 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 # MRLN) is non empty V58() countable Element of bool ExtREAL
e0 is ext-real set
e is set
(M # MRLN) . e is ext-real Element of 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:]
(M . G) . MRLN is ext-real Element of ExtREAL
sup (M # MRLN) is ext-real Element of ExtREAL
sup (rng (M # MRLN)) is ext-real Element of ExtREAL
dom (X,M) 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
M . e0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(M . e0) . MRLN is ext-real Element of ExtREAL
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
M . e0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(M . e0) . MRLN is ext-real Element of ExtREAL
dom (M . e0) is Element of bool X
great_dom ((M . e0),(R_EAL g)) is Element of bool X
f . e0 is Element of bool X
(dom (M . 0)) /\ (great_dom ((M . e0),(R_EAL g))) is Element of bool X
LN is set
rng f is non empty Element of bool (bool X)
bool (bool X) is non empty set
MRLN is set
dom f is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
e is set
f . 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
f . G is Element of bool X
M . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom ((M . G),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom ((M . G),(R_EAL g))) is Element of bool X
great_dom ((M . G),g) is Element of bool X
e0 is Element of X
(M . G) . e0 is ext-real Element of ExtREAL
M # e0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
(M # e0) . G is ext-real Element of ExtREAL
dom (X,M) is Element of bool X
(X,M) . e0 is ext-real Element of ExtREAL
sup (M # e0) is ext-real Element of ExtREAL
rng (M # e0) is non empty V58() countable Element of bool ExtREAL
sup (rng (M # e0)) is ext-real Element of ExtREAL
X is non empty set
bool X is non empty set
bool (bool 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
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)
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)):]
M . 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 (M . 0) is Element of bool X
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,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):]
rng f is non empty Element of bool S
bool S is non empty set
meet (rng f) is set
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
great_eq_dom ((X,M),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((X,M),(R_EAL g))) is Element of bool X
LN is set
rng f is non empty Element of bool (bool X)
bool (bool X) is non empty set
meet (rng f) is Element of bool X
f . 0 is Element of bool X
great_eq_dom ((M . 0),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((M . 0),(R_EAL g))) is Element of bool X
dom (X,M) 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 Element of bool X
MRLN is Element of X
M . e0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom ((M . e0),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((M . e0),(R_EAL g))) is Element of bool X
(M . e0) . MRLN is ext-real Element of ExtREAL
M # MRLN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
(M # MRLN) . e0 is ext-real Element of ExtREAL
e0 is ext-real set
rng (M # MRLN) is non empty V58() countable Element of bool ExtREAL
e is set
(M # MRLN) . e is ext-real Element of ExtREAL
inf (M # MRLN) is ext-real Element of ExtREAL
inf (rng (M # MRLN)) is ext-real Element of ExtREAL
(X,M) . LN is ext-real Element of ExtREAL
LN is set
MRLN is Element of X
(X,M) . MRLN is ext-real Element of ExtREAL
e0 is set
e is set
f . 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
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
M # MRLN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
inf (M # MRLN) is ext-real Element of ExtREAL
rng (M # MRLN) is non empty V58() countable Element of bool ExtREAL
inf (rng (M # MRLN)) is ext-real Element of ExtREAL
(M . G) . MRLN is ext-real Element of ExtREAL
(M # MRLN) . G is ext-real Element of ExtREAL
great_eq_dom ((M . G),(R_EAL g)) is Element of bool X
f . G is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((M . G),(R_EAL g))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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
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)
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)):]
M . 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 (M . 0) is Element of bool X
(X,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 bool X -valued S -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]
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):]
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(superior_setsequence f) . LN is Element of bool X
(X,M) . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom (((X,M) . LN),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom (((X,M) . LN),(R_EAL 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
M ^\ MRLN 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)):]
f ^\ MRLN is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(f ^\ MRLN) . G is Element of bool X
L 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 + L 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 + L) is Element of bool X
M . (LN + L) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom ((M . (LN + L)),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom ((M . (LN + L)),(R_EAL g))) is Element of bool X
(M ^\ MRLN) . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom (((M ^\ MRLN) . G),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom (((M ^\ MRLN) . G),(R_EAL g))) is Element of bool X
rng (f ^\ MRLN) is non empty Element of bool S
bool S is non empty set
union (rng (f ^\ MRLN)) is set
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
G 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)):]
G ^\ MRLN 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 ^\ MRLN) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
LN + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
G . (LN + 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((M ^\ MRLN) . 0) is Element of bool X
(X,(M ^\ MRLN)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom ((X,(M ^\ MRLN)),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom ((X,(M ^\ MRLN)),(R_EAL g))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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
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)
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)):]
M . 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 (M . 0) is Element of bool X
(X,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 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):]
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(inferior_setsequence f) . LN is Element of bool X
(X,M) . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom (((X,M) . LN),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom (((X,M) . LN),(R_EAL 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
M ^\ MRLN 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)):]
f ^\ MRLN is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(f ^\ MRLN) . G is Element of bool X
L 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 + L 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 + L) is Element of bool X
M . (LN + L) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom ((M . (LN + L)),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((M . (LN + L)),(R_EAL g))) is Element of bool X
(M ^\ MRLN) . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom (((M ^\ MRLN) . G),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom (((M ^\ MRLN) . G),(R_EAL g))) is Element of bool X
rng (f ^\ MRLN) is non empty Element of bool S
bool S is non empty set
meet (rng (f ^\ MRLN)) is set
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
G 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)):]
G ^\ MRLN 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 ^\ MRLN) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
LN + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
G . (LN + 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((M ^\ MRLN) . 0) is Element of bool X
(X,(M ^\ MRLN)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom ((X,(M ^\ MRLN)),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((X,(M ^\ MRLN)),(R_EAL g))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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 compl-closed sigma-multiplicative Element of bool (bool X)
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)):]
M . 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 (M . 0) is Element of bool X
(X,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 Element of S
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,M) . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
LN is V11() real ext-real set
R_EAL LN is ext-real Element of ExtREAL
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
MRLN is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]
e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
M . e0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
MRLN . e0 is Element of bool X
great_dom ((M . e0),(R_EAL LN)) is Element of bool X
f /\ (great_dom ((M . e0),(R_EAL LN))) is Element of bool X
dom (M . e0) is Element of bool X
rng MRLN is non empty Element of bool (bool X)
bool (bool X) is non empty set
e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
MRLN . e0 is Element of bool X
M . e0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom ((M . e0),(R_EAL LN)) is Element of bool X
f /\ (great_dom ((M . e0),(R_EAL LN))) is Element of bool X
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
MRLN . e is Element of bool X
M . e is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom ((M . e),(R_EAL LN)) is Element of bool X
f /\ (great_dom ((M . e),(R_EAL LN))) is Element of bool X
e0 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):]
superior_setsequence e0 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):]
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
(superior_setsequence e0) . E is Element of bool X
rng (superior_setsequence e0) is non empty Element of bool S
bool S is non empty set
great_dom (((X,M) . g),(R_EAL LN)) is Element of bool X
f /\ (great_dom (((X,M) . g),(R_EAL LN))) is Element of bool X
(X,M) . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((X,M) . E) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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 compl-closed sigma-multiplicative Element of bool (bool X)
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)):]
M . 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 (M . 0) is Element of bool X
(X,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 Element of S
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,M) . g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
LN is V11() real ext-real set
R_EAL LN is ext-real Element of ExtREAL
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
MRLN is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]
e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
M . e0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
MRLN . e0 is Element of bool X
great_eq_dom ((M . e0),(R_EAL LN)) is Element of bool X
f /\ (great_eq_dom ((M . e0),(R_EAL LN))) is Element of bool X
dom (M . e0) is Element of bool X
rng MRLN is non empty Element of bool (bool X)
bool (bool X) is non empty set
e0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
MRLN . e0 is Element of bool X
M . e0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom ((M . e0),(R_EAL LN)) is Element of bool X
f /\ (great_eq_dom ((M . e0),(R_EAL LN))) is Element of bool X
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
MRLN . e is Element of bool X
M . e is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom ((M . e),(R_EAL LN)) is Element of bool X
f /\ (great_eq_dom ((M . e),(R_EAL LN))) is Element of bool X
e0 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):]
inferior_setsequence e0 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):]
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
(inferior_setsequence e0) . E is Element of bool X
rng (inferior_setsequence e0) is non empty Element of bool S
bool S is non empty set
great_eq_dom (((X,M) . g),(R_EAL LN)) is Element of bool X
f /\ (great_eq_dom (((X,M) . g),(R_EAL LN))) is Element of bool X
(X,M) . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((X,M) . E) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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
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)
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)):]
M . 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 (M . 0) is Element of bool X
(X,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)):]
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,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):]
meet f is Element of bool X
rng f is non empty set
meet (rng f) is set
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
great_eq_dom ((X,M),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((X,M),(R_EAL g))) is Element of bool X
(X,M) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((X,M) . 0) is Element of bool X
rng f is non empty Element of bool S
bool S is non empty set
meet (rng f) is set
(X,(X,M)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom ((X,(X,M)),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_eq_dom ((X,(X,M)),(R_EAL g))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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
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)
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)):]
M . 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 (M . 0) is Element of bool X
(X,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)):]
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,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):]
rng f is non empty Element of bool S
bool S is non empty set
union (rng f) is set
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
great_dom ((X,M),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom ((X,M),(R_EAL g))) is Element of bool X
(X,M) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((X,M) . 0) is Element of bool X
(X,(X,M)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom ((X,(X,M)),(R_EAL g)) is Element of bool X
(dom (M . 0)) /\ (great_dom ((X,(X,M)),(R_EAL g))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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 compl-closed sigma-multiplicative Element of bool (bool X)
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)):]
M . 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 (M . 0) is Element of bool X
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is Element of S
(X,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)):]
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
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
E is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]
LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,M) . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((X,M) . LN) is Element of bool X
E . LN is Element of bool X
great_eq_dom (((X,M) . LN),(R_EAL g)) is Element of bool X
f /\ (great_eq_dom (((X,M) . LN),(R_EAL g))) is Element of bool X
rng E is non empty Element of bool (bool X)
bool (bool X) is non empty set
LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
E . LN is Element of bool X
(X,M) . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom (((X,M) . LN),(R_EAL g)) is Element of bool X
f /\ (great_eq_dom (((X,M) . LN),(R_EAL 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
E . MRLN is Element of bool X
(X,M) . MRLN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_eq_dom (((X,M) . MRLN),(R_EAL g)) is Element of bool X
f /\ (great_eq_dom (((X,M) . MRLN),(R_EAL g))) is Element of bool X
LN 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):]
rng LN is non empty Element of bool S
bool S is non empty set
[:NAT,S:] is non empty Relation-like set
bool [:NAT,S:] is non empty set
meet LN is Element of bool X
rng LN is non empty set
meet (rng LN) is set
great_eq_dom ((X,M),(R_EAL g)) is Element of bool X
f /\ (great_eq_dom ((X,M),(R_EAL g))) is Element of bool X
dom (X,M) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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 compl-closed sigma-multiplicative Element of bool (bool X)
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)):]
M . 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 (M . 0) is Element of bool X
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is Element of S
(X,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)):]
g is V11() real ext-real set
R_EAL g is ext-real Element of ExtREAL
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
E is non empty Relation-like NAT -defined bool X -valued Function-like total V30( NAT , bool X) Element of bool [:NAT,(bool X):]
LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
E . LN is Element of bool X
(X,M) . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom (((X,M) . LN),(R_EAL g)) is Element of bool X
f /\ (great_dom (((X,M) . LN),(R_EAL g))) is Element of bool X
dom ((X,M) . LN) is Element of bool X
rng E is non empty Element of bool (bool X)
bool (bool X) is non empty set
LN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
E . LN is Element of bool X
(X,M) . LN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom (((X,M) . LN),(R_EAL g)) is Element of bool X
f /\ (great_dom (((X,M) . LN),(R_EAL 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
E . MRLN is Element of bool X
(X,M) . MRLN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
great_dom (((X,M) . MRLN),(R_EAL g)) is Element of bool X
f /\ (great_dom (((X,M) . MRLN),(R_EAL g))) is Element of bool X
LN 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):]
rng LN is non empty Element of bool S
bool S is non empty set
[:NAT,S:] is non empty Relation-like set
bool [:NAT,S:] is non empty set
union (rng LN) is set
great_dom ((X,M),(R_EAL g)) is Element of bool X
f /\ (great_dom ((X,M),(R_EAL g))) is Element of bool X
dom (X,M) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool 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 compl-closed sigma-multiplicative Element of bool (bool X)
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)):]
M . 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 (M . 0) is Element of bool X
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is Element of S
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (X,M) is Element of bool X
dom (X,M) is Element of bool X
g is Element of X
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:]
(X,M) . g is ext-real Element of ExtREAL
(X,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
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 compl-closed sigma-multiplicative Element of bool (bool X)
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)):]
M . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (M . 0) 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 S
(X,M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (X,M) is Element of bool X
E is Element of X
f . E is ext-real Element of ExtREAL
M # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (M # E) is ext-real Element of ExtREAL
(X,M) . E is ext-real Element of ExtREAL
E is Element of X
M # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,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)):]
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
bool X is non empty set
f is Element of 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:]
lim (S # f) is ext-real Element of ExtREAL
g is V11() real ext-real set
M . f is ext-real Element of ExtREAL
|.(M . f).| is ext-real Element of ExtREAL
abs g is V11() real ext-real Element of REAL
X is non empty set
bool X is non empty set
bool (bool 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 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
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 PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]
f . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (f . 0) is Element of bool X
g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom g is Element of bool X
E is Element of S
M . E is ext-real Element of ExtREAL
LN is V11() real ext-real set
MRLN is V11() real ext-real set
R_EAL MRLN is ext-real Element of ExtREAL
e0 is Element of X
f # e0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
g . e0 is ext-real Element of ExtREAL
lim (f # e0) is ext-real Element of ExtREAL
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 Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . e0) - g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
|.((f . e0) - g).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom ((f . e0) - g) is Element of bool X
dom |.((f . e0) - g).| is Element of bool X
dom (f . e0) is Element of bool X
(dom (f . e0)) /\ (dom g) is Element of bool X
E /\ E is M11(X,S)
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 Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . e0) - g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
|.((f . e0) - g).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
less_dom (|.((f . e0) - g).|,(R_EAL MRLN)) is Element of bool X
E /\ (less_dom (|.((f . e0) - g).|,(R_EAL MRLN))) is Element of bool X
[:NAT,S:] is non empty Relation-like set
bool [:NAT,S:] is non empty set
e0 is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]
{ 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 a1 <= b2 or b1 in e0 . b2 ) } is 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
{ 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 e <= b2 or b1 in e0 . b2 ) } is set
e is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]
gL is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
e . gL is Element of S
M . (e . gL) is ext-real Element of ExtREAL
E \ (e . gL) is M11(X,S)
M . (E \ (e . gL)) is ext-real Element of ExtREAL
(M . E) - (M . (e . gL)) is ext-real Element of ExtREAL
K154((M . (e . gL))) is ext-real set
K153((M . E),K154((M . (e . gL)))) is ext-real set
fL is set
fL is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
{ 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 fL <= b2 or b1 in e0 . b2 ) } is set
e0 . gL is Element of S
HP is Element of X
f . fL is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . fL) - g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
|.((f . fL) - g).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
less_dom (|.((f . fL) - g).|,(R_EAL MRLN)) is Element of bool X
E /\ (less_dom (|.((f . fL) - g).|,(R_EAL MRLN))) is Element of bool X
L is V11() real ext-real Element of REAL
fL is V11() real ext-real Element of REAL
L - fL is V11() real ext-real Element of REAL
- fL is V11() real ext-real set
L + (- fL) is V11() real ext-real set
L 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 . L is Element of S
M . (e . L) is ext-real Element of ExtREAL
L is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng e is non empty Element of bool S
bool S is non empty set
union (rng e) is set
gL is set
fL is Element of X
f # fL is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (f # fL) is ext-real Element of ExtREAL
fL is V11() real ext-real set
fL is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
g . fL is ext-real Element of ExtREAL
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
ELN 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 . ELN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . ELN) - g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
|.((f . ELN) - g).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom |.((f . ELN) - g).| is Element of bool X
HP 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 # fL) . me is ext-real Element of ExtREAL
((f # fL) . me) - (lim (f # fL)) is ext-real Element of ExtREAL
K154((lim (f # fL))) is ext-real set
K153(((f # fL) . me),K154((lim (f # fL)))) is ext-real set
|.(((f # fL) . me) - (lim (f # fL))).| is ext-real Element of ExtREAL
f . me is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . me) . fL is ext-real Element of ExtREAL
((f . me) . fL) - (g . fL) is ext-real Element of ExtREAL
K154((g . fL)) is ext-real set
K153(((f . me) . fL),K154((g . fL))) is ext-real set
|.(((f . me) . fL) - (g . fL)).| is ext-real Element of ExtREAL
dom ((f . ELN) - g) is Element of bool X
(f . me) - g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
((f . me) - g) . fL is ext-real Element of ExtREAL
|.(((f . me) - g) . fL).| is ext-real Element of ExtREAL
|.((f . me) - g).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
|.((f . me) - g).| . fL is ext-real Element of ExtREAL
less_dom (|.((f . me) - g).|,(R_EAL MRLN)) is Element of bool X
E /\ (less_dom (|.((f . me) - g).|,(R_EAL MRLN))) is Element of bool X
e0 . ELN is Element of S
e0 . me is Element of S
{ 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 HP <= b2 or b1 in e0 . b2 ) } is set
e . HP is Element of S
M * e is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
dom (M * e) is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
gL is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
fL 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 . gL is Element of S
e . fL is Element of S
M . (e . gL) is ext-real Element of ExtREAL
M . (e . fL) is ext-real Element of ExtREAL
fL is 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 gL <= b2 or b1 in e0 . b2 ) } is set
HP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
e0 . HP is Element of S
me is Element of X
{ 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 fL <= b2 or b1 in e0 . b2 ) } is set
HP is Element of X
G is V11() real ext-real Element of REAL
NAT --> G is non empty T-Sequence-like Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
fL is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(NAT --> G) . fL is V11() real ext-real Element of REAL
fL is set
(M * e) . fL is ext-real Element of ExtREAL
fL 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 . fL is Element of S
M . (e . fL) is ext-real Element of ExtREAL
L . fL is V11() real ext-real Element of REAL
dom L is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
fL is set
fL is set
e . fL is set
HP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
e . HP is Element of S
lim L is V11() real ext-real Element of REAL
fL 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 . fL is Element of S
fL + 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
e . (fL + 1) is Element of S
fL 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 . fL is Element of S
M . (e . fL) is ext-real Element of ExtREAL
L . fL is V11() real ext-real Element of REAL
fL is V11() real ext-real Element of REAL
fL + 1 is V11() real ext-real Element of REAL
fL + 0 is V11() real ext-real Element of REAL
fL is V11() real ext-real set
rng L is non empty V57() V58() V59() Element of bool REAL
HP is ext-real set
me is set
L . me is V11() real ext-real Element of REAL
rng (M * e) is non empty V58() countable Element of bool ExtREAL
sup (rng (M * e)) is ext-real Element of ExtREAL
upper_bound (rng L) is V11() real ext-real Element of REAL
HP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
L . me is V11() real ext-real Element of REAL
e . me is Element of S
M . (e . me) is ext-real Element of ExtREAL
L . HP is V11() real ext-real Element of REAL
e . HP is Element of S
M . (e . HP) is ext-real Element of ExtREAL
upper_bound L is V11() real ext-real Element of REAL
fL 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 . fL is Element of S
E \ (e . fL) is M11(X,S)
M . (E \ (e . fL)) is ext-real Element of ExtREAL
fL is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
fL is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
fL . fL is V11() real ext-real Element of REAL
e . fL is Element of S
E \ (e . fL) is M11(X,S)
M . (E \ (e . fL)) is ext-real Element of ExtREAL
M . (e . fL) is ext-real Element of ExtREAL
(M . E) - (M . (e . fL)) is ext-real Element of ExtREAL
K154((M . (e . fL))) is ext-real set
K153((M . E),K154((M . (e . fL)))) is ext-real set
L . fL is V11() real ext-real Element of REAL
G - (L . fL) is V11() real ext-real Element of REAL
- (L . fL) is V11() real ext-real set
G + (- (L . fL)) is V11() real ext-real set
(NAT --> G) . fL is V11() real ext-real Element of REAL
((NAT --> G) . fL) - (L . fL) is V11() real ext-real Element of REAL
((NAT --> G) . fL) + (- (L . fL)) is V11() real ext-real set
- L is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- 1 is V11() real ext-real non positive set
(- 1) (#) L is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- L) . fL is V11() real ext-real Element of REAL
((NAT --> G) . fL) + ((- L) . fL) is V11() real ext-real Element of REAL
(NAT --> G) - L is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- L is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(NAT --> G) + (- L) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(NAT --> G) . 0 is V11() real ext-real Element of REAL
lim fL is V11() real ext-real Element of REAL
lim (NAT --> G) is V11() real ext-real Element of REAL
(lim (NAT --> G)) - (lim L) is V11() real ext-real Element of REAL
- (lim L) is V11() real ext-real set
(lim (NAT --> G)) + (- (lim L)) is V11() real ext-real set
G - G is V11() real ext-real Element of REAL
- G is V11() real ext-real set
G + (- G) is V11() real ext-real set
fL 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 . fL is Element of S
E \ (e . fL) is M11(X,S)
HP is Element of S
E \ HP is M11(X,S)
E /\ (e . fL) is M11(X,S)
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f . me is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
RELN is Element of X
(f . me) . RELN is ext-real Element of ExtREAL
g . RELN is ext-real Element of ExtREAL
((f . me) . RELN) - (g . RELN) is ext-real Element of ExtREAL
K154((g . RELN)) is ext-real set
K153(((f . me) . RELN),K154((g . RELN))) is ext-real set
|.(((f . me) . RELN) - (g . RELN)).| is ext-real Element of ExtREAL
{ 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 fL <= b2 or b1 in e0 . b2 ) } is set
e0 . me is Element of S
MRHP is Element of X
ELN 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 . ELN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . ELN) - g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
|.((f . ELN) - g).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
less_dom (|.((f . ELN) - g).|,(R_EAL MRLN)) is Element of bool X
E /\ (less_dom (|.((f . ELN) - g).|,(R_EAL MRLN))) is Element of bool X
(f . me) - g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
|.((f . me) - g).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
less_dom (|.((f . me) - g).|,(R_EAL MRLN)) is Element of bool X
|.((f . me) - g).| . RELN is ext-real Element of ExtREAL
dom ((f . ELN) - g) is Element of bool X
dom |.((f . ELN) - g).| is Element of bool X
((f . me) - g) . RELN is ext-real Element of ExtREAL
|.(((f . me) - g) . RELN).| is ext-real Element of ExtREAL
M . HP is ext-real Element of ExtREAL
M . (E \ (e . fL)) is ext-real Element of ExtREAL
fL . fL is V11() real ext-real Element of REAL
(fL . fL) - 0 is V11() real ext-real Element of REAL
- 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() set
(fL . fL) + (- 0) is V11() real ext-real set
abs ((fL . fL) - 0) is V11() real ext-real Element of REAL
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
ELN is Element of X
f . me is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . me) . ELN is ext-real Element of ExtREAL
g . ELN is ext-real Element of ExtREAL
((f . me) . ELN) - (g . ELN) is ext-real Element of ExtREAL
K154((g . ELN)) is ext-real set
K153(((f . me) . ELN),K154((g . ELN))) is ext-real set
|.(((f . me) . ELN) - (g . ELN)).| is ext-real Element of ExtREAL
X is non empty set
S is non empty set
[:X,S:] is non empty Relation-like set
bool [:X,S:] is non empty set
M is set
g is non empty Relation-like X -defined S -valued Function-like total V30(X,S) Element of bool [:X,S:]
f is non empty Relation-like X -defined S -valued Function-like total V30(X,S) Element of bool [:X,S:]
rng g is non empty Element of bool S
bool S is non empty set
union (rng g) is set
rng f is non empty Element of bool S
meet (rng f) is set
M \ (meet (rng f)) is Element of bool M
bool M is non empty set
dom g is non empty Element of bool X
bool X is non empty set
E is set
{M} is non empty set
DIFFERENCE ({M},(rng f)) is set
LN is set
MRLN is set
LN \ MRLN is Element of bool LN
bool LN is non empty set
dom f is non empty Element of bool X
e0 is set
f . e0 is set
e is Element of X
g . e is Element of S
E is set
LN is set
g . LN is set
MRLN is Element of X
f . MRLN is Element of S
M \ (f . MRLN) is Element of bool M
X is non empty set
bool X is non empty set
bool (bool 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 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
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 PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) (X, ExtREAL ) Element of bool [:NAT,(PFuncs (X,ExtREAL)):]
f . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (f . 0) is Element of bool X
g is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom g is Element of bool X
E is Element of S
M . E is ext-real Element of 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:]
[:NAT,S:] is non empty Relation-like set
bool [:NAT,S:] is non empty set
LN is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]
rng LN is non empty Element of bool S
bool S is non empty set
meet (rng LN) is set
e0 is V11() real ext-real set
2 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
e0 / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
e0 * (2 ") is V11() real ext-real set
G is Element of S
E \ G is M11(X,S)
M . (E \ G) is ext-real Element of ExtREAL
G is Element of S
E \ G is M11(X,S)
M . (E \ G) is ext-real Element of ExtREAL
MRLN is Element of S
MRLN /\ G is M11(X,S)
(meet (rng LN)) /\ G is Element of bool X
L is Element of S
g | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
M . L is ext-real Element of ExtREAL
dom (g | L) is Element of bool X
(dom g) /\ L is Element of bool X
fL 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)):]
fL is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
fL . fL is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (fL . fL) is Element of bool X
HP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
fL . HP is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (fL . HP) is Element of bool X
f . HP is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . HP) | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (f . HP) is Element of bool X
(dom (f . HP)) /\ L is Element of bool X
f . fL is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . fL) | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (f . fL) is Element of bool X
(dom (f . fL)) /\ L is Element of bool X
fL 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)):]
HP is Element of X
fL # HP is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
(g | L) . HP is ext-real Element of ExtREAL
lim (fL # HP) is ext-real Element of ExtREAL
dom (fL # HP) is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
f # HP is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
dom (f # HP) is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
me is set
(fL # HP) . me is ext-real Element of ExtREAL
(f # HP) . me is ext-real Element of ExtREAL
ELN 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 . ELN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . ELN) | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
((f . ELN) | L) . HP is ext-real Element of ExtREAL
(f . ELN) . HP is ext-real Element of ExtREAL
fL . ELN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(fL . ELN) . HP is ext-real Element of ExtREAL
(f # HP) . ELN is ext-real Element of ExtREAL
g . HP is ext-real Element of ExtREAL
lim (f # HP) is ext-real Element of ExtREAL
1 / 2 is V11() real ext-real non negative Element of REAL
1 * (2 ") is V11() real ext-real non negative set
(1 / 2) GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(e0 / 2) (#) ((1 / 2) GeoSeq) is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
HP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
fL . HP is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (fL . HP) is Element of bool X
f . HP is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . HP) | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (f . HP) is Element of bool X
(dom (f . HP)) /\ L is Element of bool X
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
fL . me is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (fL . me) is Element of bool X
E /\ L is M11(X,S)
ELN is Element of X
(fL . HP) . ELN is ext-real Element of ExtREAL
|.((fL . HP) . ELN).| is ext-real Element of ExtREAL
dom LN is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
LN . me is Element of S
LN . HP is Element of S
f . me is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . me) . ELN is ext-real Element of ExtREAL
|.((f . me) . ELN).| is ext-real Element of ExtREAL
fL . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (fL . 0) is Element of bool X
HP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
((e0 / 2) (#) ((1 / 2) GeoSeq)) . HP is V11() real ext-real Element of REAL
((1 / 2) GeoSeq) . HP is V11() real ext-real Element of REAL
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
((1 / 2) GeoSeq) . me is V11() real ext-real Element of REAL
(e0 / 2) * (((1 / 2) GeoSeq) . me) is V11() real ext-real Element of REAL
(1 / 2) |^ HP is V11() real ext-real Element of REAL
HP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
((e0 / 2) (#) ((1 / 2) GeoSeq)) . HP is V11() real ext-real Element of REAL
((1 / 2) GeoSeq) . HP is V11() real ext-real Element of REAL
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
((e0 / 2) (#) ((1 / 2) GeoSeq)) . me is V11() real ext-real Element of REAL
((1 / 2) GeoSeq) . me is V11() real ext-real Element of REAL
ELN is Element of S
M . ELN is ext-real Element of ExtREAL
RELN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
L \ ELN is M11(X,S)
MRHP 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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
MRHP is Element of X
fL . F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(fL . F) . MRHP is ext-real Element of ExtREAL
(g | L) . MRHP is ext-real Element of ExtREAL
((fL . F) . MRHP) - ((g | L) . MRHP) is ext-real Element of ExtREAL
K154(((g | L) . MRHP)) is ext-real set
K153(((fL . F) . MRHP),K154(((g | L) . MRHP))) is ext-real set
|.(((fL . F) . MRHP) - ((g | L) . MRHP)).| is ext-real Element of ExtREAL
HP is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]
me is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
HP . me is Element of S
M . (HP . me) is ext-real Element of ExtREAL
((e0 / 2) (#) ((1 / 2) GeoSeq)) . me is V11() real ext-real Element of REAL
me is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
ELN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
me . ELN is V11() real ext-real Element of REAL
((e0 / 2) (#) ((1 / 2) GeoSeq)) . ELN is V11() real ext-real Element of REAL
HP . ELN is Element of S
M . (HP . ELN) is ext-real Element of ExtREAL
ELN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
me . ELN is V11() real ext-real Element of REAL
((e0 / 2) (#) ((1 / 2) GeoSeq)) . ELN is V11() real ext-real Element of REAL
HP . ELN is Element of S
M . (HP . ELN) is ext-real Element of ExtREAL
ELN is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of bool [:NAT,S:]
rng ELN is non empty Element of bool S
rng HP is non empty Element of bool S
union (rng HP) is set
E /\ (union (rng HP)) is Element of bool X
RELN is non empty countable N_Measure_fam of S
MRHP is set
F is set
ELN . F is set
MRHP is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
ELN . MRHP is Element of S
M . (ELN . MRHP) is ext-real Element of ExtREAL
LN . MRHP is Element of S
E \ (LN . MRHP) is M11(X,S)
M . (E \ (LN . MRHP)) is ext-real Element of ExtREAL
union RELN is Element of S
M . (union RELN) is ext-real Element of ExtREAL
MRHP is set
E \ (meet (rng LN)) is Element of bool X
F is set
dom LN is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
MRHP is set
LN . MRHP is set
dom ELN is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
ELN . q is Element of S
LN . q is Element of S
E \ (LN . q) is M11(X,S)
MRHP is set
F is set
MRHP is set
ELN . MRHP is set
q 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 . q is Element of S
E \ (LN . q) is M11(X,S)
MRHP is Element of S
L \ MRHP is M11(X,S)
L \ (union (rng HP)) is Element of bool X
F is Element of S
E \ L is M11(X,S)
(E \ (meet (rng LN))) \/ (E \ G) is Element of bool X
M . (E \ L) is ext-real Element of ExtREAL
(M . (union RELN)) + (M . (E \ G)) is ext-real Element of ExtREAL
MRHP is Element of S
(E \ L) \/ MRHP is M11(X,S)
M . ((E \ L) \/ MRHP) is ext-real Element of ExtREAL
M . MRHP is ext-real Element of ExtREAL
(M . (E \ L)) + (M . MRHP) is ext-real Element of ExtREAL
E \ F is M11(X,S)
(E \ L) \/ (E /\ (union (rng HP))) is Element of bool X
M . (E \ F) is ext-real Element of ExtREAL
dom me is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
M * HP is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
dom (M * HP) is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
q is set
me . q is V11() real ext-real Element of REAL
(M * HP) . q is ext-real Element of ExtREAL
HP . q is set
M . (HP . q) is ext-real Element of ExtREAL
abs (1 / 2) is V11() real ext-real Element of REAL
Sum me is V11() real ext-real Element of REAL
SUM (M * HP) is ext-real Element of ExtREAL
M . (union (rng HP)) is ext-real Element of ExtREAL
q is V11() real ext-real set
lim ((1 / 2) GeoSeq) is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
((1 / 2) GeoSeq) . p is V11() real ext-real Element of REAL
(1 / 2) |^ p is V11() real ext-real Element of REAL
(((1 / 2) GeoSeq) . p) - 0 is V11() real ext-real Element of REAL
- 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() set
(((1 / 2) GeoSeq) . p) + (- 0) is V11() real ext-real set
abs ((((1 / 2) GeoSeq) . p) - 0) is V11() real ext-real Element of REAL
q is Element of X
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
HP . p is Element of S
L \ (HP . p) is M11(X,S)
dom HP is non empty V57() V58() V59() V60() V61() V62() Element of bool NAT
q is V11() real ext-real set
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
((1 / 2) GeoSeq) . p is V11() real ext-real Element of REAL
HP . p is Element of S
L \ (HP . p) is M11(X,S)
Np is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
fL . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(f . n) | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
x is Element of X
n9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V44() V46() V57() V58() V59() V60() V61() V62() Element of NAT
fL . n9 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(fL . n9) . x is ext-real Element of ExtREAL
(g | L) . x is ext-real Element of ExtREAL
((fL . n9) . x) - ((g | L) . x) is ext-real Element of ExtREAL
K154(((g | L) . x)) is ext-real set
K153(((fL . n9) . x),K154(((g | L) . x))) is ext-real set
|.(((fL . n9) . x) - ((g | L) . x)).| is ext-real Element of ExtREAL
(fL . n) . x is ext-real Element of ExtREAL
((fL . n) . x) - ((g | L) . x) is ext-real Element of ExtREAL
K153(((fL . n) . x),K154(((g | L) . x))) is ext-real set
|.(((fL . n) . x) - ((g | L) . x)).| is ext-real Element of ExtREAL
g . x is ext-real Element of ExtREAL
(f . n) . x is ext-real Element of ExtREAL
((f . n) . x) - (g . x) is ext-real Element of ExtREAL
K154((g . x)) is ext-real set
K153(((f . n) . x),K154((g . x))) is ext-real set
|.(((f . n) . x) - (g . x)).| is ext-real Element of ExtREAL
Sum ((1 / 2) GeoSeq) is V11() real ext-real Element of REAL
1 - (1 / 2) is V11() real ext-real Element of REAL
- (1 / 2) is V11() real ext-real non positive set
1 + (- (1 / 2)) is V11() real ext-real set
1 / (1 - (1 / 2)) is V11() real ext-real Element of REAL
(1 - (1 / 2)) " is V11() real ext-real set
1 * ((1 - (1 / 2)) ") is V11() real ext-real set
Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) is V11() real ext-real Element of REAL
(e0 / 2) * 2 is V11() real ext-real Element of REAL
2 * (e0 / 2) is V11() real ext-real Element of REAL