:: MEASURE8 semantic presentation

REAL is non empty V34() V73() V74() V75() V79() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V74() set
[:NAT,ExtREAL:] is non empty ext-real-valued set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
bool REAL is non empty Element of bool (bool REAL)
bool (bool REAL) is non empty set
[:NAT,(bool REAL):] is non empty set
bool [:NAT,(bool REAL):] is non empty set
Funcs (NAT,(bool REAL)) is non empty functional FUNCTION_DOMAIN of NAT , bool REAL
[:NAT,(Funcs (NAT,(bool REAL))):] is non empty set
bool [:NAT,(Funcs (NAT,(bool REAL))):] is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() set
bool omega is non empty set
[:NAT,REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
bool NAT is non empty set
COMPLEX is non empty V34() V73() V79() set
RAT is non empty V34() V73() V74() V75() V76() V79() set
INT is non empty V34() V73() V74() V75() V76() V77() V79() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V73() V74() V75() V76() V77() V78() V79() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
{{},1} is non empty V73() V74() V75() V76() V77() V78() set
Funcs (NAT,ExtREAL) is non empty functional FUNCTION_DOMAIN of NAT , ExtREAL
[:NAT,(Funcs (NAT,ExtREAL)):] is non empty set
bool [:NAT,(Funcs (NAT,ExtREAL)):] is non empty set
[:(bool REAL),ExtREAL:] is non empty ext-real-valued set
bool [:(bool REAL),ExtREAL:] is non empty set
K464() is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool REAL)
[:K464(),ExtREAL:] is non empty ext-real-valued set
bool [:K464(),ExtREAL:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V58() V62() V73() V74() V75() V76() V77() V78() V79() Element of NAT
Seg 1 is V73() V74() V75() V76() V77() V78() Element of bool NAT
{1} is non empty V73() V74() V75() V76() V77() V78() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Seg 2 is V73() V74() V75() V76() V77() V78() Element of bool NAT
{1,2} is non empty V73() V74() V75() V76() V77() V78() set
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V73() V74() V75() V76() V77() V78() V79() Element of ExtREAL
+infty is non empty ext-real positive non negative non real Element of ExtREAL
+infty is non empty ext-real positive non negative non real set
-infty is non empty ext-real non positive negative non real set
PairFunc is non empty Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V27([:NAT,NAT:]) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Partial_Sums X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
F is set
(Ser X) . F is ext-real Element of ExtREAL
(Partial_Sums X) . F is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser X) . m is ext-real Element of ExtREAL
(Partial_Sums X) . m is ext-real Element of ExtREAL
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser X) . (m + 1) is ext-real Element of ExtREAL
(Partial_Sums X) . (m + 1) is ext-real Element of ExtREAL
X . (m + 1) is ext-real Element of ExtREAL
((Partial_Sums X) . m) + (X . (m + 1)) is ext-real set
(Ser X) . 0 is ext-real Element of ExtREAL
X . 0 is ext-real Element of ExtREAL
(Partial_Sums X) . 0 is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums X) . m is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM X is ext-real Element of ExtREAL
Ser X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser X) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser X)) is ext-real Element of ExtREAL
Sum X is ext-real Element of ExtREAL
Partial_Sums X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (Partial_Sums X) is ext-real Element of ExtREAL
sup (Partial_Sums X) is ext-real Element of ExtREAL
rng (Partial_Sums X) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Partial_Sums X)) is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM X is ext-real Element of ExtREAL
Ser X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser X) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser X)) is ext-real Element of ExtREAL
Sum X is ext-real Element of ExtREAL
Partial_Sums X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (Partial_Sums X) is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM F is ext-real Element of ExtREAL
Ser F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser F) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser F)) is ext-real Element of ExtREAL
(SUM X) + (SUM F) is ext-real set
Sum F is ext-real Element of ExtREAL
Partial_Sums F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (Partial_Sums F) is ext-real Element of ExtREAL
(Sum X) + (Sum F) is ext-real set
m is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM m is ext-real Element of ExtREAL
Ser m is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser m) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser m)) is ext-real Element of ExtREAL
Sum m is ext-real Element of ExtREAL
Partial_Sums m is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (Partial_Sums m) is ext-real Element of ExtREAL
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
m . Bseq is ext-real Element of ExtREAL
X . Bseq is ext-real Element of ExtREAL
F . Bseq is ext-real Element of ExtREAL
(X . Bseq) + (F . Bseq) is ext-real set
M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
M1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M . Bseq is ext-real Element of ExtREAL
Aseq . Bseq is ext-real Element of ExtREAL
M1 . Bseq is ext-real Element of ExtREAL
(Aseq . Bseq) + (M1 . Bseq) is ext-real set
dom M is V73() V74() V75() V76() V77() V78() Element of bool NAT
Bseq is ext-real set
B is ext-real set
M . Bseq is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
Aseq . Bseq is ext-real Element of ExtREAL
Aseq . B is ext-real Element of ExtREAL
M1 . Bseq is ext-real Element of ExtREAL
M1 . B is ext-real Element of ExtREAL
(Aseq . Bseq) + (M1 . Bseq) is ext-real set
(Aseq . B) + (M1 . B) is ext-real set
lim M is ext-real Element of ExtREAL
sup M is ext-real Element of ExtREAL
rng M is non empty V45() V74() Element of bool ExtREAL
sup (rng M) is ext-real Element of ExtREAL
lim Aseq is ext-real Element of ExtREAL
sup Aseq is ext-real Element of ExtREAL
rng Aseq is non empty V45() V74() Element of bool ExtREAL
sup (rng Aseq) is ext-real Element of ExtREAL
Bseq is set
dom m is V73() V74() V75() V76() V77() V78() Element of bool NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
F . B is ext-real Element of ExtREAL
m . Bseq is ext-real Element of ExtREAL
X . B is ext-real Element of ExtREAL
(X . B) + (F . B) is ext-real set
lim M1 is ext-real Element of ExtREAL
sup M1 is ext-real Element of ExtREAL
rng M1 is non empty V45() V74() Element of bool ExtREAL
sup (rng M1) is ext-real Element of ExtREAL
(Sum X) + (SUM F) is ext-real set
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:NAT,F:] is non empty set
bool [:NAT,F:] is non empty set
{{}} is non empty V73() V74() V75() V76() V77() V78() set
[:NAT,{{}}:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,{{}}:] is non empty set
m is non empty Relation-like NAT -defined {{}} -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,{{}}:]
M1 is non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,F:]
Aseq is set
M1 . Aseq is set
dom M1 is V73() V74() V75() V76() V77() V78() Element of bool NAT
Aseq is set
M is set
M1 . Aseq is set
M1 . M is set
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
m is Relation-like NAT -defined bool X -valued Function-like FinSequence-like FinSequence of bool X
dom m is V73() V74() V75() V76() V77() V78() Element of bool NAT
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
m . M1 is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
<*{}*> is Relation-like Function-like set
m is Relation-like NAT -defined bool X -valued Function-like FinSequence-like FinSequence of bool X
dom m is V73() V74() V75() V76() V77() V78() Element of bool NAT
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
m . M1 is Element of bool X
M1 is Relation-like NAT -defined bool X -valued Function-like FinSequence-like (X,F)
Aseq is set
M1 . Aseq is set
dom M1 is V73() V74() V75() V76() V77() V78() Element of bool NAT
Aseq is set
M is set
M1 . Aseq is set
M1 . M is set
X is set
bool X is non empty set
bool (bool X) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]
{X} is non empty set
[:NAT,{X}:] is non empty set
bool [:NAT,{X}:] is non empty set
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
m . M1 is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
m is non empty compl-closed V84() V85() V86() Element of bool (bool X)
F is Element of bool X
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]
{X} is non empty set
[:NAT,{X}:] is non empty set
bool [:NAT,{X}:] is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M1 . Aseq is Element of bool X
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m)
rng Aseq is Element of bool (bool X)
bool (bool X) is non empty set
union (rng Aseq) is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
m . M1 is set
X is set
bool X is non empty set
bool (bool X) is non empty set
NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]
{X} is non empty set
[:NAT,{X}:] is non empty set
bool [:NAT,{X}:] is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
rng (NAT --> X) is Element of bool {X}
bool {X} is non empty set
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
m . M1 is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
[:NAT,(Funcs (NAT,(bool X))):] is non empty set
bool [:NAT,(Funcs (NAT,(bool X))):] is non empty set
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]
{X} is non empty set
[:NAT,{X}:] is non empty set
bool [:NAT,{X}:] is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
Aseq is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
NAT --> Aseq is non empty T-Sequence-like Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]
M is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]
rng (NAT --> X) is Element of bool {X}
bool {X} is non empty set
union (rng (NAT --> X)) is set
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
m . Bseq is Element of bool X
M . Bseq is Relation-like Function-like Element of Funcs (NAT,(bool X))
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
bool X is non empty Element of bool (bool X)
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Aseq . M is ext-real Element of ExtREAL
(X,F,M1,M) is Element of F
m . (X,F,M1,M) is ext-real Element of ExtREAL
Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Bseq is set
Aseq . Bseq is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(X,F,M1,B) is Element of F
m . (X,F,M1,B) is ext-real Element of ExtREAL
M . Bseq is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
(X,F,m,M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,M1) . Aseq is ext-real Element of ExtREAL
(X,F,M1,Aseq) is Element of F
m . (X,F,M1,Aseq) is ext-real Element of ExtREAL
m . {} is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,m)
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M1 . Aseq is Relation-like Function-like set
m . Aseq is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
Aseq is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,m)
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,Aseq,M) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . M,F)
m . M is Element of bool X
(X,F,M1,(X,F,m,Aseq,M)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,M1,(X,F,m,Aseq,M)) is ext-real Element of ExtREAL
Ser (X,F,M1,(X,F,m,Aseq,M)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,M1,(X,F,m,Aseq,M))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,M1,(X,F,m,Aseq,M)))) is ext-real Element of ExtREAL
M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M . Bseq is ext-real Element of ExtREAL
(X,F,m,Aseq,Bseq) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . Bseq,F)
m . Bseq is Element of bool X
(X,F,M1,(X,F,m,Aseq,Bseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,M1,(X,F,m,Aseq,Bseq)) is ext-real Element of ExtREAL
Ser (X,F,M1,(X,F,m,Aseq,Bseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,M1,(X,F,m,Aseq,Bseq))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,M1,(X,F,m,Aseq,Bseq)))) is ext-real Element of ExtREAL
M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Bseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
B is set
M . B is ext-real Element of ExtREAL
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(X,F,m,Aseq,B9) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . B9,F)
m . B9 is Element of bool X
(X,F,M1,(X,F,m,Aseq,B9)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,M1,(X,F,m,Aseq,B9)) is ext-real Element of ExtREAL
Ser (X,F,M1,(X,F,m,Aseq,B9)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,M1,(X,F,m,Aseq,B9))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,M1,(X,F,m,Aseq,B9)))) is ext-real Element of ExtREAL
Bseq . B is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,M1)
(X,F,M1,m,M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(X,F,M1,m,M) . Aseq is ext-real Element of ExtREAL
(X,F,M1,M,Aseq) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . Aseq,F)
M1 . Aseq is Element of bool X
(X,F,m,(X,F,M1,M,Aseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,M1,M,Aseq)) . Bseq is ext-real Element of ExtREAL
(X,F,(X,F,M1,M,Aseq),Bseq) is Element of F
m . (X,F,(X,F,M1,M,Aseq),Bseq) is ext-real Element of ExtREAL
SUM (X,F,m,(X,F,M1,M,Aseq)) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,M1,M,Aseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,M1,M,Aseq))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,M1,M,Aseq)))) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
bool X is non empty Element of bool (bool X)
M1 is Element of bool X
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
Aseq is set
M is set
M is V74() Element of bool ExtREAL
Bseq is ext-real Element of ExtREAL
B is ext-real Element of ExtREAL
B9 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1,F)
(X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,B9) is ext-real Element of ExtREAL
Ser (X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,B9)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,B9))) is ext-real Element of ExtREAL
Aseq is V74() Element of bool ExtREAL
M is V74() Element of bool ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
m is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:m,ExtREAL:] is non empty ext-real-valued set
bool [:m,ExtREAL:] is non empty set
M1 is non empty Relation-like m -defined ExtREAL -valued Function-like V27(m) quasi_total ext-real-valued zeroed nonnegative V102(X,m) Element of bool [:m,ExtREAL:]
F is Element of bool X
(X,m,M1,F) is V74() Element of bool ExtREAL
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
{X,{}} is non empty set
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng Aseq is Element of bool (bool X)
bool (bool X) is non empty set
Aseq . 0 is Element of bool X
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Aseq . M is Element of bool X
union {X,{}} is set
X \/ {} is set
Bseq is set
M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F,m)
(X,m,M1,M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,m,M1,M) is ext-real Element of ExtREAL
Ser (X,m,M1,M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,m,M1,M)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,m,M1,M))) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
bool X is non empty Element of bool (bool X)
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
PairFunc " is Relation-like Function-like set
[:NAT,[:NAT,NAT:]:] is non empty set
bool [:NAT,[:NAT,NAT:]:] is non empty set
() is non empty Relation-like NAT -defined [:NAT,NAT:] -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,[:NAT,NAT:]:]
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng m is Element of bool (bool X)
bool (bool X) is non empty set
union (rng m) is Element of bool X
M1 is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,m)
pr1 () is non empty Relation-like NAT -defined NAT -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty set
pr2 () is non empty Relation-like NAT -defined NAT -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr1 ()) . Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,M1,((pr1 ()) . Aseq)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . ((pr1 ()) . Aseq),F)
m . ((pr1 ()) . Aseq) is Element of bool X
(pr2 ()) . Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,m,M1,((pr1 ()) . Aseq)),((pr2 ()) . Aseq)) is Element of F
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M . Bseq is Element of bool X
(pr1 ()) . Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,M1,((pr1 ()) . Bseq)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . ((pr1 ()) . Bseq),F)
m . ((pr1 ()) . Bseq) is Element of bool X
(pr2 ()) . Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,m,M1,((pr1 ()) . Bseq)),((pr2 ()) . Bseq)) is Element of F
Bseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
rng Bseq is Element of bool (bool X)
union (rng Bseq) is Element of bool X
B is set
B9 is set
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
m . Cseq is Element of bool X
(X,F,m,M1,Cseq) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . Cseq,F)
rng (X,F,m,M1,Cseq) is Element of bool (bool X)
union (rng (X,F,m,M1,Cseq)) is Element of bool X
Cseq is set
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,m,M1,Cseq),Cseq) is Element of F
dom PairFunc is Relation-like NAT -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
rng () is Relation-like NAT -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
[Cseq,Cseq] is set
{Cseq,Cseq} is non empty V73() V74() V75() V76() V77() V78() set
{Cseq} is non empty V73() V74() V75() V76() V77() V78() set
{{Cseq,Cseq},{Cseq}} is non empty set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
() . n is Element of [:NAT,NAT:]
(pr1 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
[((pr1 ()) . n),((pr2 ()) . n)] is set
{((pr1 ()) . n),((pr2 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set
{((pr1 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set
{{((pr1 ()) . n),((pr2 ()) . n)},{((pr1 ()) . n)}} is non empty set
(X,F,Bseq,n) is Element of F
B is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng m),F)
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(X,F,B,B9) is Element of F
(pr1 ()) . B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,M1,((pr1 ()) . B9)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . ((pr1 ()) . B9),F)
m . ((pr1 ()) . B9) is Element of bool X
(pr2 ()) . B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,m,M1,((pr1 ()) . B9)),((pr2 ()) . B9)) is Element of F
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng m),F)
M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng m),F)
Bseq is set
Aseq . Bseq is set
M . Bseq is set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Aseq,B) is Element of F
(pr1 ()) . B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,M1,((pr1 ()) . B)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m . ((pr1 ()) . B),F)
m . ((pr1 ()) . B) is Element of bool X
(pr2 ()) . B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,m,M1,((pr1 ()) . B)),((pr2 ()) . B)) is Element of F
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
NAT --> {} is non empty T-Sequence-like Relation-like NAT -defined {{}} -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,{{}}:]
{{}} is non empty V73() V74() V75() V76() V77() V78() set
[:NAT,{{}}:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,{{}}:] is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr1 ()) . (M + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr2 ()) . (M + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT : (pr1 ()) . (M + 1) = (pr1 ()) . b₁ } is set
Cseq is set
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr1 ()) . Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Cseq + ((pr1 ()) . (M + 1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
n is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
n1 is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,n)
(X,F,n,n1) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng n),F)
rng n is Element of bool (bool X)
bool (bool X) is non empty set
union (rng n) is Element of bool X
(X,F,m,(X,F,n,n1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Partial_Sums (X,F,m,(X,F,n,n1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,m,(X,F,n,n1))) . (M + 1) is ext-real Element of ExtREAL
(X,F,n,m,n1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Partial_Sums (X,F,n,m,n1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,n,m,n1)) . Cseq is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,n,n1,x) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . x,F)
n . x is Element of bool X
k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
k . k is set
(X,F,(X,F,n,n1,x),k) is Element of F
PSv1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
k . PSv1 is set
Aseq is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq . k is set
(X,F,(X,F,n,n1,x),k) is Element of F
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq . k is set
k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
[:NAT,(Funcs (NAT,(bool X))):] is non empty set
bool [:NAT,(Funcs (NAT,(bool X))):] is non empty set
x is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
x . k is Relation-like Function-like Element of Funcs (NAT,(bool X))
M1 . k is Element of bool X
k is Relation-like Function-like set
dom k is set
rng k is set
k is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
PSv1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
k . PSv1 is Element of bool X
(X,F,n,n1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . k,F)
n . k is Element of bool X
(X,F,(X,F,n,n1,k),PSv1) is Element of F
rng k is Element of bool (bool X)
union (rng k) is Element of bool X
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,n,n1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . k,F)
n . k is Element of bool X
k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
PSv1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
k . PSv1 is set
(X,F,(X,F,n,n1,k),PSv1) is Element of F
PSv0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
k . PSv0 is set
Aseq is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq . k is set
(X,F,(X,F,n,n1,k),k) is Element of F
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq . k is set
k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
k is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
k . k is Relation-like Function-like Element of Funcs (NAT,(bool X))
M1 . k is Element of bool X
k is Relation-like Function-like set
dom k is set
rng k is set
PSv1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
PSv0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
PSv1 . PSv0 is Element of bool X
(X,F,n,n1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . k,F)
n . k is Element of bool X
(X,F,(X,F,n,n1,k),PSv0) is Element of F
rng PSv1 is Element of bool (bool X)
union (rng PSv1) is Element of bool X
k is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,M1)
(X,F,M1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng M1),F)
rng M1 is Element of bool (bool X)
union (rng M1) is Element of bool X
(X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Partial_Sums (X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(X,F,(X,F,M1,k),(M + 1)) is Element of F
(X,F,M1,k,((pr1 ()) . (M + 1))) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . (M + 1)),F)
M1 . ((pr1 ()) . (M + 1)) is Element of bool X
(X,F,(X,F,M1,k,((pr1 ()) . (M + 1))),((pr2 ()) . (M + 1))) is Element of F
(X,F,m,(X,F,M1,k)) . (M + 1) is ext-real Element of ExtREAL
m . {} is ext-real Element of ExtREAL
k is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,M1)
(X,F,M1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng M1),F)
(X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Partial_Sums (X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Cseq is non empty V73() V74() V75() V76() V77() V78() Element of bool NAT
SOS is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() Element of Cseq
(pr2 ()) . SOS is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
[:Cseq,NAT:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:Cseq,NAT:] is non empty set
SOS is non empty Relation-like Cseq -defined NAT -valued Function-like V27(Cseq) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:Cseq,NAT:]
(X,F,M1,k,((pr1 ()) . (M + 1))) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . (M + 1)),F)
(X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) * SOS is non empty Relation-like Cseq -defined ExtREAL -valued Function-like V27(Cseq) quasi_total ext-real-valued Element of bool [:Cseq,ExtREAL:]
[:Cseq,ExtREAL:] is non empty ext-real-valued set
bool [:Cseq,ExtREAL:] is non empty set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,M1,k)) . n is ext-real Element of ExtREAL
((X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) * SOS) . n is ext-real Element of ExtREAL
(X,F,(X,F,M1,k),n) is Element of F
m . (X,F,(X,F,M1,k),n) is ext-real Element of ExtREAL
(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
SOS . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,M1,k,((pr1 ()) . (M + 1))),(SOS . n)) is Element of F
m . (X,F,(X,F,M1,k,((pr1 ()) . (M + 1))),(SOS . n)) is ext-real Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr1 ()) . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) . (SOS . n) is ext-real Element of ExtREAL
(pr1 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,M1,k),n) is Element of F
m . (X,F,(X,F,M1,k),n) is ext-real Element of ExtREAL
(X,F,M1,k,((pr1 ()) . n)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . n),F)
M1 . ((pr1 ()) . n) is Element of bool X
(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is Element of F
m . (X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is ext-real Element of ExtREAL
n is set
s is set
SOS . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
SOS . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
() . n is set
(pr1 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
[((pr1 ()) . n),((pr2 ()) . n)] is set
{((pr1 ()) . n),((pr2 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set
{((pr1 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set
{{((pr1 ()) . n),((pr2 ()) . n)},{((pr1 ()) . n)}} is non empty set
() . s is set
(pr1 ()) . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr2 ()) . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
[((pr1 ()) . s),((pr2 ()) . s)] is set
{((pr1 ()) . s),((pr2 ()) . s)} is non empty V73() V74() V75() V76() V77() V78() set
{((pr1 ()) . s)} is non empty V73() V74() V75() V76() V77() V78() set
{{((pr1 ()) . s),((pr2 ()) . s)},{((pr1 ()) . s)}} is non empty set
n2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr1 ()) . n2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
c₂₆ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr1 ()) . c₂₆ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Ser (X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,m,(X,F,M1,k))) . (M + 1) is ext-real Element of ExtREAL
(Ser (X,F,m,(X,F,M1,k))) . M is ext-real Element of ExtREAL
((Ser (X,F,m,(X,F,M1,k))) . M) + ((X,F,m,(X,F,M1,k)) . (M + 1)) is ext-real set
(Partial_Sums (X,F,m,(X,F,M1,k))) . (M + 1) is ext-real Element of ExtREAL
(Partial_Sums (X,F,m,(X,F,M1,k))) . M is ext-real Element of ExtREAL
(X,F,M1,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,m,k) . n is ext-real Element of ExtREAL
(X,F,M1,m,k) . ((pr1 ()) . (M + 1)) is ext-real Element of ExtREAL
Ser (X,F,M1,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,M1,m,k)) . ((pr1 ()) . (M + 1)) is ext-real Element of ExtREAL
SUM (X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1))))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))))) is ext-real Element of ExtREAL
(Ser (X,F,M1,m,k)) . Cseq is ext-real Element of ExtREAL
SUM (X,F,m,(X,F,M1,k)) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,M1,k))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,M1,k)))) is ext-real Element of ExtREAL
(Ser (X,F,m,(X,F,M1,k))) . (M + 1) is ext-real Element of ExtREAL
(Partial_Sums (X,F,m,(X,F,M1,k))) . (M + 1) is ext-real Element of ExtREAL
Partial_Sums (X,F,M1,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,M1,m,k)) . Cseq is ext-real Element of ExtREAL
(X,F,M1,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,m,k) . n is ext-real Element of ExtREAL
Partial_Sums (X,F,M1,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,M1,m,k)) . Cseq is ext-real Element of ExtREAL
(Partial_Sums (X,F,M1,m,k)) . Cseq is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,n,n1)) . n is ext-real Element of ExtREAL
(X,F,m,(X,F,M1,k)) . n is ext-real Element of ExtREAL
(X,F,m,(X,F,M1,k)) . n is ext-real Element of ExtREAL
((X,F,m,(X,F,M1,k)) . n) + ((X,F,m,(X,F,M1,k)) . n) is ext-real set
(pr1 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,(X,F,M1,k),n) is Element of F
m . (X,F,(X,F,M1,k),n) is ext-real Element of ExtREAL
(X,F,(X,F,M1,k),n) is Element of F
m . (X,F,(X,F,M1,k),n) is ext-real Element of ExtREAL
(X,F,(X,F,n,n1),n) is Element of F
m . (X,F,(X,F,n,n1),n) is ext-real Element of ExtREAL
(X,F,n,n1,((pr1 ()) . n)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . ((pr1 ()) . n),F)
n . ((pr1 ()) . n) is Element of bool X
(X,F,(X,F,n,n1,((pr1 ()) . n)),((pr2 ()) . n)) is Element of F
m . (X,F,(X,F,n,n1,((pr1 ()) . n)),((pr2 ()) . n)) is ext-real Element of ExtREAL
(X,F,M1,k,((pr1 ()) . n)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . n),F)
M1 . ((pr1 ()) . n) is Element of bool X
(X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is Element of F
(X,F,M1,k,((pr1 ()) . n)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . n),F)
(X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is Element of F
(X,F,M1,k,((pr1 ()) . n)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . n),F)
M1 . ((pr1 ()) . n) is Element of bool X
(X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is Element of F
(X,F,M1,k,((pr1 ()) . n)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . n),F)
(X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is Element of F
Ser (X,F,m,(X,F,n,n1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,m,(X,F,n,n1))) . (M + 1) is ext-real Element of ExtREAL
((Ser (X,F,m,(X,F,M1,k))) . (M + 1)) + ((Ser (X,F,m,(X,F,M1,k))) . (M + 1)) is ext-real set
((Partial_Sums (X,F,m,(X,F,M1,k))) . (M + 1)) + ((Ser (X,F,m,(X,F,M1,k))) . (M + 1)) is ext-real set
((Partial_Sums (X,F,m,(X,F,M1,k))) . (M + 1)) + ((Partial_Sums (X,F,m,(X,F,M1,k))) . (M + 1)) is ext-real set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,n,m,n1) . n is ext-real Element of ExtREAL
(X,F,M1,m,k) . n is ext-real Element of ExtREAL
(X,F,M1,m,k) . n is ext-real Element of ExtREAL
((X,F,M1,m,k) . n) + ((X,F,M1,m,k) . n) is ext-real set
(X,F,M1,k,n) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . n,F)
M1 . n is Element of bool X
(X,F,m,(X,F,M1,k,n)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,M1,k,n)) . s is ext-real Element of ExtREAL
(X,F,(X,F,M1,k,n),s) is Element of F
m . (X,F,(X,F,M1,k,n),s) is ext-real Element of ExtREAL
SUM (X,F,m,(X,F,M1,k,n)) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,M1,k,n)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,M1,k,n))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,M1,k,n)))) is ext-real Element of ExtREAL
(X,F,M1,k,n) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . n,F)
(X,F,m,(X,F,M1,k,n)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(X,F,n,n1,n) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . n,F)
n . n is Element of bool X
(X,F,m,(X,F,n,n1,n)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,M1,k,n)) . s is ext-real Element of ExtREAL
(X,F,m,(X,F,n,n1,n)) . s is ext-real Element of ExtREAL
(X,F,(X,F,M1,k,n),s) is Element of F
m . (X,F,(X,F,M1,k,n),s) is ext-real Element of ExtREAL
(X,F,(X,F,n,n1,n),s) is Element of F
m . (X,F,(X,F,n,n1,n),s) is ext-real Element of ExtREAL
SUM (X,F,m,(X,F,M1,k,n)) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,M1,k,n)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,M1,k,n))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,M1,k,n)))) is ext-real Element of ExtREAL
SUM (X,F,m,(X,F,n,n1,n)) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,n,n1,n)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,n,n1,n))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,n,n1,n)))) is ext-real Element of ExtREAL
(SUM (X,F,m,(X,F,M1,k,n))) + (SUM (X,F,m,(X,F,M1,k,n))) is ext-real set
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,M1,k,n)) . s is ext-real Element of ExtREAL
(X,F,(X,F,M1,k,n),s) is Element of F
m . (X,F,(X,F,M1,k,n),s) is ext-real Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,n,n1,n)) . s is ext-real Element of ExtREAL
(X,F,m,(X,F,M1,k,n)) . s is ext-real Element of ExtREAL
(X,F,(X,F,M1,k,n),s) is Element of F
m . (X,F,(X,F,M1,k,n),s) is ext-real Element of ExtREAL
(X,F,(X,F,n,n1,n),s) is Element of F
m . (X,F,(X,F,n,n1,n),s) is ext-real Element of ExtREAL
Ser (X,F,n,m,n1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,n,m,n1)) . Cseq is ext-real Element of ExtREAL
Ser (X,F,M1,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,M1,m,k)) . Cseq is ext-real Element of ExtREAL
((Ser (X,F,M1,m,k)) . Cseq) + ((Ser (X,F,M1,m,k)) . Cseq) is ext-real set
((Partial_Sums (X,F,M1,m,k)) . Cseq) + ((Ser (X,F,M1,m,k)) . Cseq) is ext-real set
((Partial_Sums (X,F,M1,m,k)) . Cseq) + ((Partial_Sums (X,F,M1,m,k)) . Cseq) is ext-real set
(pr1 ()) . 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Bseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
B is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,Bseq)
(X,F,Bseq,B) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng Bseq),F)
rng Bseq is Element of bool (bool X)
bool (bool X) is non empty set
union (rng Bseq) is Element of bool X
(X,F,m,(X,F,Bseq,B)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Partial_Sums (X,F,m,(X,F,Bseq,B)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,m,(X,F,Bseq,B))) . 0 is ext-real Element of ExtREAL
(X,F,Bseq,m,B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Partial_Sums (X,F,Bseq,m,B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,Bseq,m,B)) . M is ext-real Element of ExtREAL
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Bseq,m,B) . B9 is ext-real Element of ExtREAL
(X,F,Bseq,m,B) . M is ext-real Element of ExtREAL
Ser (X,F,Bseq,m,B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,Bseq,m,B)) . M is ext-real Element of ExtREAL
(X,F,m,(X,F,Bseq,B)) . 0 is ext-real Element of ExtREAL
(X,F,(X,F,Bseq,B),0) is Element of F
m . (X,F,(X,F,Bseq,B),0) is ext-real Element of ExtREAL
(X,F,Bseq,B,((pr1 ()) . 0)) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Bseq . ((pr1 ()) . 0),F)
Bseq . ((pr1 ()) . 0) is Element of bool X
(X,F,m,(X,F,Bseq,B,((pr1 ()) . 0))) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(pr2 ()) . 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,(X,F,Bseq,B,((pr1 ()) . 0))) . ((pr2 ()) . 0) is ext-real Element of ExtREAL
(X,F,(X,F,Bseq,B,((pr1 ()) . 0)),((pr2 ()) . 0)) is Element of F
m . (X,F,(X,F,Bseq,B,((pr1 ()) . 0)),((pr2 ()) . 0)) is ext-real Element of ExtREAL
SUM (X,F,m,(X,F,Bseq,B,((pr1 ()) . 0))) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,Bseq,B,((pr1 ()) . 0))) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,Bseq,B,((pr1 ()) . 0)))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,Bseq,B,((pr1 ()) . 0))))) is ext-real Element of ExtREAL
(X,F,Bseq,m,B) . ((pr1 ()) . 0) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng M1 is Element of bool (bool X)
bool (bool X) is non empty set
union (rng M1) is Element of bool X
(X,F,m,(union (rng M1))) is non empty V74() Element of bool ExtREAL
inf (X,F,m,(union (rng M1))) is ext-real Element of ExtREAL
Aseq is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,M1)
(X,F,M1,m,Aseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,M1,m,Aseq) is ext-real Element of ExtREAL
Ser (X,F,M1,m,Aseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,M1,m,Aseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,M1,m,Aseq))) is ext-real Element of ExtREAL
(X,F,M1,Aseq) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng M1),F)
(X,F,m,(X,F,M1,Aseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,(X,F,M1,Aseq)) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,M1,Aseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,M1,Aseq))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,M1,Aseq)))) is ext-real Element of ExtREAL
Bseq is ext-real set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser (X,F,m,(X,F,M1,Aseq))) . B is ext-real Element of ExtREAL
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(Ser (X,F,M1,m,Aseq)) . B9 is ext-real Element of ExtREAL
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Cseq is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,Cseq)
(X,F,Cseq,Cseq) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng Cseq),F)
rng Cseq is Element of bool (bool X)
union (rng Cseq) is Element of bool X
(X,F,m,(X,F,Cseq,Cseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (X,F,m,(X,F,Cseq,Cseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,m,(X,F,Cseq,Cseq))) . B is ext-real Element of ExtREAL
(X,F,Cseq,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (X,F,Cseq,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (X,F,Cseq,m,Cseq)) . B9 is ext-real Element of ExtREAL
Partial_Sums (X,F,m,(X,F,Cseq,Cseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,m,(X,F,Cseq,Cseq))) . B is ext-real Element of ExtREAL
Partial_Sums (X,F,Cseq,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Partial_Sums (X,F,Cseq,m,Cseq)) . B9 is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
{} X is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V73() V74() V75() V76() V77() V78() V79() Element of bool X
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
m is Element of bool X
(m,({} X)) followed_by ({} X) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 . 0 is Element of bool X
M1 . 1 is Element of bool X
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M1 . Aseq is Element of bool X
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
rng Aseq is Element of bool (bool X)
bool (bool X) is non empty set
union (rng Aseq) is Element of bool X
M is set
dom Aseq is V73() V74() V75() V76() V77() V78() Element of bool NAT
(X,F,Aseq,0) is Element of F
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
bool X is non empty Element of bool (bool X)
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
M1 is set
(X,F,m) . M1 is ext-real Element of ExtREAL
m . M1 is ext-real Element of ExtREAL
Aseq is Element of bool X
{} X is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V73() V74() V75() V76() V77() V78() V79() Element of bool X
(Aseq,({} X)) followed_by ({} X) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
(X,F,M,1) is Element of F
(X,F,M,0) is Element of F
rng M is Element of bool (bool X)
bool (bool X) is non empty set
union (rng M) is Element of bool X
Bseq is set
dom M is V73() V74() V75() V76() V77() V78() Element of bool NAT
Bseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Aseq,F)
(X,F,m,Bseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,Bseq) . B is ext-real Element of ExtREAL
(X,F,Bseq,B) is Element of F
m . {} is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,m,Bseq) . B is ext-real Element of ExtREAL
SUM (X,F,m,Bseq) is ext-real Element of ExtREAL
Ser (X,F,m,Bseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,Bseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,Bseq))) is ext-real Element of ExtREAL
(Ser (X,F,m,Bseq)) . 1 is ext-real Element of ExtREAL
(X,F,m,Bseq) . 0 is ext-real Element of ExtREAL
(X,F,Bseq,0) is Element of F
m . (X,F,Bseq,0) is ext-real Element of ExtREAL
m . Aseq is ext-real Element of ExtREAL
(X,F,m,Aseq) is non empty V74() Element of bool ExtREAL
(X,F,m) . Aseq is ext-real Element of ExtREAL
inf (X,F,m,Aseq) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
bool X is non empty Element of bool (bool X)
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
rng (X,F,m) is V74() Element of bool ExtREAL
M1 is ext-real set
Aseq is set
(X,F,m) . Aseq is ext-real Element of ExtREAL
Bseq is ext-real set
M is Element of bool X
(X,F,m,M) is non empty V74() Element of bool ExtREAL
B is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M,F)
(X,F,m,B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,B) is ext-real Element of ExtREAL
Ser (X,F,m,B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,B)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,B))) is ext-real Element of ExtREAL
inf (X,F,m,M) is ext-real Element of ExtREAL
M1 is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
bool X is non empty Element of bool (bool X)
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
(X,F,m) . {} is ext-real Element of ExtREAL
m . {} is ext-real Element of ExtREAL
{} X is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V73() V74() V75() V76() V77() V78() V79() Element of bool X
dom (X,F,m) is Element of bool (bool X)
bool (bool X) is non empty set
rng (X,F,m) is V74() Element of bool ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
bool X is non empty Element of bool (bool X)
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
M1 is Element of bool X
(X,F,m) . M1 is ext-real Element of ExtREAL
Aseq is Element of bool X
(X,F,m) . Aseq is ext-real Element of ExtREAL
M is set
(X,F,m,Aseq) is non empty V74() Element of bool ExtREAL
Bseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Aseq,F)
(X,F,m,Bseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,Bseq) is ext-real Element of ExtREAL
Ser (X,F,m,Bseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,Bseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,Bseq))) is ext-real Element of ExtREAL
rng Bseq is Element of bool (bool X)
bool (bool X) is non empty set
union (rng Bseq) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1,F)
(X,F,m,B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,B) is ext-real Element of ExtREAL
Ser (X,F,m,B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,B)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,B))) is ext-real Element of ExtREAL
(X,F,m,M1) is non empty V74() Element of bool ExtREAL
inf (X,F,m,M1) is ext-real Element of ExtREAL
inf (X,F,m,Aseq) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng M1 is Element of bool (bool X)
bool (bool X) is non empty set
union (rng M1) is Element of bool X
(X,F,m) . (union (rng M1)) is ext-real Element of ExtREAL
(X,F,m) * M1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM ((X,F,m) * M1) is ext-real Element of ExtREAL
Ser ((X,F,m) * M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser ((X,F,m) * M1)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser ((X,F,m) * M1))) is ext-real Element of ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M1 . Aseq is Element of bool X
(X,F,m) . (M1 . Aseq) is ext-real Element of ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M1 . Aseq is Element of bool X
(X,F,m) . (M1 . Aseq) is ext-real Element of ExtREAL
dom M1 is V73() V74() V75() V76() V77() V78() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
((X,F,m) * M1) . M is ext-real Element of ExtREAL
M1 . M is Element of bool X
(X,F,m) . (M1 . M) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng M1 is Element of bool (bool X)
bool (bool X) is non empty set
union (rng M1) is Element of bool X
(X,F,m) . (union (rng M1)) is ext-real Element of ExtREAL
(X,F,m) * M1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM ((X,F,m) * M1) is ext-real Element of ExtREAL
Ser ((X,F,m) * M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser ((X,F,m) * M1)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser ((X,F,m) * M1))) is ext-real Element of ExtREAL
{+infty} is non empty V74() set
(X,F,m,(union (rng M1))) is non empty V74() Element of bool ExtREAL
inf (X,F,m,(union (rng M1))) is ext-real Element of ExtREAL
(Ser ((X,F,m) * M1)) . 0 is ext-real Element of ExtREAL
((X,F,m) * M1) . 0 is ext-real Element of ExtREAL
Bseq is ext-real V56() real set
(sup (rng (Ser ((X,F,m) * M1)))) + Bseq is ext-real set
B is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM B is ext-real Element of ExtREAL
Ser B is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser B) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser B)) is ext-real Element of ExtREAL
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
B . B9 is ext-real Element of ExtREAL
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . B9 is Element of bool X
(X,F,m,(M1 . B9)) is non empty V74() Element of bool ExtREAL
inf (X,F,m,(M1 . B9)) is ext-real Element of ExtREAL
B . B9 is ext-real Element of ExtREAL
(inf (X,F,m,(M1 . B9))) + (B . B9) is ext-real set
(X,F,m) . (M1 . B9) is ext-real Element of ExtREAL
(X,F,m,(M1 . B9)) \ {+infty} is V74() Element of bool ExtREAL
Cseq is set
Cseq is ext-real Element of ExtREAL
Cseq is ext-real set
n is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . B9,F)
(X,F,m,n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,n) is ext-real Element of ExtREAL
Ser (X,F,m,n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,n)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,n))) is ext-real Element of ExtREAL
n1 is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))
[:NAT,(Funcs (NAT,(bool X))):] is non empty set
bool [:NAT,(Funcs (NAT,(bool X))):] is non empty set
B9 is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
B9 . Cseq is Relation-like Function-like Element of Funcs (NAT,(bool X))
M1 . Cseq is Element of bool X
(X,F,m,(M1 . Cseq)) is non empty V74() Element of bool ExtREAL
inf (X,F,m,(M1 . Cseq)) is ext-real Element of ExtREAL
B . Cseq is ext-real Element of ExtREAL
(inf (X,F,m,(M1 . Cseq))) + (B . Cseq) is ext-real set
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . Cseq,F)
(X,F,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,Cseq) is ext-real Element of ExtREAL
Ser (X,F,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,Cseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,Cseq))) is ext-real Element of ExtREAL
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
((X,F,m) * M1) . Cseq is ext-real Element of ExtREAL
B . Cseq is ext-real Element of ExtREAL
(((X,F,m) * M1) . Cseq) + (B . Cseq) is ext-real set
Cseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Cseq is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,M1)
(X,F,M1,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,m,Cseq) . Cseq is ext-real Element of ExtREAL
Cseq . Cseq is ext-real Element of ExtREAL
M1 . Cseq is Element of bool X
(X,F,M1,Cseq,Cseq) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . Cseq,F)
(X,F,m,(M1 . Cseq)) is non empty V74() Element of bool ExtREAL
inf (X,F,m,(M1 . Cseq)) is ext-real Element of ExtREAL
B . Cseq is ext-real Element of ExtREAL
(inf (X,F,m,(M1 . Cseq))) + (B . Cseq) is ext-real set
((X,F,m) * M1) . Cseq is ext-real Element of ExtREAL
(X,F,m) . (M1 . Cseq) is ext-real Element of ExtREAL
(((X,F,m) * M1) . Cseq) + (B . Cseq) is ext-real set
(X,F,m,(X,F,M1,Cseq,Cseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,(X,F,M1,Cseq,Cseq)) is ext-real Element of ExtREAL
Ser (X,F,m,(X,F,M1,Cseq,Cseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,(X,F,M1,Cseq,Cseq))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,(X,F,M1,Cseq,Cseq)))) is ext-real Element of ExtREAL
n is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . Cseq,F)
(X,F,m,n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,n) is ext-real Element of ExtREAL
Ser (X,F,m,n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,n)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,n))) is ext-real Element of ExtREAL
SUM (X,F,M1,m,Cseq) is ext-real Element of ExtREAL
Ser (X,F,M1,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,M1,m,Cseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,M1,m,Cseq))) is ext-real Element of ExtREAL
SUM Cseq is ext-real Element of ExtREAL
Ser Cseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser Cseq) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser Cseq)) is ext-real Element of ExtREAL
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Cseq . Cseq is ext-real Element of ExtREAL
((X,F,m) * M1) . Cseq is ext-real Element of ExtREAL
B . Cseq is ext-real Element of ExtREAL
(((X,F,m) * M1) . Cseq) + (B . Cseq) is ext-real set
(SUM ((X,F,m) * M1)) + (SUM B) is ext-real set
(SUM ((X,F,m) * M1)) + Bseq is ext-real set
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Aseq is Element of bool X
(X,F,m,(M1 . Aseq)) is non empty V74() Element of bool ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Aseq is Element of bool X
(X,F,m,(M1 . Aseq)) is non empty V74() Element of bool ExtREAL
inf {+infty} is ext-real Element of ExtREAL
(X,F,m) . (M1 . Aseq) is ext-real Element of ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Aseq is Element of bool X
(X,F,m,(M1 . Aseq)) is non empty V74() Element of bool ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
(X,F,m) . {} is ext-real Element of ExtREAL
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
M1 is Element of bool X
Aseq is Element of bool X
(X,F,m) . M1 is ext-real Element of ExtREAL
(X,F,m) . Aseq is ext-real Element of ExtREAL
M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng M is Element of bool (bool X)
bool (bool X) is non empty set
union (rng M) is Element of bool X
(X,F,m) . (union (rng M)) is ext-real Element of ExtREAL
(X,F,m) * M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM ((X,F,m) * M) is ext-real Element of ExtREAL
Ser ((X,F,m) * M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser ((X,F,m) * M)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser ((X,F,m) * M))) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued Element of bool [:(bool X),ExtREAL:]
bool X is non empty Element of bool (bool X)
[:(bool X),ExtREAL:] is non empty ext-real-valued set
bool [:(bool X),ExtREAL:] is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
Partial_Union m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(Partial_Union m) . M1 is Element of bool X
M1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Union m) . (M1 + 1) is Element of bool X
(X,F,m,(M1 + 1)) is Element of F
((Partial_Union m) . M1) \/ (X,F,m,(M1 + 1)) is Element of bool X
(Partial_Union m) . 0 is Element of bool X
(X,F,m,0) is Element of F
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
Partial_Diff_Union m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(Partial_Diff_Union m) . M1 is Element of bool X
M1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Diff_Union m) . (M1 + 1) is Element of bool X
Partial_Union m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
(Partial_Union m) . M1 is Element of bool X
(X,F,m,(M1 + 1)) is Element of F
(X,F,m,(M1 + 1)) \ ((Partial_Union m) . M1) is Element of bool X
(Partial_Diff_Union m) . 0 is Element of bool X
(X,F,m,0) is Element of F
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:NAT,F:] is non empty set
bool [:NAT,F:] is non empty set
m is Element of bool X
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,m,F)
Partial_Diff_Union M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Bseq is set
M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng M is Element of bool (bool X)
bool (bool X) is non empty set
B is set
M . B is set
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M . B9 is Element of bool X
(Partial_Diff_Union M1) . B9 is Element of bool X
((Partial_Diff_Union M1) . B9) /\ m is Element of bool X
Bseq is non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,F:]
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Bseq . B is Element of F
Bseq . B9 is Element of F
(Partial_Diff_Union M1) . B9 is Element of bool X
((Partial_Diff_Union M1) . B9) /\ m is Element of bool X
(Partial_Diff_Union M1) . B is Element of bool X
((Partial_Diff_Union M1) . B) /\ m is Element of bool X
B9 is set
rng M1 is Element of bool (bool X)
union (rng M1) is Element of bool X
Union M1 is Element of bool X
Union (Partial_Diff_Union M1) is Element of bool X
rng (Partial_Diff_Union M1) is Element of bool (bool X)
union (rng (Partial_Diff_Union M1)) is Element of bool X
Cseq is set
Cseq is set
(Partial_Diff_Union M1) . Cseq is set
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Diff_Union M1) . Cseq is Element of bool X
((Partial_Diff_Union M1) . Cseq) /\ m is Element of bool X
B is non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,F:]
B . Cseq is Element of F
rng B is Element of bool F
bool F is non empty set
union (rng B) is set
B9 is set
Cseq is set
Cseq is set
B . Cseq is set
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Diff_Union M1) . Cseq is Element of bool X
((Partial_Diff_Union M1) . Cseq) /\ m is Element of bool X
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
B . B9 is Element of F
(Partial_Diff_Union M1) . B9 is Element of bool X
((Partial_Diff_Union M1) . B9) /\ m is Element of bool X
(X,F,M1,B9) is Element of F
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued C_Measure of X
bool X is non empty Element of bool (bool X)
M1 is set
m . M1 is ext-real Element of ExtREAL
(X,F,m) . M1 is ext-real Element of ExtREAL
Aseq is Element of bool X
(X,F,m,Aseq) is non empty V74() Element of bool ExtREAL
M is ext-real set
Bseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Aseq,F)
(X,F,m,Bseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,Bseq) is ext-real Element of ExtREAL
Ser (X,F,m,Bseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,Bseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,Bseq))) is ext-real Element of ExtREAL
[:NAT,F:] is non empty set
bool [:NAT,F:] is non empty set
B is non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,F:]
rng B is Element of bool F
bool F is non empty set
union (rng B) is set
m * B is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(m * B) . B9 is ext-real Element of ExtREAL
(X,F,m,Bseq) . B9 is ext-real Element of ExtREAL
B . B9 is Element of F
m . (B . B9) is ext-real Element of ExtREAL
(X,F,Bseq,B9) is Element of F
m . (X,F,Bseq,B9) is ext-real Element of ExtREAL
SUM (m * B) is ext-real Element of ExtREAL
Ser (m * B) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (m * B)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (m * B))) is ext-real Element of ExtREAL
inf (X,F,m,Aseq) is ext-real Element of ExtREAL
(X,F,m) . Aseq is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
F is Element of bool X
X \ F is Element of bool X
m is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued C_Measure of X
sigma_Field m is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
M1 is Element of bool X
Aseq is Element of bool X
m . M1 is ext-real Element of ExtREAL
m . Aseq is ext-real Element of ExtREAL
(m . M1) + (m . Aseq) is ext-real set
M1 \/ Aseq is Element of bool X
m . (M1 \/ Aseq) is ext-real Element of ExtREAL
(M1 \/ Aseq) /\ (X \ F) is Element of bool X
(M1 \/ Aseq) /\ X is Element of bool X
((M1 \/ Aseq) /\ X) \ F is Element of bool X
X /\ M1 is Element of bool X
X /\ Aseq is Element of bool X
(X /\ M1) \/ (X /\ Aseq) is Element of bool X
((X /\ M1) \/ (X /\ Aseq)) \ F is Element of bool X
M1 \/ (X /\ Aseq) is Element of bool X
(M1 \/ (X /\ Aseq)) \ F is Element of bool X
(M1 \/ Aseq) \ F is Element of bool X
M1 \ F is Element of bool X
Aseq \ F is Element of bool X
(M1 \ F) \/ (Aseq \ F) is Element of bool X
{} \/ (Aseq \ F) is set
{} \/ Aseq is set
(M1 \/ Aseq) /\ F is Element of bool X
F /\ M1 is Element of bool X
F /\ Aseq is Element of bool X
(F /\ M1) \/ (F /\ Aseq) is Element of bool X
M1 \/ (F /\ Aseq) is Element of bool X
M1 \/ {} is set
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued C_Measure of X
bool X is non empty Element of bool (bool X)
sigma_Field (X,F,m) is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
Aseq is set
M is Element of bool X
X \ M is Element of bool X
Bseq is Element of bool X
Bseq /\ M is Element of bool X
(X,F,m) . (Bseq /\ M) is ext-real Element of ExtREAL
Bseq /\ (X \ M) is Element of bool X
(X,F,m) . (Bseq /\ (X \ M)) is ext-real Element of ExtREAL
((X,F,m) . (Bseq /\ M)) + ((X,F,m) . (Bseq /\ (X \ M))) is ext-real set
(X,F,m) . Bseq is ext-real Element of ExtREAL
B9 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Bseq,F)
(X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,B9) is ext-real Element of ExtREAL
Ser (X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,B9)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,B9))) is ext-real Element of ExtREAL
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Cseq . Cseq is Element of bool X
(X,F,B9,Cseq) is Element of F
(X,F,B9,Cseq) /\ Aseq is Element of bool X
n is set
rng B9 is Element of bool (bool X)
bool (bool X) is non empty set
union (rng B9) is Element of bool X
n1 is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,B9,x) is Element of F
n is set
n1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,B9,n1) is Element of F
(X,F,B9,n1) /\ Aseq is Element of bool X
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
(X,F,Cseq,n1) is Element of F
rng Cseq is Element of bool (bool X)
bool (bool X) is non empty set
union (rng Cseq) is Element of bool X
X \ Aseq is Element of bool X
n1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
x is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
x . k is Element of bool X
(X,F,B9,k) is Element of F
(X,F,B9,k) /\ (X \ Aseq) is Element of bool X
k is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,B9,k) is Element of F
(X,F,B9,k) /\ (X \ Aseq) is Element of bool X
k is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
(X,F,k,k) is Element of F
rng k is Element of bool (bool X)
union (rng k) is Element of bool X
n is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Bseq /\ M,F)
(X,F,m,n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
k is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Bseq /\ (X \ M),F)
(X,F,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(X,F,m,B9) . k is ext-real Element of ExtREAL
(X,F,m,n) . k is ext-real Element of ExtREAL
(X,F,m,k) . k is ext-real Element of ExtREAL
((X,F,m,n) . k) + ((X,F,m,k) . k) is ext-real set
(X,F,B9,k) is Element of F
m . (X,F,B9,k) is ext-real Element of ExtREAL
(X,F,n,k) is Element of F
m . (X,F,n,k) is ext-real Element of ExtREAL
(X,F,k,k) is Element of F
m . (X,F,k,k) is ext-real Element of ExtREAL
(X,F,B9,k) /\ Aseq is Element of bool X
(X,F,B9,k) /\ (X \ Aseq) is Element of bool X
(X,F,n,k) \/ (X,F,k,k) is Element of F
Aseq \/ (X \ Aseq) is set
(X,F,B9,k) /\ (Aseq \/ (X \ Aseq)) is Element of bool X
Aseq \/ X is set
(X,F,B9,k) /\ (Aseq \/ X) is Element of bool X
(X,F,B9,k) /\ X is Element of bool X
(X,F,m,(Bseq /\ (X \ M))) is non empty V74() Element of bool ExtREAL
inf (X,F,m,(Bseq /\ (X \ M))) is ext-real Element of ExtREAL
SUM (X,F,m,k) is ext-real Element of ExtREAL
Ser (X,F,m,k) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,k)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,k))) is ext-real Element of ExtREAL
(X,F,m,(Bseq /\ M)) is non empty V74() Element of bool ExtREAL
inf (X,F,m,(Bseq /\ M)) is ext-real Element of ExtREAL
SUM (X,F,m,n) is ext-real Element of ExtREAL
Ser (X,F,m,n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,n)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,n))) is ext-real Element of ExtREAL
(SUM (X,F,m,n)) + (SUM (X,F,m,k)) is ext-real set
(X,F,m,Bseq) is non empty V74() Element of bool ExtREAL
B9 is ext-real set
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,Bseq,F)
(X,F,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,Cseq) is ext-real Element of ExtREAL
Ser (X,F,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,Cseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,Cseq))) is ext-real Element of ExtREAL
inf (X,F,m,Bseq) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
M1 is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued Element of bool [:F,ExtREAL:]
M1 * m is Relation-like NAT -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:NAT,ExtREAL:]
Aseq is set
rng m is Element of bool (bool X)
bool (bool X) is non empty set
M is set
m . M is set
dom M1 is Element of bool F
bool F is non empty set
dom (M1 * m) is V73() V74() V75() V76() V77() V78() Element of bool NAT
dom m is V73() V74() V75() V76() V77() V78() Element of bool NAT
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
M1 is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued Element of bool [:F,ExtREAL:]
m * M1 is Relation-like Function-like ext-real-valued set
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like NAT -defined bool X -valued F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued Element of bool [:F,ExtREAL:]
M1 * m is Relation-like NAT -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:NAT,ExtREAL:]
rng m is Element of bool F
bool F is non empty set
dom M1 is Element of bool F
dom (M1 * m) is V73() V74() V75() V76() V77() V78() Element of bool NAT
dom m is V73() V74() V75() V76() V77() V78() Element of bool NAT
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like NAT -defined F -valued bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued Element of bool [:F,ExtREAL:]
m * M1 is Relation-like Function-like ext-real-valued set
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(Ser X) . m is ext-real Element of ExtREAL
(Ser F) . m is ext-real Element of ExtREAL
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(Ser X) . M1 is ext-real Element of ExtREAL
(Ser F) . M1 is ext-real Element of ExtREAL
M1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser X) . (M1 + 1) is ext-real Element of ExtREAL
(Ser F) . (M1 + 1) is ext-real Element of ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
X . Aseq is ext-real Element of ExtREAL
F . Aseq is ext-real Element of ExtREAL
X . (M1 + 1) is ext-real Element of ExtREAL
F . (M1 + 1) is ext-real Element of ExtREAL
((Ser X) . M1) + (X . (M1 + 1)) is ext-real set
((Ser F) . M1) + (F . (M1 + 1)) is ext-real set
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
X . Aseq is ext-real Element of ExtREAL
F . Aseq is ext-real Element of ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
X . Aseq is ext-real Element of ExtREAL
F . Aseq is ext-real Element of ExtREAL
(Ser X) . 0 is ext-real Element of ExtREAL
X . 0 is ext-real Element of ExtREAL
(Ser F) . 0 is ext-real Element of ExtREAL
F . 0 is ext-real Element of ExtREAL
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
X . M1 is ext-real Element of ExtREAL
F . M1 is ext-real Element of ExtREAL
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
F is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued C_Measure of X
sigma_Field F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:NAT,(sigma_Field F):] is non empty set
bool [:NAT,(sigma_Field F):] is non empty set
m is non empty Relation-like NAT -defined sigma_Field F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(sigma_Field F):]
rng m is non empty Element of bool (bool X)
union (rng m) is Element of bool X
F . (union (rng m)) is ext-real Element of ExtREAL
F * m is Relation-like NAT -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:NAT,ExtREAL:]
Sum (F * m) is ext-real Element of ExtREAL
Partial_Sums (F * m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (Partial_Sums (F * m)) is ext-real Element of ExtREAL
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
X \ (union (rng m)) is Element of bool X
Aseq is Element of bool X
Aseq (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * (Aseq (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (F * (Aseq (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Aseq /\ (X \ (union (rng m))) is Element of bool X
F . (Aseq /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
F . Aseq is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser (F * (Aseq (/\) M1))) . M is ext-real Element of ExtREAL
((Ser (F * (Aseq (/\) M1))) . M) + (F . (Aseq /\ (X \ (union (rng m))))) is ext-real set
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Bseq + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
B is Element of bool X
M1 . (Bseq + 1) is Element of bool X
X \ (M1 . (Bseq + 1)) is Element of bool X
B /\ (X \ (M1 . (Bseq + 1))) is Element of bool X
(B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * ((B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (F * ((B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (F * ((B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1))) . Bseq is ext-real Element of ExtREAL
(B /\ (X \ (M1 . (Bseq + 1)))) /\ (X \ (union (rng m))) is Element of bool X
F . ((B /\ (X \ (M1 . (Bseq + 1)))) /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
((Ser (F * ((B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1))) . Bseq) + (F . ((B /\ (X \ (M1 . (Bseq + 1)))) /\ (X \ (union (rng m))))) is ext-real set
F . (B /\ (X \ (M1 . (Bseq + 1)))) is ext-real Element of ExtREAL
B (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * (B (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(F * (B (/\) M1)) . B9 is ext-real Element of ExtREAL
(F * ((B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1)) . B9 is ext-real Element of ExtREAL
M1 . B9 is Element of bool X
(M1 . B9) /\ (X \ (M1 . (Bseq + 1))) is Element of bool X
((B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1) . B9 is Element of bool X
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Cseq is Element of bool X
(B /\ (X \ (M1 . (Bseq + 1)))) /\ (M1 . Cseq) is Element of bool X
B /\ ((M1 . B9) /\ (X \ (M1 . (Bseq + 1)))) is Element of bool X
(B (/\) M1) . Cseq is Element of bool X
(F * ((B /\ (X \ (M1 . (Bseq + 1)))) (/\) M1)) . Cseq is ext-real Element of ExtREAL
F . ((B (/\) M1) . Cseq) is ext-real Element of ExtREAL
Ser (F * (B (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (F * (B (/\) M1))) . Bseq is ext-real Element of ExtREAL
(X \ (M1 . (Bseq + 1))) /\ (X \ (union (rng m))) is Element of bool X
B /\ (X \ (union (rng m))) is Element of bool X
F . (B /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
((Ser (F * (B (/\) M1))) . Bseq) + (F . (B /\ (X \ (union (rng m))))) is ext-real set
B is Element of bool X
B (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * (B (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (F * (B (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (F * (B (/\) M1))) . (Bseq + 1) is ext-real Element of ExtREAL
B /\ (X \ (union (rng m))) is Element of bool X
F . (B /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
((Ser (F * (B (/\) M1))) . (Bseq + 1)) + (F . (B /\ (X \ (union (rng m))))) is ext-real set
F . B is ext-real Element of ExtREAL
B /\ (X \ (M1 . (Bseq + 1))) is Element of bool X
B /\ X is Element of bool X
(B /\ X) \ (M1 . (Bseq + 1)) is Element of bool X
B \ (M1 . (Bseq + 1)) is Element of bool X
(Ser (F * (B (/\) M1))) . Bseq is ext-real Element of ExtREAL
((Ser (F * (B (/\) M1))) . Bseq) + (F . (B /\ (X \ (union (rng m))))) is ext-real set
F . (B \ (M1 . (Bseq + 1))) is ext-real Element of ExtREAL
B \/ (B \ (M1 . (Bseq + 1))) is Element of bool X
B /\ (M1 . (Bseq + 1)) is Element of bool X
F . (B /\ (M1 . (Bseq + 1))) is ext-real Element of ExtREAL
(F . (B /\ (M1 . (Bseq + 1)))) + (F . (B \ (M1 . (Bseq + 1)))) is ext-real set
(B /\ (M1 . (Bseq + 1))) \/ (B \ (M1 . (Bseq + 1))) is Element of bool X
F . ((B /\ (M1 . (Bseq + 1))) \/ (B \ (M1 . (Bseq + 1)))) is ext-real Element of ExtREAL
(M1 . (Bseq + 1)) \/ (B \ (M1 . (Bseq + 1))) is Element of bool X
(B \/ (B \ (M1 . (Bseq + 1)))) /\ ((M1 . (Bseq + 1)) \/ (B \ (M1 . (Bseq + 1)))) is Element of bool X
F . ((B \/ (B \ (M1 . (Bseq + 1)))) /\ ((M1 . (Bseq + 1)) \/ (B \ (M1 . (Bseq + 1))))) is ext-real Element of ExtREAL
(M1 . (Bseq + 1)) \/ B is Element of bool X
(B \/ (B \ (M1 . (Bseq + 1)))) /\ ((M1 . (Bseq + 1)) \/ B) is Element of bool X
F . ((B \/ (B \ (M1 . (Bseq + 1)))) /\ ((M1 . (Bseq + 1)) \/ B)) is ext-real Element of ExtREAL
(((Ser (F * (B (/\) M1))) . Bseq) + (F . (B /\ (X \ (union (rng m)))))) + (F . (B /\ (M1 . (Bseq + 1)))) is ext-real set
((Ser (F * (B (/\) M1))) . Bseq) + (F . (B /\ (M1 . (Bseq + 1)))) is ext-real set
(B (/\) M1) . (Bseq + 1) is Element of bool X
F . ((B (/\) M1) . (Bseq + 1)) is ext-real Element of ExtREAL
((Ser (F * (B (/\) M1))) . Bseq) + (F . ((B (/\) M1) . (Bseq + 1))) is ext-real set
(F * (B (/\) M1)) . (Bseq + 1) is ext-real Element of ExtREAL
((Ser (F * (B (/\) M1))) . Bseq) + ((F * (B (/\) M1)) . (Bseq + 1)) is ext-real set
(F * (B (/\) M1)) . Bseq is ext-real Element of ExtREAL
-infty is non empty ext-real non positive negative non real Element of ExtREAL
m . 0 is Element of sigma_Field F
Bseq is Element of bool X
M1 . 0 is Element of bool X
Bseq /\ (M1 . 0) is Element of bool X
X \ (M1 . 0) is Element of bool X
Bseq /\ (X \ (M1 . 0)) is Element of bool X
F . (Bseq /\ (M1 . 0)) is ext-real Element of ExtREAL
F . (Bseq /\ (X \ (M1 . 0))) is ext-real Element of ExtREAL
(F . (Bseq /\ (M1 . 0))) + (F . (Bseq /\ (X \ (M1 . 0)))) is ext-real set
(Bseq /\ (M1 . 0)) \/ (Bseq /\ (X \ (M1 . 0))) is Element of bool X
F . ((Bseq /\ (M1 . 0)) \/ (Bseq /\ (X \ (M1 . 0)))) is ext-real Element of ExtREAL
Bseq /\ X is Element of bool X
(Bseq /\ X) \ (M1 . 0) is Element of bool X
(Bseq /\ (M1 . 0)) \/ ((Bseq /\ X) \ (M1 . 0)) is Element of bool X
F . ((Bseq /\ (M1 . 0)) \/ ((Bseq /\ X) \ (M1 . 0))) is ext-real Element of ExtREAL
Bseq \ (M1 . 0) is Element of bool X
(Bseq /\ (M1 . 0)) \/ (Bseq \ (M1 . 0)) is Element of bool X
F . ((Bseq /\ (M1 . 0)) \/ (Bseq \ (M1 . 0))) is ext-real Element of ExtREAL
F . Bseq is ext-real Element of ExtREAL
Union M1 is Element of bool X
X \ (m . 0) is Element of bool X
Bseq /\ (X \ (union (rng m))) is Element of bool X
Bseq /\ (X \ (m . 0)) is Element of bool X
F . (Bseq /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
F . (Bseq /\ (X \ (m . 0))) is ext-real Element of ExtREAL
Bseq (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * (Bseq (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (F * (Bseq (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (F * (Bseq (/\) M1))) . 0 is ext-real Element of ExtREAL
(F * (Bseq (/\) M1)) . 0 is ext-real Element of ExtREAL
(Bseq (/\) M1) . 0 is Element of bool X
F . ((Bseq (/\) M1) . 0) is ext-real Element of ExtREAL
((Ser (F * (Bseq (/\) M1))) . 0) + (F . (Bseq /\ (X \ (union (rng m))))) is ext-real set
Bseq is Element of bool X
Bseq (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * (Bseq (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (F * (Bseq (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(Ser (F * (Bseq (/\) M1))) . 0 is ext-real Element of ExtREAL
Bseq /\ (X \ (union (rng m))) is Element of bool X
F . (Bseq /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
((Ser (F * (Bseq (/\) M1))) . 0) + (F . (Bseq /\ (X \ (union (rng m))))) is ext-real set
F . Bseq is ext-real Element of ExtREAL
Union M1 is Element of bool X
Aseq is Element of bool X
Aseq (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * (Aseq (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (F * (Aseq (/\) M1)) is ext-real Element of ExtREAL
Ser (F * (Aseq (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (F * (Aseq (/\) M1))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (F * (Aseq (/\) M1)))) is ext-real Element of ExtREAL
Aseq /\ (X \ (union (rng m))) is Element of bool X
F . (Aseq /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
(SUM (F * (Aseq (/\) M1))) + (F . (Aseq /\ (X \ (union (rng m))))) is ext-real set
F . Aseq is ext-real Element of ExtREAL
Aseq /\ (Union M1) is Element of bool X
F . (Aseq /\ (Union M1)) is ext-real Element of ExtREAL
-infty is non empty ext-real non positive negative non real Element of ExtREAL
(F . Aseq) - (F . (Aseq /\ (X \ (union (rng m))))) is ext-real set
M is ext-real set
Bseq is set
(Ser (F * (Aseq (/\) M1))) . Bseq is ext-real Element of ExtREAL
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(F * (Aseq (/\) M1)) . B is ext-real Element of ExtREAL
(Ser (F * (Aseq (/\) M1))) . B is ext-real Element of ExtREAL
((Ser (F * (Aseq (/\) M1))) . B) + (F . (Aseq /\ (X \ (union (rng m))))) is ext-real set
rng (Aseq (/\) M1) is Element of bool (bool X)
bool (bool X) is non empty set
union (rng (Aseq (/\) M1)) is Element of bool X
F . (union (rng (Aseq (/\) M1))) is ext-real Element of ExtREAL
Union (Aseq (/\) M1) is Element of bool X
F . (Union (Aseq (/\) M1)) is ext-real Element of ExtREAL
(union (rng m)) /\ (Union M1) is Element of bool X
F . ((union (rng m)) /\ (Union M1)) is ext-real Element of ExtREAL
(union (rng m)) (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * ((union (rng m)) (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (F * ((union (rng m)) (/\) M1)) is ext-real Element of ExtREAL
Ser (F * ((union (rng m)) (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (F * ((union (rng m)) (/\) M1))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (F * ((union (rng m)) (/\) M1)))) is ext-real Element of ExtREAL
X \ (Union M1) is Element of bool X
Aseq is Element of bool X
M is Element of bool X
F . Aseq is ext-real Element of ExtREAL
F . M is ext-real Element of ExtREAL
(F . Aseq) + (F . M) is ext-real set
Aseq \/ M is Element of bool X
F . (Aseq \/ M) is ext-real Element of ExtREAL
(Aseq \/ M) /\ (X \ (Union M1)) is Element of bool X
Aseq /\ (X \ (Union M1)) is Element of bool X
M \/ (Aseq /\ (X \ (Union M1))) is Element of bool X
(X \ (Union M1)) /\ (Union M1) is Element of bool X
(Union M1) /\ (X \ (Union M1)) is Element of bool X
(Aseq \/ M) /\ (X \ (union (rng m))) is Element of bool X
F . ((Aseq \/ M) /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
M /\ (Union M1) is Element of bool X
(Aseq \/ M) /\ (Union M1) is Element of bool X
Aseq \/ (M /\ (Union M1)) is Element of bool X
(Aseq \/ M) (/\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
F * ((Aseq \/ M) (/\) M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (F * ((Aseq \/ M) (/\) M1)) is ext-real Element of ExtREAL
Ser (F * ((Aseq \/ M) (/\) M1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (F * ((Aseq \/ M) (/\) M1))) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (F * ((Aseq \/ M) (/\) M1)))) is ext-real Element of ExtREAL
(SUM (F * ((Aseq \/ M) (/\) M1))) + (F . ((Aseq \/ M) /\ (X \ (union (rng m))))) is ext-real set
F * M1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (F * M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(union (rng m)) /\ (X \ (union (rng m))) is Element of bool X
F . ((union (rng m)) /\ (X \ (union (rng m)))) is ext-real Element of ExtREAL
M is set
((union (rng m)) (/\) M1) . M is set
m . M is set
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Bseq is Element of bool X
(union (rng m)) /\ (M1 . Bseq) is Element of bool X
sup (Ser (F * M1)) is ext-real Element of ExtREAL
rng (Ser (F * M1)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (F * M1))) is ext-real Element of ExtREAL
dom (Ser (F * M1)) is V73() V74() V75() V76() V77() V78() Element of bool NAT
M is ext-real set
Bseq is ext-real set
(Ser (F * M1)) . M is ext-real Element of ExtREAL
(Ser (F * M1)) . Bseq is ext-real Element of ExtREAL
lim (Ser (F * M1)) is ext-real Element of ExtREAL
Partial_Sums (F * M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (Partial_Sums (F * M1)) is ext-real Element of ExtREAL
(SUM (F * ((union (rng m)) (/\) M1))) + (F . ((union (rng m)) /\ (X \ (union (rng m))))) is ext-real set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued C_Measure of X
sigma_Field F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
m is non empty Relation-like NAT -defined bool X -valued sigma_Field F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Union m is Element of bool X
Partial_Diff_Union m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(bool X):]
rng (Partial_Diff_Union m) is Element of bool (bool X)
bool (bool X) is non empty set
[:NAT,(sigma_Field F):] is non empty set
bool [:NAT,(sigma_Field F):] is non empty set
Aseq is non empty Relation-like NAT -defined sigma_Field F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(sigma_Field F):]
M is non empty Relation-like NAT -defined sigma_Field F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(sigma_Field F):]
rng M is non empty Element of bool (bool X)
union (rng M) is Element of bool X
Union (Partial_Diff_Union m) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
(X,F,M1,m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (X,F,M1,m) is ext-real Element of ExtREAL
lim_sup M1 is Element of bool X
m . (lim_sup M1) is ext-real Element of ExtREAL
Partial_Union M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Partial_Diff_Union M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(bool X):]
rng (Partial_Diff_Union M1) is Element of bool F
bool F is non empty set
[:NAT,F:] is non empty set
bool [:NAT,F:] is non empty set
Aseq is non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,F:]
m * Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Ser (m * Aseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(X,F,(Partial_Union M1),m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
M is set
(Ser (m * Aseq)) . M is ext-real Element of ExtREAL
(X,F,(Partial_Union M1),m) . M is ext-real Element of ExtREAL
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser (m * Aseq)) . Bseq is ext-real Element of ExtREAL
(X,F,(Partial_Union M1),m) . Bseq is ext-real Element of ExtREAL
Bseq + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser (m * Aseq)) . (Bseq + 1) is ext-real Element of ExtREAL
(X,F,(Partial_Union M1),m) . (Bseq + 1) is ext-real Element of ExtREAL
Partial_Union (Partial_Diff_Union M1) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
(Partial_Union (Partial_Diff_Union M1)) . Bseq is M7(X,F)
(Partial_Union M1) . Bseq is M7(X,F)
(Partial_Diff_Union M1) . (Bseq + 1) is M7(X,F)
M1 . (Bseq + 1) is M7(X,F)
(M1 . (Bseq + 1)) \ ((Partial_Union M1) . Bseq) is M7(X,F)
(m * Aseq) . (Bseq + 1) is ext-real Element of ExtREAL
((Ser (m * Aseq)) . Bseq) + ((m * Aseq) . (Bseq + 1)) is ext-real set
m . ((Partial_Diff_Union M1) . (Bseq + 1)) is ext-real Element of ExtREAL
((X,F,(Partial_Union M1),m) . Bseq) + (m . ((Partial_Diff_Union M1) . (Bseq + 1))) is ext-real set
m . ((Partial_Union M1) . Bseq) is ext-real Element of ExtREAL
(m . ((Partial_Union M1) . Bseq)) + (m . ((Partial_Diff_Union M1) . (Bseq + 1))) is ext-real set
m . ((Partial_Union (Partial_Diff_Union M1)) . Bseq) is ext-real Element of ExtREAL
(m . ((Partial_Union (Partial_Diff_Union M1)) . Bseq)) + (m . ((Partial_Diff_Union M1) . (Bseq + 1))) is ext-real set
((Partial_Union (Partial_Diff_Union M1)) . Bseq) \/ ((Partial_Diff_Union M1) . (Bseq + 1)) is M7(X,F)
m . (((Partial_Union (Partial_Diff_Union M1)) . Bseq) \/ ((Partial_Diff_Union M1) . (Bseq + 1))) is ext-real Element of ExtREAL
(Partial_Union (Partial_Diff_Union M1)) . (Bseq + 1) is M7(X,F)
m . ((Partial_Union (Partial_Diff_Union M1)) . (Bseq + 1)) is ext-real Element of ExtREAL
(Partial_Union M1) . (Bseq + 1) is M7(X,F)
m . ((Partial_Union M1) . (Bseq + 1)) is ext-real Element of ExtREAL
(Ser (m * Aseq)) . 0 is ext-real Element of ExtREAL
(m * Aseq) . 0 is ext-real Element of ExtREAL
(Partial_Diff_Union M1) . 0 is M7(X,F)
m . ((Partial_Diff_Union M1) . 0) is ext-real Element of ExtREAL
M1 . 0 is M7(X,F)
m . (M1 . 0) is ext-real Element of ExtREAL
(Partial_Union M1) . 0 is M7(X,F)
m . ((Partial_Union M1) . 0) is ext-real Element of ExtREAL
(X,F,(Partial_Union M1),m) . 0 is ext-real Element of ExtREAL
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Ser (m * Aseq)) . Bseq is ext-real Element of ExtREAL
(X,F,(Partial_Union M1),m) . Bseq is ext-real Element of ExtREAL
M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
dom M is V73() V74() V75() V76() V77() V78() Element of bool NAT
Bseq is ext-real set
B is ext-real set
M . Bseq is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
SUM (m * Aseq) is ext-real Element of ExtREAL
rng (Ser (m * Aseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (m * Aseq))) is ext-real Element of ExtREAL
rng Aseq is non empty Element of bool (bool X)
union (rng Aseq) is Element of bool X
m . (union (rng Aseq)) is ext-real Element of ExtREAL
lim M is ext-real Element of ExtREAL
sup M is ext-real Element of ExtREAL
rng M is non empty V45() V74() Element of bool ExtREAL
sup (rng M) is ext-real Element of ExtREAL
Partial_Union (Partial_Diff_Union M1) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Union M1 is Element of bool X
Union (Partial_Diff_Union M1) is Element of bool X
m . (Union M1) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
(X,F,M1,m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
dom (X,F,M1,m) is V73() V74() V75() V76() V77() V78() Element of bool NAT
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,Aseq) is Element of F
(X,F,M1,M) is Element of F
(X,F,M1,m) . Aseq is ext-real Element of ExtREAL
m . (X,F,M1,Aseq) is ext-real Element of ExtREAL
(X,F,M1,m) . M is ext-real Element of ExtREAL
m . (X,F,M1,M) is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,m) . M is ext-real Element of ExtREAL
(X,F,M1,m) . Aseq is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
(X,F,M1,m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
dom (X,F,M1,m) is V73() V74() V75() V76() V77() V78() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,Aseq) is Element of F
(X,F,M1,M) is Element of F
(X,F,M1,m) . Aseq is ext-real Element of ExtREAL
m . (X,F,M1,Aseq) is ext-real Element of ExtREAL
(X,F,M1,m) . M is ext-real Element of ExtREAL
m . (X,F,M1,M) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
(X,F,M1,m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
dom (X,F,M1,m) is V73() V74() V75() V76() V77() V78() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,m) . M is ext-real Element of ExtREAL
M1 . M is M7(X,F)
m . (M1 . M) is ext-real Element of ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Aseq is M7(X,F)
rng M1 is Element of bool F
bool F is non empty set
(X,F,M1,m) . Aseq is ext-real Element of ExtREAL
m . (M1 . Aseq) is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,m) . M is ext-real Element of ExtREAL
(X,F,M1,m) . Aseq is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
(X,F,M1,m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
dom (X,F,M1,m) is V73() V74() V75() V76() V77() V78() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,M1,m) . M is ext-real Element of ExtREAL
M1 . M is M7(X,F)
m . (M1 . M) is ext-real Element of ExtREAL
Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Aseq is M7(X,F)
rng M1 is Element of bool F
bool F is non empty set
(X,F,M1,m) . Aseq is ext-real Element of ExtREAL
m . (M1 . Aseq) is ext-real Element of ExtREAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like NAT -defined bool X -valued F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
M1 . 0 is M7(X,F)
m . (M1 . 0) is ext-real Element of ExtREAL
(X,F,M1,m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (X,F,M1,m) is ext-real Element of ExtREAL
lim_sup M1 is Element of bool X
m . (lim_sup M1) is ext-real Element of ExtREAL
(M1 . 0) \ (lim_sup M1) is Element of bool X
m . ((M1 . 0) \ (lim_sup M1)) is ext-real Element of ExtREAL
Aseq is set
(M1 . 0) (\) M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng ((M1 . 0) (\) M1) is Element of bool (bool X)
bool (bool X) is non empty set
M is set
((M1 . 0) (\) M1) . M is set
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . Bseq is M7(X,F)
(M1 . 0) \ (M1 . Bseq) is M7(X,F)
(X,F,M1,m) . 0 is ext-real Element of ExtREAL
M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
M1 . B is M7(X,F)
Aseq is non empty Relation-like NAT -defined bool X -valued F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Aseq . B is M7(X,F)
M1 . Bseq is Element of bool X
(M1 . 0) \ (M1 . Bseq) is Element of bool X
(M1 . Bseq) \/ ((M1 . 0) \ (M1 . Bseq)) is Element of bool X
(M1 . 0) \/ (M1 . Bseq) is Element of bool X
Aseq . Bseq is Element of bool X
(M1 . Bseq) \/ (Aseq . Bseq) is Element of bool X
m . (M1 . Bseq) is ext-real Element of ExtREAL
m . (Aseq . Bseq) is ext-real Element of ExtREAL
(m . (M1 . Bseq)) + (m . (Aseq . Bseq)) is ext-real set
M . Bseq is ext-real Element of ExtREAL
(X,F,M1,m) . Bseq is ext-real Element of ExtREAL
((X,F,M1,m) . Bseq) + (m . (Aseq . Bseq)) is ext-real set
(X,F,Aseq,m) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(X,F,Aseq,m) . Bseq is ext-real Element of ExtREAL
((X,F,M1,m) . Bseq) + ((X,F,Aseq,m) . Bseq) is ext-real set
rng Aseq is Element of bool F
bool F is non empty set
[:NAT,F:] is non empty set
bool [:NAT,F:] is non empty set
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
M . Bseq is ext-real Element of ExtREAL
rng M1 is Element of bool F
-infty is non empty ext-real non positive negative non real Element of ExtREAL
inferior_setsequence M1 is non empty Relation-like NAT -defined F -valued bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(inferior_setsequence M1) . (0 + 1) is M7(X,F)
Intersection M1 is Element of bool X
(M1 . 0) \/ (lim_sup M1) is Element of bool X
((M1 . 0) \ (lim_sup M1)) \/ (lim_sup M1) is Element of bool X
m . (((M1 . 0) \ (lim_sup M1)) \/ (lim_sup M1)) is ext-real Element of ExtREAL
(m . ((M1 . 0) \ (lim_sup M1))) + (m . (lim_sup M1)) is ext-real set
m . ((M1 . 0) \/ (lim_sup M1)) is ext-real Element of ExtREAL
Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Aseq . Bseq is M7(X,F)
Aseq . B is M7(X,F)
M1 . B is M7(X,F)
M1 . Bseq is M7(X,F)
(M1 . 0) \ (M1 . Bseq) is M7(X,F)
(M1 . 0) \ (M1 . B) is M7(X,F)
lim M is ext-real Element of ExtREAL
lim (X,F,Aseq,m) is ext-real Element of ExtREAL
(lim (X,F,Aseq,m)) + (lim (X,F,M1,m)) is ext-real set
lim_sup Aseq is Element of bool X
m . (lim_sup Aseq) is ext-real Element of ExtREAL
(lim (X,F,M1,m)) + (m . ((M1 . 0) \ (lim_sup M1))) is ext-real set
((lim (X,F,M1,m)) + (m . ((M1 . 0) \ (lim_sup M1)))) - (m . ((M1 . 0) \ (lim_sup M1))) is ext-real set
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:m,ExtREAL:] is non empty ext-real-valued set
bool [:m,ExtREAL:] is non empty set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
sigma F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:(sigma F),ExtREAL:] is non empty ext-real-valued set
bool [:(sigma F),ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is non empty Relation-like sigma F -defined ExtREAL -valued Function-like V27( sigma F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:(sigma F),ExtREAL:]
[:NAT,F:] is non empty set
bool [:NAT,F:] is non empty set
Aseq is non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,F:]
rng Aseq is Element of bool F
bool F is non empty set
union (rng Aseq) is set
m * Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (m * Aseq) is ext-real Element of ExtREAL
Ser (m * Aseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (m * Aseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (m * Aseq))) is ext-real Element of ExtREAL
m . (union (rng Aseq)) is ext-real Element of ExtREAL
[:NAT,(sigma F):] is non empty set
bool [:NAT,(sigma F):] is non empty set
M is non empty Relation-like NAT -defined sigma F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(sigma F):]
B is set
Bseq is non empty Relation-like NAT -defined sigma F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(sigma F):]
M1 * Bseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(M1 * Bseq) . B is ext-real Element of ExtREAL
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Bseq . B9 is Element of sigma F
M1 . (Bseq . B9) is ext-real Element of ExtREAL
Aseq . B9 is Element of F
m . (Aseq . B9) is ext-real Element of ExtREAL
(m * Aseq) . B is ext-real Element of ExtREAL
M1 . (union (rng Aseq)) is ext-real Element of ExtREAL
SUM (M1 * Bseq) is ext-real Element of ExtREAL
Ser (M1 * Bseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (M1 * Bseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (M1 * Bseq))) is ext-real Element of ExtREAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
sigma F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:(sigma F),ExtREAL:] is non empty ext-real-valued set
bool [:(sigma F),ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued C_Measure of X
bool X is non empty Element of bool (bool X)
sigma_Field (X,F,m) is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
sigma_Meas (X,F,m) is non empty Relation-like sigma_Field (X,F,m) -defined ExtREAL -valued Function-like V27( sigma_Field (X,F,m)) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:(sigma_Field (X,F,m)),ExtREAL:]
[:(sigma_Field (X,F,m)),ExtREAL:] is non empty ext-real-valued set
bool [:(sigma_Field (X,F,m)),ExtREAL:] is non empty set
(sigma_Meas (X,F,m)) | (sigma F) is Relation-like sigma_Field (X,F,m) -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:(sigma_Field (X,F,m)),ExtREAL:]
[:NAT,(sigma F):] is non empty set
bool [:NAT,(sigma F):] is non empty set
Aseq is non empty Relation-like sigma F -defined ExtREAL -valued Function-like V27( sigma F) quasi_total ext-real-valued Element of bool [:(sigma F),ExtREAL:]
M is non empty Relation-like NAT -defined sigma F -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(sigma F):]
Aseq * M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (Aseq * M) is ext-real Element of ExtREAL
Ser (Aseq * M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (Aseq * M)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (Aseq * M))) is ext-real Element of ExtREAL
rng M is non empty Element of bool (bool X)
union (rng M) is Element of bool X
Aseq . (union (rng M)) is ext-real Element of ExtREAL
[:NAT,(sigma_Field (X,F,m)):] is non empty set
bool [:NAT,(sigma_Field (X,F,m)):] is non empty set
(sigma F) |` M is Relation-like NAT -defined sigma F -valued Function-like Element of bool [:NAT,(sigma F):]
(sigma_Meas (X,F,m)) * ((sigma F) |` M) is Relation-like NAT -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:NAT,ExtREAL:]
Bseq is non empty Relation-like NAT -defined sigma_Field (X,F,m) -valued Function-like V27( NAT ) quasi_total disjoint_valued Element of bool [:NAT,(sigma_Field (X,F,m)):]
(sigma_Meas (X,F,m)) * Bseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng Bseq is non empty Element of bool (bool X)
union (rng Bseq) is Element of bool X
(sigma_Meas (X,F,m)) . (union (rng Bseq)) is ext-real Element of ExtREAL
Aseq . {} is ext-real Element of ExtREAL
(sigma_Meas (X,F,m)) . {} is ext-real Element of ExtREAL
M is non empty Relation-like sigma F -defined ExtREAL -valued Function-like V27( sigma F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:(sigma F),ExtREAL:]
Bseq is set
M . Bseq is ext-real Element of ExtREAL
m . Bseq is ext-real Element of ExtREAL
(sigma_Meas (X,F,m)) . Bseq is ext-real Element of ExtREAL
B is Element of bool X
(X,F,m) . B is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
Partial_Union Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
(Partial_Union Aseq) . M1 is Element of bool X
m . ((Partial_Union Aseq) . M1) is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
(Partial_Union Aseq) . M is Element of bool X
m . ((Partial_Union Aseq) . M) is ext-real Element of ExtREAL
M + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Aseq,(M + 1)) is Element of F
m . (X,F,Aseq,(M + 1)) is ext-real Element of ExtREAL
(m . ((Partial_Union Aseq) . M)) + (m . (X,F,Aseq,(M + 1))) is ext-real set
(Partial_Union Aseq) . (M + 1) is Element of bool X
((Partial_Union Aseq) . M) \/ (X,F,Aseq,(M + 1)) is Element of bool X
m . ((Partial_Union Aseq) . (M + 1)) is ext-real Element of ExtREAL
(Partial_Union Aseq) . 0 is Element of bool X
(X,F,Aseq,0) is Element of F
m . ((Partial_Union Aseq) . 0) is ext-real Element of ExtREAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
F is non empty compl-closed V84() V85() V86() Element of bool (bool X)
[:F,ExtREAL:] is non empty ext-real-valued set
bool [:F,ExtREAL:] is non empty set
sigma F is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
[:(sigma F),ExtREAL:] is non empty ext-real-valued set
bool [:(sigma F),ExtREAL:] is non empty set
m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]
(X,F,m) is non empty Relation-like bool X -defined ExtREAL -valued Function-like V27( bool X) quasi_total ext-real-valued C_Measure of X
sigma_Field (X,F,m) is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool X)
sigma_Meas (X,F,m) is non empty Relation-like sigma_Field (X,F,m) -defined ExtREAL -valued Function-like V27( sigma_Field (X,F,m)) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:(sigma_Field (X,F,m)),ExtREAL:]
[:(sigma_Field (X,F,m)),ExtREAL:] is non empty ext-real-valued set
bool [:(sigma_Field (X,F,m)),ExtREAL:] is non empty set
(sigma_Meas (X,F,m)) | (sigma F) is Relation-like sigma_Field (X,F,m) -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:(sigma_Field (X,F,m)),ExtREAL:]
M1 is non empty Relation-like sigma F -defined ExtREAL -valued Function-like V27( sigma F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:(sigma F),ExtREAL:]
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
rng Aseq is Element of bool (bool X)
bool (bool X) is non empty set
union (rng Aseq) is Element of bool X
Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
rng Aseq is Element of bool (bool X)
bool (bool X) is non empty set
union (rng Aseq) is Element of bool X
M is non empty Relation-like sigma F -defined ExtREAL -valued Function-like V27( sigma F) quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:(sigma F),ExtREAL:]
Partial_Union Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
B is Element of bool X
M . B is ext-real Element of ExtREAL
M1 . B is ext-real Element of ExtREAL
B9 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,B,F)
(X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,B9) is ext-real Element of ExtREAL
Ser (X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,B9)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,B9))) is ext-real Element of ExtREAL
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,B9,Cseq) is Element of F
Cseq is set
rng B9 is Element of bool (bool X)
Cseq is set
B9 . Cseq is set
Cseq is non empty Relation-like NAT -defined bool X -valued sigma F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
rng Cseq is Element of bool (sigma F)
bool (sigma F) is non empty set
[:NAT,(sigma F):] is non empty set
bool [:NAT,(sigma F):] is non empty set
union (rng Cseq) is set
Union Cseq is Element of bool X
M . (Union Cseq) is ext-real Element of ExtREAL
Cseq is non empty Relation-like NAT -defined sigma F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(sigma F):]
M * Cseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
Cseq is set
(M * Cseq) . Cseq is ext-real Element of ExtREAL
(X,F,m,B9) . Cseq is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
dom Cseq is V73() V74() V75() V76() V77() V78() Element of bool NAT
Cseq . n is Element of sigma F
M . (Cseq . n) is ext-real Element of ExtREAL
(X,F,B9,n) is Element of F
m . (X,F,B9,n) is ext-real Element of ExtREAL
SUM (M * Cseq) is ext-real Element of ExtREAL
Ser (M * Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (M * Cseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (M * Cseq))) is ext-real Element of ExtREAL
rng Cseq is non empty Element of bool (bool X)
union (rng Cseq) is Element of bool X
M . (union (rng Cseq)) is ext-real Element of ExtREAL
(X,F,m,B) is non empty V74() Element of bool ExtREAL
B9 is ext-real set
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,B,F)
(X,F,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (X,F,m,Cseq) is ext-real Element of ExtREAL
Ser (X,F,m,Cseq) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser (X,F,m,Cseq)) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser (X,F,m,Cseq))) is ext-real Element of ExtREAL
inf (X,F,m,B) is ext-real Element of ExtREAL
(X,F,m) . B is ext-real Element of ExtREAL
(sigma_Meas (X,F,m)) . B is ext-real Element of ExtREAL
Bseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)
B is set
M . B is ext-real Element of ExtREAL
M1 . B is ext-real Element of ExtREAL
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Bseq,B9) is Element of F
B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Bseq,B9) is Element of F
M . (X,F,Bseq,B9) is ext-real Element of ExtREAL
m . (X,F,Bseq,B9) is ext-real Element of ExtREAL
(X,F,Bseq,B9) \ B is Element of bool X
M . ((X,F,Bseq,B9) \ B) is ext-real Element of ExtREAL
(M . B) + (M . ((X,F,Bseq,B9) \ B)) is ext-real set
B \/ ((X,F,Bseq,B9) \ B) is set
M . (B \/ ((X,F,Bseq,B9) \ B)) is ext-real Element of ExtREAL
(X,F,Bseq,B9) \/ B is set
M . ((X,F,Bseq,B9) \/ B) is ext-real Element of ExtREAL
(M . (X,F,Bseq,B9)) - (M . ((X,F,Bseq,B9) \ B)) is ext-real set
M1 . (X,F,Bseq,B9) is ext-real Element of ExtREAL
M1 . ((X,F,Bseq,B9) \ B) is ext-real Element of ExtREAL
(M1 . B) + (M1 . ((X,F,Bseq,B9) \ B)) is ext-real set
M1 . (B \/ ((X,F,Bseq,B9) \ B)) is ext-real Element of ExtREAL
M1 . ((X,F,Bseq,B9) \/ B) is ext-real Element of ExtREAL
(M1 . (X,F,Bseq,B9)) - (M1 . ((X,F,Bseq,B9) \ B)) is ext-real set
Cseq is Element of bool X
M . Cseq is ext-real Element of ExtREAL
M1 . Cseq is ext-real Element of ExtREAL
B is set
M . B is ext-real Element of ExtREAL
M1 . B is ext-real Element of ExtREAL
Cseq is set
Bseq . Cseq is set
B /\ (Bseq . Cseq) is set
(Bseq . Cseq) /\ B is set
X /\ X is set
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Cseq . Cseq is Element of bool X
Cseq . n is Element of bool X
(X,F,Bseq,Cseq) is Element of F
(X,F,Bseq,n) is Element of F
B /\ (X,F,Bseq,Cseq) is Element of bool X
B /\ (X,F,Bseq,n) is Element of bool X
Cseq is set
rng Cseq is Element of bool (bool X)
n is set
Cseq . n is set
n1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Bseq,n1) is Element of F
(X,F,Bseq,n1) /\ B is Element of bool X
Cseq is non empty Relation-like NAT -defined bool X -valued sigma F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Partial_Union Cseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
(X,(sigma F),(Partial_Union Cseq),M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
(X,(sigma F),(Partial_Union Cseq),M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
n is set
(X,(sigma F),(Partial_Union Cseq),M1) . n is ext-real Element of ExtREAL
(X,(sigma F),(Partial_Union Cseq),M) . n is ext-real Element of ExtREAL
x is set
n1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Union Cseq) . n1 is Element of bool X
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set
Cseq . k is Element of bool X
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Bseq,k) is Element of F
B /\ (X,F,Bseq,k) is Element of bool X
(X,F,Bseq,n1) is Element of F
x is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
(X,F,Bseq,k) is Element of F
M1 . ((Partial_Union Cseq) . n1) is ext-real Element of ExtREAL
rng (Partial_Union Cseq) is Element of bool (bool X)
dom (Partial_Union Cseq) is V73() V74() V75() V76() V77() V78() Element of bool NAT
M . ((Partial_Union Cseq) . n1) is ext-real Element of ExtREAL
B9 is Element of bool X
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT
Cseq . n is M7(X, sigma F)
(X,F,Bseq,n) is Element of F
B9 /\ (X,F,Bseq,n) is Element of bool X
B9 (/\) Bseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]
Union Cseq is Element of bool X
Union Bseq is Element of bool X
B9 /\ (Union Bseq) is Element of bool X
Union Aseq is Element of bool X
B9 /\ (Union Aseq) is Element of bool X
B9 /\ X is Element of bool X
lim_sup Cseq is Element of bool X
(X,(sigma F),Cseq,M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (X,(sigma F),Cseq,M1) is ext-real Element of ExtREAL
lim (X,(sigma F),(Partial_Union Cseq),M) is ext-real Element of ExtREAL
(X,(sigma F),Cseq,M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]
lim (X,(sigma F),Cseq,M) is ext-real Element of ExtREAL
M . (lim_sup Cseq) is ext-real Element of ExtREAL