:: 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

bool is non empty set
bool ExtREAL is non empty set
bool REAL is non empty Element of bool ()
bool () is non empty set
[:NAT,():] is non empty set
bool [:NAT,():] is non empty set
Funcs (NAT,()) is non empty functional FUNCTION_DOMAIN of NAT , bool REAL
[:NAT,(Funcs (NAT,())):] is non empty set
bool [:NAT,(Funcs (NAT,())):] 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

bool 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

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,():] is non empty set
bool [:NAT,():] is non empty set
is non empty ext-real-valued set
bool is non empty set
K464() is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool ()
is non empty ext-real-valued set
bool is non empty set

bool is non empty set

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

+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

F is set
(Ser X) . F is ext-real Element of ExtREAL
() . F is ext-real Element of ExtREAL

(Ser X) . m is ext-real Element of ExtREAL
() . 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
() . (m + 1) is ext-real Element of ExtREAL
X . (m + 1) is ext-real Element of ExtREAL
(() . m) + (X . (m + 1)) is ext-real set
(Ser X) . 0 is ext-real Element of ExtREAL

() . m is ext-real Element of ExtREAL

rng (Ser X) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser X)) is ext-real Element of ExtREAL

rng () is non empty V45() V74() Element of bool ExtREAL
sup (rng ()) is ext-real Element of ExtREAL

rng (Ser X) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser X)) is ext-real Element of 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 X) + (Sum F) is ext-real set

rng (Ser m) is non empty V45() V74() Element of bool ExtREAL
sup (rng (Ser 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 . 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

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

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

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

bool is non empty set

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)

dom m is V73() V74() V75() V76() V77() V78() Element of bool NAT

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)

dom m is V73() V74() V75() V76() V77() V78() Element of bool NAT

m . M1 is Element of bool X

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)

{X} is non empty set
is non empty set
bool is non empty 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

{X} is non empty set
is non empty set
bool is non empty 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 . M1 is set
X is set
bool X is non empty set
bool (bool X) is non empty set

{X} is non empty set
is non empty set
bool 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 () is Element of bool {X}
bool {X} is non empty 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

F is non empty compl-closed V84() V85() V86() Element of bool (bool X)

{X} is non empty set
is non empty set
bool is non empty set
M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)

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 () is Element of bool {X}
bool {X} is non empty set
union (rng ()) is 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)
is non empty ext-real-valued set
bool is non empty set
bool X is non empty Element of bool (bool X)

M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,F)

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

Bseq is set
Aseq . Bseq is ext-real Element of ExtREAL

(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)
is non empty ext-real-valued set
bool 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 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

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)

M1 is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,m)

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)
is non empty ext-real-valued set
bool is non empty set
Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X

Aseq is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total (X,F,m)

(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
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
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 . 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
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
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

B is set
M . B is ext-real Element of ExtREAL

(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
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
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)
is non empty ext-real-valued set
bool is non empty 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) . 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
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
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)
is non empty ext-real-valued set
bool is non empty set
bool X is non empty Element of bool (bool X)
M1 is Element of bool X

Aseq is set
M is set
M is V74() Element of bool ExtREAL
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,M1,F)

SUM (X,F,m,B9) is ext-real Element of 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)
is non empty ext-real-valued set
bool is non empty set

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

rng Aseq is Element of bool (bool X)
bool (bool X) is non empty set
Aseq . 0 is Element of bool X

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)

SUM (X,m,M1,M) is ext-real Element of 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)
is non empty ext-real-valued set
bool 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

is non empty set
bool 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
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)

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)

bool is non empty 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
(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

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

[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 Element of
(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)

(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

(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)
is non empty ext-real-valued set
bool is non empty set

is non empty V73() V74() V75() V76() V77() V78() set

bool is non empty set

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 + ((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

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
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
(Partial_Sums (X,F,m,(X,F,n,n1))) . (M + 1) is ext-real Element of ExtREAL

(Partial_Sums (X,F,n,m,n1)) . Cseq is ext-real Element of ExtREAL

(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 . 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 . k is set
(X,F,(X,F,n,n1,x),k) is Element of F

Aseq . k is set

[: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))):]

x . k is Relation-like Function-like Element of Funcs (NAT,(bool X))
M1 . k is Element of bool X

dom k is set
rng k is 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

(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

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 . k is set
(X,F,(X,F,n,n1,k),k) is Element of F

Aseq . k is set

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 . k is Relation-like Function-like Element of Funcs (NAT,(bool X))
M1 . k is Element of bool X

dom k is set
rng k is 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
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
(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

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
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
Cseq is non empty V73() V74() V75() V76() V77() V78() Element of bool NAT

(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

bool [:Cseq,NAT:] is non empty set

(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
(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

(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

(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
(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) . 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)) . ((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
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
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)) . Cseq is ext-real Element of ExtREAL

(X,F,M1,m,k) . n is ext-real Element of 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

(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
(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

(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

(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
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
(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

(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
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
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,