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
{ b1 where b1 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 ()) . b1 } 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
c26 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 ()) . c26 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,