:: MEASURE7 semantic presentation

REAL is non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval set
NAT is non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V57() interval set
[:NAT,ExtREAL:] is Relation-like non empty V68() set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below set
bool omega is non empty set
[:NAT,REAL:] is Relation-like non empty V67() V68() V69() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
RAT is non empty V34() V56() V57() V58() V59() V62() set
INT is non empty V34() V56() V57() V58() V59() V60() V62() set
0. is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval Element of ExtREAL
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real left_end bounded_below Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval Element of NAT
+infty is ext-real non real Element of ExtREAL
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval set
diameter {} is ext-real Element of ExtREAL
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty V67() V68() V69() V70() set
[:NAT,[:NAT,NAT:]:] is Relation-like non empty set
bool [:NAT,[:NAT,NAT:]:] is non empty set
+infty is non real set
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM G0 is ext-real Element of ExtREAL
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
D is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . D is ext-real Element of ExtREAL
D + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . (D + 1) is ext-real Element of ExtREAL
G0 . (D + 1) is ext-real Element of ExtREAL
0. + (G0 . (D + 1)) is ext-real Element of ExtREAL
(Ser G0) . 0 is ext-real Element of ExtREAL
G0 . 0 is ext-real Element of ExtREAL
rng (Ser G0) is non empty V48() V57() Element of bool ExtREAL
{0.} is functional non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool ExtREAL
D is set
dom (Ser G0) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
bool NAT is non empty set
G is set
(Ser G0) . G is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . G is ext-real Element of ExtREAL
D is set
dom (Ser G0) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
bool NAT is non empty set
sup {0.} is ext-real Element of ExtREAL
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
D is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G0 . D is ext-real Element of ExtREAL
(Ser G0) . D is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real real set
G + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . G is ext-real Element of ExtREAL
((Ser G0) . G) + (G0 . D) is ext-real Element of ExtREAL
0. + (G0 . D) is ext-real Element of ExtREAL
D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . G is ext-real Element of ExtREAL
(Ser D) . G is ext-real Element of ExtREAL
(Ser G) . G is ext-real Element of ExtREAL
((Ser D) . G) + ((Ser G) . G) is ext-real Element of ExtREAL
G + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . (G + 1) is ext-real Element of ExtREAL
(Ser D) . (G + 1) is ext-real Element of ExtREAL
(Ser G) . (G + 1) is ext-real Element of ExtREAL
((Ser D) . (G + 1)) + ((Ser G) . (G + 1)) is ext-real Element of ExtREAL
D . (G + 1) is ext-real Element of ExtREAL
((Ser D) . G) + (D . (G + 1)) is ext-real Element of ExtREAL
G . (G + 1) is ext-real Element of ExtREAL
((Ser G) . G) + (G . (G + 1)) is ext-real Element of ExtREAL
G0 . (G + 1) is ext-real Element of ExtREAL
(D . (G + 1)) + (G . (G + 1)) is ext-real Element of ExtREAL
0. + 0. is V30() ext-real real Element of ExtREAL
K139(0.,0.) is V30() ext-real real set
(((Ser D) . G) + ((Ser G) . G)) + (G0 . (G + 1)) is ext-real Element of ExtREAL
((Ser D) . G) + (G0 . (G + 1)) is ext-real Element of ExtREAL
(((Ser D) . G) + (G0 . (G + 1))) + ((Ser G) . G) is ext-real Element of ExtREAL
(((Ser D) . G) + (D . (G + 1))) + (G . (G + 1)) is ext-real Element of ExtREAL
((((Ser D) . G) + (D . (G + 1))) + (G . (G + 1))) + ((Ser G) . G) is ext-real Element of ExtREAL
(Ser G) . 0 is ext-real Element of ExtREAL
G . 0 is ext-real Element of ExtREAL
(Ser G0) . 0 is ext-real Element of ExtREAL
G0 . 0 is ext-real Element of ExtREAL
(Ser D) . 0 is ext-real Element of ExtREAL
D . 0 is ext-real Element of ExtREAL
((Ser D) . 0) + ((Ser G) . 0) is ext-real Element of ExtREAL
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM G0 is ext-real Element of ExtREAL
SUM D is ext-real Element of ExtREAL
SUM G is ext-real Element of ExtREAL
(SUM D) + (SUM G) is ext-real Element of ExtREAL
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . G is ext-real Element of ExtREAL
(Ser D) . G is ext-real Element of ExtREAL
(Ser G) . G is ext-real Element of ExtREAL
((Ser D) . G) + ((Ser G) . G) is ext-real Element of ExtREAL
G + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . (G + 1) is ext-real Element of ExtREAL
(Ser D) . (G + 1) is ext-real Element of ExtREAL
(Ser G) . (G + 1) is ext-real Element of ExtREAL
((Ser D) . (G + 1)) + ((Ser G) . (G + 1)) is ext-real Element of ExtREAL
D . (G + 1) is ext-real Element of ExtREAL
((Ser D) . G) + (D . (G + 1)) is ext-real Element of ExtREAL
G . (G + 1) is ext-real Element of ExtREAL
((Ser G) . G) + (G . (G + 1)) is ext-real Element of ExtREAL
0. + 0. is V30() ext-real real Element of ExtREAL
K139(0.,0.) is V30() ext-real real set
(D . (G + 1)) + (G . (G + 1)) is ext-real Element of ExtREAL
G0 . (G + 1) is ext-real Element of ExtREAL
((Ser G0) . G) + (G0 . (G + 1)) is ext-real Element of ExtREAL
((Ser G) . G) + (G0 . (G + 1)) is ext-real Element of ExtREAL
((Ser D) . G) + (((Ser G) . G) + (G0 . (G + 1))) is ext-real Element of ExtREAL
((Ser G) . G) + ((D . (G + 1)) + (G . (G + 1))) is ext-real Element of ExtREAL
((Ser D) . G) + (((Ser G) . G) + ((D . (G + 1)) + (G . (G + 1)))) is ext-real Element of ExtREAL
(((Ser G) . G) + (G . (G + 1))) + (D . (G + 1)) is ext-real Element of ExtREAL
((Ser D) . G) + ((((Ser G) . G) + (G . (G + 1))) + (D . (G + 1))) is ext-real Element of ExtREAL
(Ser G) . 0 is ext-real Element of ExtREAL
G . 0 is ext-real Element of ExtREAL
(Ser G0) . 0 is ext-real Element of ExtREAL
G0 . 0 is ext-real Element of ExtREAL
(Ser D) . 0 is ext-real Element of ExtREAL
D . 0 is ext-real Element of ExtREAL
((Ser D) . 0) + ((Ser G) . 0) is ext-real Element of ExtREAL
rng (Ser G0) is non empty V48() V57() Element of bool ExtREAL
G is ext-real set
dom (Ser G0) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
bool NAT is non empty set
A is set
(Ser G0) . A is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G) . B is ext-real Element of ExtREAL
rng (Ser G) is non empty V48() V57() Element of bool ExtREAL
sup (rng (Ser G)) is ext-real Element of ExtREAL
(Ser D) . B is ext-real Element of ExtREAL
rng (Ser D) is non empty V48() V57() Element of bool ExtREAL
sup (rng (Ser D)) is ext-real Element of ExtREAL
((Ser D) . B) + ((Ser G) . B) is ext-real Element of ExtREAL
sup (rng (Ser G0)) is ext-real Element of ExtREAL
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM D is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . G is ext-real Element of ExtREAL
Ser D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser D) . G is ext-real Element of ExtREAL
dom (Ser D) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
bool NAT is non empty set
rng (Ser D) is non empty V48() V57() Element of bool ExtREAL
sup (rng (Ser D)) is ext-real Element of ExtREAL
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM G0 is ext-real Element of ExtREAL
D is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G0 . D is ext-real Element of ExtREAL
D is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . D is ext-real Element of ExtREAL
G0 is non empty set
[:G0,ExtREAL:] is Relation-like non empty V68() set
bool [:G0,ExtREAL:] is non empty set
D is Relation-like G0 -defined ExtREAL -valued Function-like non empty V14(G0) quasi_total V68() Element of bool [:G0,ExtREAL:]
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . G is ext-real Element of ExtREAL
G is Element of G0
D . G is ext-real Element of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . G is ext-real Element of ExtREAL
D . G is ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . A is ext-real Element of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
A is set
G . A is ext-real Element of ExtREAL
G . A is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . B is ext-real Element of ExtREAL
D . B is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . B is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G0 is non empty set
[:G0,ExtREAL:] is Relation-like non empty V68() set
bool [:G0,ExtREAL:] is non empty set
D is Relation-like G0 -defined ExtREAL -valued Function-like non empty V14(G0) quasi_total V68() Element of bool [:G0,ExtREAL:]
(G0,D) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(G0,D) . G is ext-real Element of ExtREAL
D . G is ext-real Element of ExtREAL
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
D is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . D is ext-real Element of ExtREAL
(Ser G0) . G is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D + G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . (D + G) is ext-real Element of ExtREAL
G + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D + (G + 1) is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . (D + (G + 1)) is ext-real Element of ExtREAL
(D + G) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . ((D + G) + 1) is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real real set
D + G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D + A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D + 0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . (D + 0) is ext-real Element of ExtREAL
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
D . G0 is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser D) . G is ext-real Element of ExtREAL
G + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser D) . (G + 1) is ext-real Element of ExtREAL
D . (G + 1) is ext-real Element of ExtREAL
((Ser D) . G) + (D . (G + 1)) is ext-real Element of ExtREAL
(Ser D) . 0 is ext-real Element of ExtREAL
D . 0 is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser D) . G is ext-real Element of ExtREAL
G + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser D) . (G + 1) is ext-real Element of ExtREAL
D . (G + 1) is ext-real Element of ExtREAL
((Ser D) . G) + (D . (G + 1)) is ext-real Element of ExtREAL
D . (G + 1) is ext-real Element of ExtREAL
((Ser D) . G) + (D . (G + 1)) is ext-real Element of ExtREAL
D . 0 is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser D) . G is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser D) . G is ext-real Element of ExtREAL
bool NAT is non empty set
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM G0 is ext-real Element of ExtREAL
D is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
[:D,NAT:] is Relation-like RAT -valued INT -valued non empty V67() V68() V69() V70() set
bool [:D,NAT:] is non empty set
G is Relation-like D -defined NAT -valued Function-like non empty V14(D) quasi_total V67() V68() V69() V70() Element of bool [:D,NAT:]
G0 * G is Relation-like D -defined ExtREAL -valued Function-like non empty V14(D) quasi_total V68() Element of bool [:D,ExtREAL:]
[:D,ExtREAL:] is Relation-like non empty V68() set
bool [:D,ExtREAL:] is non empty set
(D,(G0 * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (D,(G0 * G)) is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . (G + 1) is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
A + B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
n * G is Relation-like D -defined ExtREAL -valued Function-like non empty V14(D) quasi_total V68() Element of bool [:D,ExtREAL:]
(D,(n * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser (D,(n * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (D,(n * G))) . (G + 1) is ext-real Element of ExtREAL
Ser n is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser n) . (A + B) is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . n is ext-real Element of ExtREAL
n is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
n * G is Relation-like D -defined ExtREAL -valued Function-like non empty V14(D) quasi_total V68() Element of bool [:D,ExtREAL:]
(D,(n * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
eps is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
eps . eps is ext-real Element of ExtREAL
(n * G) . eps is ext-real Element of ExtREAL
G . eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . (G . eps) is ext-real Element of ExtREAL
E is epsilon-transitive epsilon-connected ordinal natural V30() ext-real real Element of D
G . E is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . eps is ext-real Element of ExtREAL
n . eps is ext-real Element of ExtREAL
E is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . E is ext-real Element of ExtREAL
E is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
E * G is Relation-like D -defined ExtREAL -valued Function-like non empty V14(D) quasi_total V68() Element of bool [:D,ExtREAL:]
(D,(E * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(D,(E * G)) . (G + 1) is ext-real Element of ExtREAL
eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real real Element of D
(E * G) . eps is ext-real Element of ExtREAL
G . eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
E . (G . eps) is ext-real Element of ExtREAL
eps . eps is ext-real Element of ExtREAL
(n * G) . eps is ext-real Element of ExtREAL
n . (G . eps) is ext-real Element of ExtREAL
n . (G . eps) is ext-real Element of ExtREAL
Ser eps is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser eps) . (G + 1) is ext-real Element of ExtREAL
n . (G . (G + 1)) is ext-real Element of ExtREAL
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,(E * G)) . FF is ext-real Element of ExtREAL
G . FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . (G . FF) is ext-real Element of ExtREAL
(E * G) . FF is ext-real Element of ExtREAL
E . (G . FF) is ext-real Element of ExtREAL
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real real Element of D
G . G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,(n * G)) . FF is ext-real Element of ExtREAL
eps . FF is ext-real Element of ExtREAL
(D,(E * G)) . FF is ext-real Element of ExtREAL
(eps . FF) + ((D,(E * G)) . FF) is ext-real Element of ExtREAL
(n * G) . FF is ext-real Element of ExtREAL
G . FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . (G . FF) is ext-real Element of ExtREAL
G . FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . (G . FF) is ext-real Element of ExtREAL
(n * G) . FF is ext-real Element of ExtREAL
Ser n is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser n) . (A + B) is ext-real Element of ExtREAL
n . (G . (G + 1)) is ext-real Element of ExtREAL
Ser (D,(E * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (D,(E * G))) . (G + 1) is ext-real Element of ExtREAL
(Ser (D,(E * G))) . G is ext-real Element of ExtREAL
((Ser (D,(E * G))) . G) + ((D,(E * G)) . (G + 1)) is ext-real Element of ExtREAL
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
E . G0 is ext-real Element of ExtREAL
n . G0 is ext-real Element of ExtREAL
((Ser eps) . (G + 1)) + ((Ser (D,(E * G))) . (G + 1)) is ext-real Element of ExtREAL
Ser E is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser E) . A is ext-real Element of ExtREAL
(Ser E) . (A + B) is ext-real Element of ExtREAL
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . G0 is ext-real Element of ExtREAL
n . G0 is ext-real Element of ExtREAL
E . G0 is ext-real Element of ExtREAL
(n . G0) + (E . G0) is ext-real Element of ExtREAL
((Ser n) . (A + B)) + ((Ser E) . (A + B)) is ext-real Element of ExtREAL
B is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
B * G is Relation-like D -defined ExtREAL -valued Function-like non empty V14(D) quasi_total V68() Element of bool [:D,ExtREAL:]
(D,(B * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser (D,(B * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (D,(B * G))) . (G + 1) is ext-real Element of ExtREAL
Ser B is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser B) . A is ext-real Element of ExtREAL
(D,(B * G)) . (G + 1) is ext-real Element of ExtREAL
(Ser (D,(B * G))) . G is ext-real Element of ExtREAL
((Ser (D,(B * G))) . G) + ((D,(B * G)) . (G + 1)) is ext-real Element of ExtREAL
G . 0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
A is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
A * G is Relation-like D -defined ExtREAL -valued Function-like non empty V14(D) quasi_total V68() Element of bool [:D,ExtREAL:]
(D,(A * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser (D,(A * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (D,(A * G))) . 0 is ext-real Element of ExtREAL
Ser A is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser A) . G is ext-real Element of ExtREAL
(D,(A * G)) . 0 is ext-real Element of ExtREAL
(A * G) . 0 is ext-real Element of ExtREAL
A . (G . 0) is ext-real Element of ExtREAL
G is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval Element of NAT
A is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
A * G is Relation-like D -defined ExtREAL -valued Function-like non empty V14(D) quasi_total V68() Element of bool [:D,ExtREAL:]
(D,(A * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser (D,(A * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (D,(A * G))) . 0 is ext-real Element of ExtREAL
Ser A is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser A) . G is ext-real Element of ExtREAL
A . 0 is ext-real Element of ExtREAL
(D,(A * G)) . 0 is ext-real Element of ExtREAL
Ser (D,(G0 * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
rng (Ser (D,(G0 * G))) is non empty V48() V57() Element of bool ExtREAL
Ser G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
rng (Ser G0) is non empty V48() V57() Element of bool ExtREAL
G is ext-real set
dom (Ser (D,(G0 * G))) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
A is set
(Ser (D,(G0 * G))) . A is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser G0) . F is ext-real Element of ExtREAL
dom (Ser G0) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
A is ext-real set
sup (rng (Ser (D,(G0 * G)))) is ext-real Element of ExtREAL
sup (rng (Ser G0)) is ext-real Element of ExtREAL
D is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM G0 is ext-real Element of ExtREAL
SUM D is ext-real Element of ExtREAL
G is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
[:G,NAT:] is Relation-like RAT -valued INT -valued non empty V67() V68() V69() V70() set
bool [:G,NAT:] is non empty set
G is Relation-like G -defined NAT -valued Function-like non empty V14(G) quasi_total V67() V68() V69() V70() Element of bool [:G,NAT:]
D * G is Relation-like G -defined ExtREAL -valued Function-like non empty V14(G) quasi_total V68() Element of bool [:G,ExtREAL:]
[:G,ExtREAL:] is Relation-like non empty V68() set
bool [:G,ExtREAL:] is non empty set
(G,(D * G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
bool REAL is non empty Element of bool (bool REAL)
[:NAT,(bool REAL):] is Relation-like non empty set
bool [:NAT,(bool REAL):] is non empty set
NAT --> REAL is Relation-like NAT -defined {REAL} -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,{REAL}:]
{REAL} is non empty set
[:NAT,{REAL}:] is Relation-like non empty set
bool [:NAT,{REAL}:] is non empty set
G0 is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng G0 is non empty Element of bool (bool REAL)
bool (bool REAL) is non empty set
union (rng G0) is V56() V57() V58() Element of bool REAL
D is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G0 . D is V56() V57() V58() Element of bool REAL
D is V56() V57() V58() Element of bool REAL
D is V56() V57() V58() Element of bool REAL
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D)
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . G is set
Funcs (NAT,(bool REAL)) is functional non empty FUNCTION_DOMAIN of NAT , bool REAL
[:NAT,(Funcs (NAT,(bool REAL))):] is Relation-like non empty set
bool [:NAT,(Funcs (NAT,(bool REAL))):] is non empty set
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
G is Relation-like NAT -defined bool REAL -valued Function-like V14( NAT ) quasi_total Element of Funcs (NAT,(bool REAL))
NAT --> G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool REAL))):]
G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool REAL))):]
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . A is V56() V57() V58() Element of bool REAL
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . A is Relation-like Function-like Element of Funcs (NAT,(bool REAL))
D . A is V56() V57() V58() Element of bool REAL
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . A is Relation-like Function-like Element of Funcs (NAT,(bool REAL))
D . A is V56() V57() V58() Element of bool REAL
D is V56() V57() V58() Element of bool REAL
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D)
D is V56() V57() V58() Element of bool REAL
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D)
(D,G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,G) . G is ext-real Element of ExtREAL
(D,G,G) is V56() V57() V58() interval Element of bool REAL
diameter (D,G,G) is ext-real Element of ExtREAL
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (D)
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . G is Relation-like Function-like set
D . G is V56() V57() V58() Element of bool REAL
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
Funcs (NAT,ExtREAL) is functional non empty FUNCTION_DOMAIN of NAT , ExtREAL
[:NAT,(Funcs (NAT,ExtREAL)):] is Relation-like non empty set
bool [:NAT,(Funcs (NAT,ExtREAL)):] is non empty set
G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (D)
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . G is V56() V57() V58() Element of bool REAL
(D,G,G) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . G)
((D . G),(D,G,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is Relation-like NAT -defined Funcs (NAT,ExtREAL) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,ExtREAL)):]
D is V56() V57() V58() Element of bool REAL
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D)
(D,G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (D,G) is ext-real Element of ExtREAL
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (D)
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . G is V56() V57() V58() Element of bool REAL
(D,G,G) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . G)
((D . G),(D,G,G)) is ext-real Element of ExtREAL
((D . G),(D,G,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((D . G),(D,G,G)) is ext-real Element of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . A is ext-real Element of ExtREAL
D . A is V56() V57() V58() Element of bool REAL
(D,G,A) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . A)
((D . A),(D,G,A)) is ext-real Element of ExtREAL
((D . A),(D,G,A)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((D . A),(D,G,A)) is ext-real Element of ExtREAL
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (D)
(D,G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,G) . G is ext-real Element of ExtREAL
D . G is V56() V57() V58() Element of bool REAL
(D,G,G) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . G)
((D . G),(D,G,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . G),(D,G,G)) . A is ext-real Element of ExtREAL
((D . G),(D,G,G),A) is V56() V57() V58() interval Element of bool REAL
diameter ((D . G),(D,G,G),A) is ext-real Element of ExtREAL
((D . G),(D,G,G)) is ext-real Element of ExtREAL
SUM ((D . G),(D,G,G)) is ext-real Element of ExtREAL
D is V56() V57() V58() Element of bool REAL
G is set
G is set
G is V57() Element of bool ExtREAL
A is ext-real Element of ExtREAL
B is ext-real Element of ExtREAL
F is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D)
(D,F) is ext-real Element of ExtREAL
(D,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (D,F) is ext-real Element of ExtREAL
G is V57() Element of bool ExtREAL
G is V57() Element of bool ExtREAL
D is V56() V57() V58() Element of bool REAL
(D) is V57() Element of bool ExtREAL
{} REAL is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval Element of bool REAL
{REAL,({} REAL)} is non empty set
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng G is non empty Element of bool (bool REAL)
G . 0 is V56() V57() V58() Element of bool REAL
{REAL,{}} is non empty set
union {REAL,{}} is set
REAL \/ {} is non empty V56() V57() V58() set
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . G is V56() V57() V58() Element of bool REAL
A is set
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D)
(D,G) is ext-real Element of ExtREAL
(D,G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (D,G) is ext-real Element of ExtREAL
D is V56() V57() V58() Element of bool REAL
(D) is non empty V57() Element of bool ExtREAL
inf (D) is ext-real Element of ExtREAL
[:(bool REAL),ExtREAL:] is Relation-like non empty V68() set
bool [:(bool REAL),ExtREAL:] is non empty set
D is Relation-like bool REAL -defined ExtREAL -valued Function-like non empty V14( bool REAL) quasi_total V68() Element of bool [:(bool REAL),ExtREAL:]
G is V56() V57() V58() Element of bool REAL
D . G is ext-real Element of ExtREAL
(G) is non empty V57() Element of bool ExtREAL
inf (G) is ext-real Element of ExtREAL
(G) is ext-real Element of ExtREAL
G is V56() V57() V58() Element of bool REAL
D . G is ext-real Element of ExtREAL
(G) is non empty V57() Element of bool ExtREAL
inf (G) is ext-real Element of ExtREAL
() is Relation-like bool REAL -defined ExtREAL -valued Function-like non empty V14( bool REAL) quasi_total V68() Element of bool [:(bool REAL),ExtREAL:]
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
G is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,[:NAT,NAT:]:]
rng G is Relation-like NAT -defined NAT -valued non empty V67() V68() V69() V70() Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty set
rng D is non empty Element of bool (bool REAL)
union (rng D) is V56() V57() V58() Element of bool REAL
pr1 G is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) quasi_total V67() V68() V69() V70() Element of bool [:NAT,NAT:]
G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (D)
pr2 G is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) quasi_total V67() V68() V69() V70() Element of bool [:NAT,NAT:]
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr1 G) . A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . ((pr1 G) . A) is V56() V57() V58() Element of bool REAL
(D,G,((pr1 G) . A)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . A))
(pr2 G) . A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . ((pr1 G) . A)),(D,G,((pr1 G) . A)),((pr2 G) . A)) is V56() V57() V58() interval Element of bool REAL
A is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng A is non empty Element of bool (bool REAL)
union (rng A) is V56() V57() V58() Element of bool REAL
B is set
F is set
dom D is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
n is set
D . n is set
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . n is V56() V57() V58() Element of bool REAL
(D,G,n) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . n)
rng (D,G,n) is non empty Element of bool (bool REAL)
union (rng (D,G,n)) is V56() V57() V58() Element of bool REAL
eps is set
dom (D,G,n) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
eps is set
(D,G,n) . eps is set
dom G is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
E is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
[n,E] is Element of [:NAT,NAT:]
{n,E} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{n} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{{n,E},{n}} is non empty set
FF is set
G . FF is set
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr1 G) . FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr2 G) . FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
[((pr1 G) . FF),((pr2 G) . FF)] is Element of [:NAT,NAT:]
{((pr1 G) . FF),((pr2 G) . FF)} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{((pr1 G) . FF)} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{{((pr1 G) . FF),((pr2 G) . FF)},{((pr1 G) . FF)}} is non empty set
A . FF is V56() V57() V58() Element of bool REAL
B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
A . B is V56() V57() V58() Element of bool REAL
(pr1 G) . B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . ((pr1 G) . B) is V56() V57() V58() Element of bool REAL
(D,G,((pr1 G) . B)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . B))
(pr2 G) . B is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . ((pr1 G) . B)),(D,G,((pr1 G) . B)),((pr2 G) . B)) is V56() V57() V58() interval Element of bool REAL
B is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng D))
F is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((union (rng D)),B,F) is V56() V57() V58() interval Element of bool REAL
(pr1 G) . F is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . ((pr1 G) . F) is V56() V57() V58() Element of bool REAL
(D,G,((pr1 G) . F)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . F))
(pr2 G) . F is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . ((pr1 G) . F)),(D,G,((pr1 G) . F)),((pr2 G) . F)) is V56() V57() V58() interval Element of bool REAL
A is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng D))
B is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng D))
F is set
A . F is set
B . F is set
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((union (rng D)),A,n) is V56() V57() V58() interval Element of bool REAL
(pr1 G) . n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . ((pr1 G) . n) is V56() V57() V58() Element of bool REAL
(D,G,((pr1 G) . n)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . n))
(pr2 G) . n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . ((pr1 G) . n)),(D,G,((pr1 G) . n)),((pr2 G) . n)) is V56() V57() V58() interval Element of bool REAL
{} REAL is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval Element of bool REAL
NAT --> ({} REAL) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total V67() V68() V69() V70() Element of bool [:NAT,(bool REAL):]
[:NAT,(bool REAL):] is Relation-like non empty set
bool [:NAT,(bool REAL):] is non empty set
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
G is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,[:NAT,NAT:]:]
rng G is Relation-like NAT -defined NAT -valued non empty V67() V68() V69() V70() Element of bool [:NAT,NAT:]
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
A + 1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
pr1 G is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) quasi_total V67() V68() V69() V70() Element of bool [:NAT,NAT:]
(pr1 G) . (A + 1) is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT : (pr1 G) . (A + 1) = (pr1 G) . b₁ } is set
F is set
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr1 G) . n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n + ((pr1 G) . (A + 1)) is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
eps is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng eps is non empty Element of bool (bool REAL)
union (rng eps) is V56() V57() V58() Element of bool REAL
eps is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (eps)
(eps,eps,G) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng eps))
((union (rng eps)),(eps,eps,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser ((union (rng eps)),(eps,eps,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser ((union (rng eps)),(eps,eps,G))) . (A + 1) is ext-real Element of ExtREAL
(eps,eps) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser (eps,eps) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (eps,eps)) . n is ext-real Element of ExtREAL
E is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
eps . E is V56() V57() V58() Element of bool REAL
(eps,eps,E) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (eps . E)
FF is Relation-like NAT -defined bool REAL -valued Function-like V14( NAT ) quasi_total Element of Funcs (NAT,(bool REAL))
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FF . FF is set
((eps . E),(eps,eps,E),FF) is V56() V57() V58() interval Element of bool REAL
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FF . G0 is set
G is Relation-like NAT -defined bool REAL -valued Function-like V14( NAT ) quasi_total Element of Funcs (NAT,(bool REAL))
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . FF is set
((eps . E),(eps,eps,E),FF) is V56() V57() V58() interval Element of bool REAL
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . FF is set
E is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool REAL))):]
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
E . FF is Relation-like Function-like Element of Funcs (NAT,(bool REAL))
D . FF is V56() V57() V58() Element of bool REAL
FF is Relation-like Function-like set
dom FF is set
rng FF is set
G0 is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G0 . n is V56() V57() V58() Element of bool REAL
eps . FF is V56() V57() V58() Element of bool REAL
(eps,eps,FF) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (eps . FF)
((eps . FF),(eps,eps,FF),n) is V56() V57() V58() interval Element of bool REAL
rng G0 is non empty Element of bool (bool REAL)
union (rng G0) is V56() V57() V58() Element of bool REAL
n is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . FF)
F is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
pr2 G is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) quasi_total V67() V68() V69() V70() Element of bool [:NAT,NAT:]
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
eps . FF is V56() V57() V58() Element of bool REAL
(eps,eps,FF) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (eps . FF)
FF is Relation-like NAT -defined bool REAL -valued Function-like V14( NAT ) quasi_total Element of Funcs (NAT,(bool REAL))
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FF . G0 is set
((eps . FF),(eps,eps,FF),G0) is V56() V57() V58() interval Element of bool REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FF . n is set
G is Relation-like NAT -defined bool REAL -valued Function-like V14( NAT ) quasi_total Element of Funcs (NAT,(bool REAL))
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . FF is set
((eps . FF),(eps,eps,FF),FF) is V56() V57() V58() interval Element of bool REAL
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . G0 is set
FF is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool REAL))):]
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FF . FF is Relation-like Function-like Element of Funcs (NAT,(bool REAL))
D . FF is V56() V57() V58() Element of bool REAL
G0 is Relation-like Function-like set
dom G0 is set
rng G0 is set
n is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
n . FS is V56() V57() V58() Element of bool REAL
eps . FF is V56() V57() V58() Element of bool REAL
(eps,eps,FF) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (eps . FF)
((eps . FF),(eps,eps,FF),FS) is V56() V57() V58() interval Element of bool REAL
rng n is non empty Element of bool (bool REAL)
union (rng n) is V56() V57() V58() Element of bool REAL
FS is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . FF)
FF is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (D)
(D,FF,G) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng D))
rng D is non empty Element of bool (bool REAL)
union (rng D) is V56() V57() V58() Element of bool REAL
n is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (D)
(D,n,G) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng D))
((union (rng D)),(D,FF,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser ((union (rng D)),(D,FF,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser ((union (rng D)),(D,FF,G))) . (A + 1) is ext-real Element of ExtREAL
SUM ((union (rng D)),(D,FF,G)) is ext-real Element of ExtREAL
((union (rng D)),(D,n,G),(A + 1)) is V56() V57() V58() interval Element of bool REAL
D . ((pr1 G) . (A + 1)) is V56() V57() V58() Element of bool REAL
(D,n,((pr1 G) . (A + 1))) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . (A + 1)))
(pr2 G) . (A + 1) is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . ((pr1 G) . (A + 1))),(D,n,((pr1 G) . (A + 1))),((pr2 G) . (A + 1))) is V56() V57() V58() interval Element of bool REAL
((union (rng D)),(D,n,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
((union (rng D)),(D,n,G)) . (A + 1) is ext-real Element of ExtREAL
Ser ((union (rng D)),(D,n,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser ((union (rng D)),(D,n,G))) . (A + 1) is ext-real Element of ExtREAL
(Ser ((union (rng D)),(D,n,G))) . A is ext-real Element of ExtREAL
((Ser ((union (rng D)),(D,n,G))) . A) + (((union (rng D)),(D,n,G)) . (A + 1)) is ext-real Element of ExtREAL
(D,n) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,n) . FS is ext-real Element of ExtREAL
Ser (D,n) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (D,n)) . n is ext-real Element of ExtREAL
(Ser (D,n)) . n is ext-real Element of ExtREAL
FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((union (rng eps)),(eps,eps,G)) . FS is ext-real Element of ExtREAL
((union (rng D)),(D,FF,G)) . FS is ext-real Element of ExtREAL
((union (rng D)),(D,n,G)) . FS is ext-real Element of ExtREAL
(((union (rng D)),(D,FF,G)) . FS) + (((union (rng D)),(D,n,G)) . FS) is ext-real Element of ExtREAL
((union (rng D)),(D,FF,G),FS) is V56() V57() V58() interval Element of bool REAL
diameter ((union (rng D)),(D,FF,G),FS) is ext-real Element of ExtREAL
((union (rng D)),(D,n,G),FS) is V56() V57() V58() interval Element of bool REAL
diameter ((union (rng D)),(D,n,G),FS) is ext-real Element of ExtREAL
((union (rng eps)),(eps,eps,G),FS) is V56() V57() V58() interval Element of bool REAL
diameter ((union (rng eps)),(eps,eps,G),FS) is ext-real Element of ExtREAL
(pr1 G) . FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
eps . ((pr1 G) . FS) is V56() V57() V58() Element of bool REAL
(eps,eps,((pr1 G) . FS)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (eps . ((pr1 G) . FS))
(pr2 G) . FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((eps . ((pr1 G) . FS)),(eps,eps,((pr1 G) . FS)),((pr2 G) . FS)) is V56() V57() V58() interval Element of bool REAL
diameter ((eps . ((pr1 G) . FS)),(eps,eps,((pr1 G) . FS)),((pr2 G) . FS)) is ext-real Element of ExtREAL
D . ((pr1 G) . FS) is V56() V57() V58() Element of bool REAL
(D,n,((pr1 G) . FS)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . FS))
((D . ((pr1 G) . FS)),(D,n,((pr1 G) . FS)),((pr2 G) . FS)) is V56() V57() V58() interval Element of bool REAL
(D,FF,((pr1 G) . FS)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . FS))
((D . ((pr1 G) . FS)),(D,FF,((pr1 G) . FS)),((pr2 G) . FS)) is V56() V57() V58() interval Element of bool REAL
D . ((pr1 G) . FS) is V56() V57() V58() Element of bool REAL
(D,FF,((pr1 G) . FS)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . FS))
((D . ((pr1 G) . FS)),(D,FF,((pr1 G) . FS)),((pr2 G) . FS)) is V56() V57() V58() interval Element of bool REAL
(D,n,((pr1 G) . FS)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . FS))
((D . ((pr1 G) . FS)),(D,n,((pr1 G) . FS)),((pr2 G) . FS)) is V56() V57() V58() interval Element of bool REAL
((Ser ((union (rng D)),(D,FF,G))) . (A + 1)) + ((Ser ((union (rng D)),(D,n,G))) . (A + 1)) is ext-real Element of ExtREAL
FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,n) . FS is ext-real Element of ExtREAL
FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real real Element of F
(pr2 G) . FS is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
[:F,NAT:] is Relation-like RAT -valued INT -valued non empty V67() V68() V69() V70() set
bool [:F,NAT:] is non empty set
FS is Relation-like F -defined NAT -valued Function-like non empty V14(F) quasi_total V67() V68() V69() V70() Element of bool [:F,NAT:]
(D,FF) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(eps,eps) . c₁₉ is ext-real Element of ExtREAL
(D,FF) . c₁₉ is ext-real Element of ExtREAL
(D,n) . c₁₉ is ext-real Element of ExtREAL
((D,FF) . c₁₉) + ((D,n) . c₁₉) is ext-real Element of ExtREAL
eps . c₁₉ is V56() V57() V58() Element of bool REAL
(eps,eps,c₁₉) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (eps . c₁₉)
((eps . c₁₉),(eps,eps,c₁₉)) is ext-real Element of ExtREAL
((eps . c₁₉),(eps,eps,c₁₉)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((eps . c₁₉),(eps,eps,c₁₉)) is ext-real Element of ExtREAL
D . c₁₉ is V56() V57() V58() Element of bool REAL
(D,FF,c₁₉) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . c₁₉)
((D . c₁₉),(D,FF,c₁₉)) is ext-real Element of ExtREAL
((D . c₁₉),(D,FF,c₁₉)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((D . c₁₉),(D,FF,c₁₉)) is ext-real Element of ExtREAL
(D,n,c₁₉) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . c₁₉)
((D . c₁₉),(D,n,c₁₉)) is ext-real Element of ExtREAL
((D . c₁₉),(D,n,c₁₉)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((D . c₁₉),(D,n,c₁₉)) is ext-real Element of ExtREAL
((D . c₁₉),(D,FF,c₁₉)) + ((D . c₁₉),(D,n,c₁₉)) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((eps . c₁₉),(eps,eps,c₁₉)) . s2 is ext-real Element of ExtREAL
((D . c₁₉),(D,FF,c₁₉)) . s2 is ext-real Element of ExtREAL
((D . c₁₉),(D,FF,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((D . c₁₉),(D,FF,c₁₉),s2) is ext-real Element of ExtREAL
((eps . c₁₉),(eps,eps,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((eps . c₁₉),(eps,eps,c₁₉),s2) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . c₁₉),(D,n,c₁₉)) . s2 is ext-real Element of ExtREAL
((D . c₁₉),(D,n,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((D . c₁₉),(D,n,c₁₉),s2) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . c₁₉),(D,FF,c₁₉)) . s2 is ext-real Element of ExtREAL
((eps . c₁₉),(eps,eps,c₁₉)) . s2 is ext-real Element of ExtREAL
((D . c₁₉),(D,FF,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((D . c₁₉),(D,FF,c₁₉),s2) is ext-real Element of ExtREAL
((eps . c₁₉),(eps,eps,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((eps . c₁₉),(eps,eps,c₁₉),s2) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . c₁₉),(D,n,c₁₉)) . s2 is ext-real Element of ExtREAL
((eps . c₁₉),(eps,eps,c₁₉)) . s2 is ext-real Element of ExtREAL
((D . c₁₉),(D,n,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((D . c₁₉),(D,n,c₁₉),s2) is ext-real Element of ExtREAL
((eps . c₁₉),(eps,eps,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((eps . c₁₉),(eps,eps,c₁₉),s2) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((eps . c₁₉),(eps,eps,c₁₉)) . s2 is ext-real Element of ExtREAL
((D . c₁₉),(D,n,c₁₉)) . s2 is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . c₁₉),(D,FF,c₁₉)) . s2 is ext-real Element of ExtREAL
((D . c₁₉),(D,FF,c₁₉),s2) is V56() V57() V58() interval Element of bool REAL
diameter ((D . c₁₉),(D,FF,c₁₉),s2) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . c₁₉),(D,n,c₁₉)) . s2 is ext-real Element of ExtREAL
((eps . c₁₉),(eps,eps,c₁₉)) . s2 is ext-real Element of ExtREAL
c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,FF) . c₁₉ is ext-real Element of ExtREAL
(D,FF) . ((pr1 G) . (A + 1)) is ext-real Element of ExtREAL
Ser (D,FF) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (D,FF)) . ((pr1 G) . (A + 1)) is ext-real Element of ExtREAL
(Ser (D,FF)) . n is ext-real Element of ExtREAL
(D,FF,((pr1 G) . (A + 1))) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . (A + 1)))
((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1)))) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1)))) * FS is Relation-like F -defined ExtREAL -valued Function-like non empty V14(F) quasi_total V68() Element of bool [:F,ExtREAL:]
[:F,ExtREAL:] is Relation-like non empty V68() set
bool [:F,ExtREAL:] is non empty set
c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((union (rng D)),(D,FF,G)) . c₁₉ is ext-real Element of ExtREAL
(((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1)))) * FS) . c₁₉ is ext-real Element of ExtREAL
(pr2 G) . c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FS . c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((union (rng D)),(D,FF,G),c₁₉) is V56() V57() V58() interval Element of bool REAL
diameter ((union (rng D)),(D,FF,G),c₁₉) is ext-real Element of ExtREAL
((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1))),((pr2 G) . c₁₉)) is V56() V57() V58() interval Element of bool REAL
diameter ((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1))),((pr2 G) . c₁₉)) is ext-real Element of ExtREAL
((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1)))) . (FS . c₁₉) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr1 G) . s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr1 G) . c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((union (rng D)),(D,FF,G),c₁₉) is V56() V57() V58() interval Element of bool REAL
diameter ((union (rng D)),(D,FF,G),c₁₉) is ext-real Element of ExtREAL
D . ((pr1 G) . c₁₉) is V56() V57() V58() Element of bool REAL
(D,FF,((pr1 G) . c₁₉)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (D . ((pr1 G) . c₁₉))
(pr2 G) . c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((D . ((pr1 G) . c₁₉)),(D,FF,((pr1 G) . c₁₉)),((pr2 G) . c₁₉)) is V56() V57() V58() interval Element of bool REAL
diameter ((D . ((pr1 G) . c₁₉)),(D,FF,((pr1 G) . c₁₉)),((pr2 G) . c₁₉)) is ext-real Element of ExtREAL
c₁₉ is set
s2 is set
FS . c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FS . s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
G . s1 is Element of [:NAT,NAT:]
(pr1 G) . s1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr2 G) . s1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
[((pr1 G) . s1),((pr2 G) . s1)] is Element of [:NAT,NAT:]
{((pr1 G) . s1),((pr2 G) . s1)} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{((pr1 G) . s1)} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{{((pr1 G) . s1),((pr2 G) . s1)},{((pr1 G) . s1)}} is non empty set
G . s2 is Element of [:NAT,NAT:]
(pr1 G) . s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr2 G) . s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
[((pr1 G) . s2),((pr2 G) . s2)] is Element of [:NAT,NAT:]
{((pr1 G) . s2),((pr2 G) . s2)} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{((pr1 G) . s2)} is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below set
{{((pr1 G) . s2),((pr2 G) . s2)},{((pr1 G) . s2)}} is non empty set
FS . s1 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FS . s2 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
c₂₃ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr1 G) . c₂₃ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(pr1 G) . c₂₄ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
SUM ((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1)))) is ext-real Element of ExtREAL
((D . ((pr1 G) . (A + 1))),(D,FF,((pr1 G) . (A + 1)))) is ext-real Element of ExtREAL
c₁₉ is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(D,FF) . c₁₉ is ext-real Element of ExtREAL
((Ser (D,FF)) . n) + ((Ser (D,n)) . n) is ext-real Element of ExtREAL
pr1 G is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) quasi_total V67() V68() V69() V70() Element of bool [:NAT,NAT:]
(pr1 G) . 0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
B is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng B is non empty Element of bool (bool REAL)
union (rng B) is V56() V57() V58() Element of bool REAL
F is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (B)
(B,F,G) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng B))
((union (rng B)),(B,F,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser ((union (rng B)),(B,F,G)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser ((union (rng B)),(B,F,G))) . 0 is ext-real Element of ExtREAL
(B,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser (B,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (B,F)) . A is ext-real Element of ExtREAL
n is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng B))
((union (rng B)),n) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
((union (rng B)),n) . 0 is ext-real Element of ExtREAL
((union (rng B)),n,0) is V56() V57() V58() interval Element of bool REAL
diameter ((union (rng B)),n,0) is ext-real Element of ExtREAL
B . ((pr1 G) . 0) is V56() V57() V58() Element of bool REAL
(B,F,((pr1 G) . 0)) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (B . ((pr1 G) . 0))
((B . ((pr1 G) . 0)),(B,F,((pr1 G) . 0))) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
pr2 G is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) quasi_total V67() V68() V69() V70() Element of bool [:NAT,NAT:]
(pr2 G) . 0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
((B . ((pr1 G) . 0)),(B,F,((pr1 G) . 0))) . ((pr2 G) . 0) is ext-real Element of ExtREAL
((B . ((pr1 G) . 0)),(B,F,((pr1 G) . 0)),((pr2 G) . 0)) is V56() V57() V58() interval Element of bool REAL
diameter ((B . ((pr1 G) . 0)),(B,F,((pr1 G) . 0)),((pr2 G) . 0)) is ext-real Element of ExtREAL
((B . ((pr1 G) . 0)),(B,F,((pr1 G) . 0))) is ext-real Element of ExtREAL
SUM ((B . ((pr1 G) . 0)),(B,F,((pr1 G) . 0))) is ext-real Element of ExtREAL
Ser ((union (rng B)),n) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser ((union (rng B)),n)) . 0 is ext-real Element of ExtREAL
(B,F) . ((pr1 G) . 0) is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(B,F) . n is ext-real Element of ExtREAL
(B,F) . A is ext-real Element of ExtREAL
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng G is non empty Element of bool (bool REAL)
union (rng G) is V56() V57() V58() Element of bool REAL
((union (rng G))) is non empty V57() Element of bool ExtREAL
inf ((union (rng G))) is ext-real Element of ExtREAL
G is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (G)
(G,G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (G,G) is ext-real Element of ExtREAL
A is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,[:NAT,NAT:]:]
dom A is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
rng A is Relation-like NAT -defined NAT -valued non empty V67() V68() V69() V70() Element of bool [:NAT,NAT:]
A is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,[:NAT,NAT:]:]
dom A is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
rng A is Relation-like NAT -defined NAT -valued non empty V67() V68() V69() V70() Element of bool [:NAT,NAT:]
(G,G,A) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( union (rng G))
((union (rng G)),(G,G,A)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
Ser ((union (rng G)),(G,G,A)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
rng (Ser ((union (rng G)),(G,G,A))) is non empty V48() V57() Element of bool ExtREAL
Ser (G,G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
rng (Ser (G,G)) is non empty V48() V57() Element of bool ExtREAL
F is ext-real set
dom (Ser ((union (rng G)),(G,G,A))) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
n is set
(Ser ((union (rng G)),(G,G,A))) . n is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(Ser (G,G)) . eps is ext-real Element of ExtREAL
dom (Ser (G,G)) is non empty V56() V57() V58() V59() V60() V61() left_end bounded_below Element of bool NAT
((union (rng G)),(G,G,A)) is ext-real Element of ExtREAL
SUM ((union (rng G)),(G,G,A)) is ext-real Element of ExtREAL
sup (rng (Ser ((union (rng G)),(G,G,A)))) is ext-real Element of ExtREAL
sup (rng (Ser (G,G))) is ext-real Element of ExtREAL
D is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng D is non empty Element of bool (bool REAL)
union (rng D) is V56() V57() V58() Element of bool REAL
G is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
D . G is V56() V57() V58() Element of bool REAL
A is V56() V57() V58() Element of bool REAL
B is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (A)
(A,B) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
F is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(A,B) . F is ext-real Element of ExtREAL
(A,B,F) is V56() V57() V58() interval Element of bool REAL
diameter (A,B,F) is ext-real Element of ExtREAL
A is V56() V57() V58() Element of bool REAL
() . A is ext-real Element of ExtREAL
(A) is non empty V57() Element of bool ExtREAL
B is ext-real set
F is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (A)
(A,F) is ext-real Element of ExtREAL
(A,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (A,F) is ext-real Element of ExtREAL
Ser (A,F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (A,F)) . 0 is ext-real Element of ExtREAL
rng (Ser (A,F)) is non empty V48() V57() Element of bool ExtREAL
sup (rng (Ser (A,F))) is ext-real Element of ExtREAL
inf (A) is ext-real Element of ExtREAL
G is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total ( {} REAL)
(({} REAL),G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
A is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(({} REAL),G) . A is ext-real Element of ExtREAL
(({} REAL),G,A) is V56() V57() V58() interval Element of bool REAL
diameter (({} REAL),G,A) is ext-real Element of ExtREAL
(({} REAL),G) is ext-real Element of ExtREAL
SUM (({} REAL),G) is ext-real Element of ExtREAL
Ser (({} REAL),G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
(Ser (({} REAL),G)) . 0 is ext-real Element of ExtREAL
(({} REAL),G) . 0 is ext-real Element of ExtREAL
(({} REAL)) is non empty V57() Element of bool ExtREAL
A is ext-real set
inf (({} REAL)) is ext-real Element of ExtREAL
() . ({} REAL) is ext-real Element of ExtREAL
inf (({} REAL)) is ext-real Element of ExtREAL
() . {} is ext-real Element of ExtREAL
A is V56() V57() V58() Element of bool REAL
B is V56() V57() V58() Element of bool REAL
() . A is ext-real Element of ExtREAL
() . B is ext-real Element of ExtREAL
(B) is non empty V57() Element of bool ExtREAL
(A) is non empty V57() Element of bool ExtREAL
F is set
n is ext-real Element of ExtREAL
n is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (B)
(B,n) is ext-real Element of ExtREAL
(B,n) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (B,n) is ext-real Element of ExtREAL
rng n is non empty Element of bool (bool REAL)
union (rng n) is V56() V57() V58() Element of bool REAL
eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(B,n,eps) is V56() V57() V58() interval Element of bool REAL
eps is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (A)
(A,eps) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(B,n) . eps is ext-real Element of ExtREAL
(A,eps) . eps is ext-real Element of ExtREAL
(A,eps,eps) is V56() V57() V58() interval Element of bool REAL
diameter (A,eps,eps) is ext-real Element of ExtREAL
SUM (A,eps) is ext-real Element of ExtREAL
eps is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(A,eps) . eps is ext-real Element of ExtREAL
(B,n) . eps is ext-real Element of ExtREAL
(A,eps,eps) is V56() V57() V58() interval Element of bool REAL
diameter (A,eps,eps) is ext-real Element of ExtREAL
(A,eps) is ext-real Element of ExtREAL
inf (A) is ext-real Element of ExtREAL
inf (B) is ext-real Element of ExtREAL
F is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool REAL):]
rng F is non empty Element of bool (bool REAL)
union (rng F) is V56() V57() V58() Element of bool REAL
() . (union (rng F)) is ext-real Element of ExtREAL
() * F is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (() * F) is ext-real Element of ExtREAL
{+infty} is non empty V57() Element of bool ExtREAL
Ser (() * F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
rng (Ser (() * F)) is non empty V48() V57() Element of bool ExtREAL
sup (rng (Ser (() * F))) is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(() * F) . n is ext-real Element of ExtREAL
F . n is V56() V57() V58() Element of bool REAL
() . (F . n) is ext-real Element of ExtREAL
((union (rng F))) is non empty V57() Element of bool ExtREAL
inf ((union (rng F))) is ext-real Element of ExtREAL
(() * F) . 0 is ext-real Element of ExtREAL
(Ser (() * F)) . 0 is ext-real Element of ExtREAL
eps is V30() ext-real real set
(sup (rng (Ser (() * F)))) + eps is ext-real set
eps is ext-real Element of ExtREAL
E is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM E is ext-real Element of ExtREAL
(SUM (() * F)) + (SUM E) is ext-real Element of ExtREAL
(SUM (() * F)) + eps is ext-real Element of ExtREAL
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
F . FF is V56() V57() V58() Element of bool REAL
((F . FF)) is non empty V57() Element of bool ExtREAL
inf ((F . FF)) is ext-real Element of ExtREAL
E . FF is ext-real Element of ExtREAL
(inf ((F . FF))) + (E . FF) is ext-real Element of ExtREAL
() . (F . FF) is ext-real Element of ExtREAL
((F . FF)) \ {+infty} is V57() Element of bool ExtREAL
FF is set
G0 is ext-real Element of ExtREAL
n is ext-real set
FS is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (F . FF)
((F . FF),FS) is ext-real Element of ExtREAL
((F . FF),FS) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((F . FF),FS) is ext-real Element of ExtREAL
FS is Relation-like NAT -defined bool REAL -valued Function-like V14( NAT ) quasi_total Element of Funcs (NAT,(bool REAL))
FF is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool REAL))):]
FF is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
FF . FF is Relation-like Function-like Element of Funcs (NAT,(bool REAL))
F . FF is V56() V57() V58() Element of bool REAL
((F . FF)) is non empty V57() Element of bool ExtREAL
inf ((F . FF)) is ext-real Element of ExtREAL
E . FF is ext-real Element of ExtREAL
(inf ((F . FF))) + (E . FF) is ext-real Element of ExtREAL
G0 is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (F . FF)
((F . FF),G0) is ext-real Element of ExtREAL
((F . FF),G0) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((F . FF),G0) is ext-real Element of ExtREAL
FF is Relation-like NAT -defined Funcs (NAT,(bool REAL)) -valued Function-like non empty V14( NAT ) quasi_total (F)
(F,FF) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM (F,FF) is ext-real Element of ExtREAL
G0 is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(() * F) . G0 is ext-real Element of ExtREAL
E . G0 is ext-real Element of ExtREAL
((() * F) . G0) + (E . G0) is ext-real Element of ExtREAL
G0 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(F,FF) . n is ext-real Element of ExtREAL
G0 . n is ext-real Element of ExtREAL
F . n is V56() V57() V58() Element of bool REAL
(F,FF,n) is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (F . n)
((F . n)) is non empty V57() Element of bool ExtREAL
inf ((F . n)) is ext-real Element of ExtREAL
E . n is ext-real Element of ExtREAL
(inf ((F . n))) + (E . n) is ext-real Element of ExtREAL
(() * F) . n is ext-real Element of ExtREAL
() . (F . n) is ext-real Element of ExtREAL
((() * F) . n) + (E . n) is ext-real Element of ExtREAL
((F . n),(F,FF,n)) is ext-real Element of ExtREAL
((F . n),(F,FF,n)) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((F . n),(F,FF,n)) is ext-real Element of ExtREAL
FS is Relation-like NAT -defined bool REAL -valued Function-like non empty V14( NAT ) quasi_total (F . n)
((F . n),FS) is ext-real Element of ExtREAL
((F . n),FS) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) quasi_total V68() Element of bool [:NAT,ExtREAL:]
SUM ((F . n),FS) is ext-real Element of ExtREAL
SUM G0 is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
E . n is ext-real Element of ExtREAL
{+infty} is non empty V57() Element of bool ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
F . n is V56() V57() V58() Element of bool REAL
((F . n)) is non empty V57() Element of bool ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
F . n is V56() V57() V58() Element of bool REAL
((F . n)) is non empty V57() Element of bool ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
(() * F) . n is ext-real Element of ExtREAL
F . n is V56() V57() V58() Element of bool REAL
() . (F . n) is ext-real Element of ExtREAL
inf {+infty} is ext-real Element of ExtREAL
() . (F . n) is ext-real Element of ExtREAL
(() * F) . n is ext-real Element of ExtREAL
{+infty} is non empty V57() Element of bool ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below Element of NAT
F . n is V56() V57() V58() Element of bool REAL
((F . n)) is non empty V57() Element of bool ExtREAL
() is Relation-like bool REAL -defined ExtREAL -valued Function-like non empty V14( bool REAL) quasi_total V68() C_Measure of REAL
sigma_Field () is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool REAL)
() is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool REAL)
sigma_Meas () is Relation-like sigma_Field () -defined ExtREAL -valued Function-like non empty V14( sigma_Field ()) quasi_total V68() V76() nonnegative sigma-additive Element of bool [:(sigma_Field ()),ExtREAL:]
[:(sigma_Field ()),ExtREAL:] is Relation-like non empty V68() set
bool [:(sigma_Field ()),ExtREAL:] is non empty set
[:(),ExtREAL:] is Relation-like non empty V68() set
bool [:(),ExtREAL:] is non empty set
() is Relation-like () -defined ExtREAL -valued Function-like non empty V14(()) quasi_total V68() V76() nonnegative sigma-additive Element of bool [:(),ExtREAL:]