:: MEASURE8 semantic presentation

REAL is non empty V34() V73() V74() V75() V79() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() Element of bool REAL

bool REAL is non empty set

ExtREAL is non empty V74() set

[:NAT,ExtREAL:] is non empty ext-real-valued set

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

bool ExtREAL is non empty set

bool REAL is non empty Element of bool (bool REAL)

bool (bool REAL) is non empty set

[:NAT,(bool REAL):] is non empty set

bool [:NAT,(bool REAL):] is non empty set

Funcs (NAT,(bool REAL)) is non empty functional FUNCTION_DOMAIN of NAT , bool REAL

[:NAT,(Funcs (NAT,(bool REAL))):] is non empty set

bool [:NAT,(Funcs (NAT,(bool REAL))):] is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() set

bool omega is non empty set

[:NAT,REAL:] is non empty complex-valued ext-real-valued real-valued set

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

bool NAT is non empty set

COMPLEX is non empty V34() V73() V79() set

RAT is non empty V34() V73() V74() V75() V76() V79() set

INT is non empty V34() V73() V74() V75() V76() V77() V79() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V73() V74() V75() V76() V77() V78() V79() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

{{},1} is non empty V73() V74() V75() V76() V77() V78() set

Funcs (NAT,ExtREAL) is non empty functional FUNCTION_DOMAIN of NAT , ExtREAL

[:NAT,(Funcs (NAT,ExtREAL)):] is non empty set

bool [:NAT,(Funcs (NAT,ExtREAL)):] is non empty set

[:(bool REAL),ExtREAL:] is non empty ext-real-valued set

bool [:(bool REAL),ExtREAL:] is non empty set

K464() is non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive Element of bool (bool REAL)

[:K464(),ExtREAL:] is non empty ext-real-valued set

bool [:K464(),ExtREAL:] is non empty set

[:NAT,NAT:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

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

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V58() V62() V73() V74() V75() V76() V77() V78() V79() Element of NAT

Seg 1 is V73() V74() V75() V76() V77() V78() Element of bool NAT

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

Seg 2 is V73() V74() V75() V76() V77() V78() Element of bool NAT

{1,2} is non empty V73() V74() V75() V76() V77() V78() set

0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative Function-like functional V56() real V73() V74() V75() V76() V77() V78() V79() Element of ExtREAL

+infty is non empty ext-real positive non negative non real Element of ExtREAL

+infty is non empty ext-real positive non negative non real set

-infty is non empty ext-real non positive negative non real set

PairFunc is non empty Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V27([:NAT,NAT:]) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]

X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Ser X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Partial_Sums X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

F is set

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

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

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

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

(Partial_Sums X) . m is ext-real Element of ExtREAL

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(Ser X) . (m + 1) is ext-real Element of ExtREAL

(Partial_Sums X) . (m + 1) is ext-real Element of ExtREAL

X . (m + 1) is ext-real Element of ExtREAL

((Partial_Sums X) . m) + (X . (m + 1)) is ext-real set

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

X . 0 is ext-real Element of ExtREAL

(Partial_Sums X) . 0 is ext-real Element of ExtREAL

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(Partial_Sums X) . m is ext-real Element of ExtREAL

X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM X is ext-real Element of ExtREAL

Ser X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser X) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser X)) is ext-real Element of ExtREAL

Sum X is ext-real Element of ExtREAL

Partial_Sums X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (Partial_Sums X) is ext-real Element of ExtREAL

sup (Partial_Sums X) is ext-real Element of ExtREAL

rng (Partial_Sums X) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Partial_Sums X)) is ext-real Element of ExtREAL

X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM X is ext-real Element of ExtREAL

Ser X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser X) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser X)) is ext-real Element of ExtREAL

Sum X is ext-real Element of ExtREAL

Partial_Sums X is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (Partial_Sums X) is ext-real Element of ExtREAL

F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM F is ext-real Element of ExtREAL

Ser F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser F) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser F)) is ext-real Element of ExtREAL

(SUM X) + (SUM F) is ext-real set

Sum F is ext-real Element of ExtREAL

Partial_Sums F is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (Partial_Sums F) is ext-real Element of ExtREAL

(Sum X) + (Sum F) is ext-real set

m is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM m is ext-real Element of ExtREAL

Ser m is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser m) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser m)) is ext-real Element of ExtREAL

Sum m is ext-real Element of ExtREAL

Partial_Sums m is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (Partial_Sums m) is ext-real Element of ExtREAL

Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

m . Bseq is ext-real Element of ExtREAL

X . Bseq is ext-real Element of ExtREAL

F . Bseq is ext-real Element of ExtREAL

(X . Bseq) + (F . Bseq) is ext-real set

M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

M1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

M . Bseq is ext-real Element of ExtREAL

Aseq . Bseq is ext-real Element of ExtREAL

M1 . Bseq is ext-real Element of ExtREAL

(Aseq . Bseq) + (M1 . Bseq) is ext-real set

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

Bseq is ext-real set

B is ext-real set

M . Bseq is ext-real Element of ExtREAL

M . B is ext-real Element of ExtREAL

Aseq . Bseq is ext-real Element of ExtREAL

Aseq . B is ext-real Element of ExtREAL

M1 . Bseq is ext-real Element of ExtREAL

M1 . B is ext-real Element of ExtREAL

(Aseq . Bseq) + (M1 . Bseq) is ext-real set

(Aseq . B) + (M1 . B) is ext-real set

lim M is ext-real Element of ExtREAL

sup M is ext-real Element of ExtREAL

rng M is non empty V45() V74() Element of bool ExtREAL

sup (rng M) is ext-real Element of ExtREAL

lim Aseq is ext-real Element of ExtREAL

sup Aseq is ext-real Element of ExtREAL

rng Aseq is non empty V45() V74() Element of bool ExtREAL

sup (rng Aseq) is ext-real Element of ExtREAL

Bseq is set

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

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

F . B is ext-real Element of ExtREAL

m . Bseq is ext-real Element of ExtREAL

X . B is ext-real Element of ExtREAL

(X . B) + (F . B) is ext-real set

lim M1 is ext-real Element of ExtREAL

sup M1 is ext-real Element of ExtREAL

rng M1 is non empty V45() V74() Element of bool ExtREAL

sup (rng M1) is ext-real Element of ExtREAL

(Sum X) + (SUM F) is ext-real set

X is set

bool X is non empty set

bool (bool X) is non empty set

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

[:NAT,F:] is non empty set

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

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

[:NAT,{{}}:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:NAT,{{}}:] is non empty set

m is non empty Relation-like NAT -defined {{}} -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,{{}}:]

M1 is non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,F:]

Aseq is set

M1 . Aseq is set

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

Aseq is set

M is set

M1 . Aseq is set

M1 . M is set

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

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

m is Relation-like NAT -defined bool X -valued Function-like FinSequence-like FinSequence of bool X

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

M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

m . M1 is Element of bool X

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

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

<*{}*> is Relation-like Function-like set

m is Relation-like NAT -defined bool X -valued Function-like FinSequence-like FinSequence of bool X

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

M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

m . M1 is Element of bool X

M1 is Relation-like NAT -defined bool X -valued Function-like FinSequence-like (X,F)

Aseq is set

M1 . Aseq is set

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

Aseq is set

M is set

M1 . Aseq is set

M1 . M is set

X is set

bool X is non empty set

bool (bool X) is non empty set

X is set

bool X is non empty set

bool (bool X) is non empty set

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

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

NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]

{X} is non empty set

[:NAT,{X}:] is non empty set

bool [:NAT,{X}:] is non empty set

m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

m . M1 is Element of bool X

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

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

F is Element of bool X

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]

{X} is non empty set

[:NAT,{X}:] is non empty set

bool [:NAT,{X}:] is non empty set

M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

M1 . Aseq is Element of bool X

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

rng Aseq is Element of bool (bool X)

bool (bool X) is non empty set

union (rng Aseq) is Element of bool X

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

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

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

M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

m . M1 is set

X is set

bool X is non empty set

bool (bool X) is non empty set

NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]

{X} is non empty set

[:NAT,{X}:] is non empty set

bool [:NAT,{X}:] is non empty set

bool X is non empty Element of bool (bool X)

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

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

rng (NAT --> X) is Element of bool {X}

bool {X} is non empty set

m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

M1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

m . M1 is Element of bool X

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X

[:NAT,(Funcs (NAT,(bool X))):] is non empty set

bool [:NAT,(Funcs (NAT,(bool X))):] is non empty set

m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

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

NAT --> X is non empty T-Sequence-like Relation-like NAT -defined {X} -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,{X}:]

{X} is non empty set

[:NAT,{X}:] is non empty set

bool [:NAT,{X}:] is non empty set

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

Aseq is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

NAT --> Aseq is non empty T-Sequence-like Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]

M is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]

rng (NAT --> X) is Element of bool {X}

bool {X} is non empty set

union (rng (NAT --> X)) is set

Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

m . Bseq is Element of bool X

M . Bseq is Relation-like Function-like Element of Funcs (NAT,(bool X))

X is set

bool X is non empty set

bool (bool X) is non empty set

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

[:F,ExtREAL:] is non empty ext-real-valued set

bool [:F,ExtREAL:] is non empty set

bool X is non empty Element of bool (bool X)

m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]

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

Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

Aseq . M is ext-real Element of ExtREAL

(X,F,M1,M) is Element of F

m . (X,F,M1,M) is ext-real Element of ExtREAL

Aseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Bseq is set

Aseq . Bseq is ext-real Element of ExtREAL

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

(X,F,M1,B) is Element of F

m . (X,F,M1,B) is ext-real Element of ExtREAL

M . Bseq is ext-real Element of ExtREAL

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

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

[:F,ExtREAL:] is non empty ext-real-valued set

bool [:F,ExtREAL:] is non empty set

m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]

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

(X,F,m,M1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,m,M1) . Aseq is ext-real Element of ExtREAL

(X,F,M1,Aseq) is Element of F

m . (X,F,M1,Aseq) is ext-real Element of ExtREAL

m . {} is ext-real Element of ExtREAL

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X

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

m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

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

Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

M1 . Aseq is Relation-like Function-like set

m . Aseq is Element of bool X

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

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

[:F,ExtREAL:] is non empty ext-real-valued set

bool [:F,ExtREAL:] is non empty set

Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X

m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

M1 is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]

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

M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

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

m . M is Element of bool X

(X,F,M1,(X,F,m,Aseq,M)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM (X,F,M1,(X,F,m,Aseq,M)) is ext-real Element of ExtREAL

Ser (X,F,M1,(X,F,m,Aseq,M)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser (X,F,M1,(X,F,m,Aseq,M))) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser (X,F,M1,(X,F,m,Aseq,M)))) is ext-real Element of ExtREAL

M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

M . Bseq is ext-real Element of ExtREAL

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

m . Bseq is Element of bool X

(X,F,M1,(X,F,m,Aseq,Bseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM (X,F,M1,(X,F,m,Aseq,Bseq)) is ext-real Element of ExtREAL

Ser (X,F,M1,(X,F,m,Aseq,Bseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser (X,F,M1,(X,F,m,Aseq,Bseq))) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser (X,F,M1,(X,F,m,Aseq,Bseq)))) is ext-real Element of ExtREAL

M is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Bseq is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

B is set

M . B is ext-real Element of ExtREAL

B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

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

m . B9 is Element of bool X

(X,F,M1,(X,F,m,Aseq,B9)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM (X,F,M1,(X,F,m,Aseq,B9)) is ext-real Element of ExtREAL

Ser (X,F,M1,(X,F,m,Aseq,B9)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser (X,F,M1,(X,F,m,Aseq,B9))) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser (X,F,M1,(X,F,m,Aseq,B9)))) is ext-real Element of ExtREAL

Bseq . B is ext-real Element of ExtREAL

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X

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

[:F,ExtREAL:] is non empty ext-real-valued set

bool [:F,ExtREAL:] is non empty set

m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]

M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

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

(X,F,M1,m,M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

(X,F,M1,m,M) . Aseq is ext-real Element of ExtREAL

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

M1 . Aseq is Element of bool X

(X,F,m,(X,F,M1,M,Aseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,m,(X,F,M1,M,Aseq)) . Bseq is ext-real Element of ExtREAL

(X,F,(X,F,M1,M,Aseq),Bseq) is Element of F

m . (X,F,(X,F,M1,M,Aseq),Bseq) is ext-real Element of ExtREAL

SUM (X,F,m,(X,F,M1,M,Aseq)) is ext-real Element of ExtREAL

Ser (X,F,m,(X,F,M1,M,Aseq)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser (X,F,m,(X,F,M1,M,Aseq))) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser (X,F,m,(X,F,M1,M,Aseq)))) is ext-real Element of ExtREAL

X is set

bool X is non empty set

bool (bool X) is non empty set

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

[:F,ExtREAL:] is non empty ext-real-valued set

bool [:F,ExtREAL:] is non empty set

bool X is non empty Element of bool (bool X)

M1 is Element of bool X

m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]

Aseq is set

M is set

M is V74() Element of bool ExtREAL

Bseq is ext-real Element of ExtREAL

B is ext-real Element of ExtREAL

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

(X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM (X,F,m,B9) is ext-real Element of ExtREAL

Ser (X,F,m,B9) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser (X,F,m,B9)) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser (X,F,m,B9))) is ext-real Element of ExtREAL

Aseq is V74() Element of bool ExtREAL

M is V74() Element of bool ExtREAL

X is set

bool X is non empty set

bool (bool X) is non empty set

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

[:m,ExtREAL:] is non empty ext-real-valued set

bool [:m,ExtREAL:] is non empty set

M1 is non empty Relation-like m -defined ExtREAL -valued Function-like V27(m) quasi_total ext-real-valued zeroed nonnegative V102(X,m) Element of bool [:m,ExtREAL:]

F is Element of bool X

(X,m,M1,F) is V74() Element of bool ExtREAL

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

{X,{}} is non empty set

Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

rng Aseq is Element of bool (bool X)

bool (bool X) is non empty set

Aseq . 0 is Element of bool X

M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

Aseq . M is Element of bool X

union {X,{}} is set

X \/ {} is set

Bseq is set

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

(X,m,M1,M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM (X,m,M1,M) is ext-real Element of ExtREAL

Ser (X,m,M1,M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

rng (Ser (X,m,M1,M)) is non empty V45() V74() Element of bool ExtREAL

sup (rng (Ser (X,m,M1,M))) is ext-real Element of ExtREAL

X is set

bool X is non empty set

bool (bool X) is non empty set

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

[:F,ExtREAL:] is non empty ext-real-valued set

bool [:F,ExtREAL:] is non empty set

bool X is non empty Element of bool (bool X)

[:(bool X),ExtREAL:] is non empty ext-real-valued set

bool [:(bool X),ExtREAL:] is non empty set

m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]

PairFunc " is Relation-like Function-like set

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

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

() is non empty Relation-like NAT -defined [:NAT,NAT:] -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,[:NAT,NAT:]:]

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X

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

m is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

rng m is Element of bool (bool X)

bool (bool X) is non empty set

union (rng m) is Element of bool X

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

pr1 () is non empty Relation-like NAT -defined NAT -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

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

pr2 () is non empty Relation-like NAT -defined NAT -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr1 ()) . Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

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

m . ((pr1 ()) . Aseq) is Element of bool X

(pr2 ()) . Aseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,m,M1,((pr1 ()) . Aseq)),((pr2 ()) . Aseq)) is Element of F

Aseq is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

M . Bseq is Element of bool X

(pr1 ()) . Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

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

m . ((pr1 ()) . Bseq) is Element of bool X

(pr2 ()) . Bseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,m,M1,((pr1 ()) . Bseq)),((pr2 ()) . Bseq)) is Element of F

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

rng Bseq is Element of bool (bool X)

union (rng Bseq) is Element of bool X

B is set

B9 is set

Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

m . Cseq is Element of bool X

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

rng (X,F,m,M1,Cseq) is Element of bool (bool X)

union (rng (X,F,m,M1,Cseq)) is Element of bool X

Cseq is set

Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,m,M1,Cseq),Cseq) is Element of F

dom PairFunc is Relation-like NAT -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

rng () is Relation-like NAT -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

[Cseq,Cseq] is set

{Cseq,Cseq} is non empty V73() V74() V75() V76() V77() V78() set

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

{{Cseq,Cseq},{Cseq}} is non empty set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

() . n is Element of [:NAT,NAT:]

(pr1 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

[((pr1 ()) . n),((pr2 ()) . n)] is set

{((pr1 ()) . n),((pr2 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set

{((pr1 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set

{{((pr1 ()) . n),((pr2 ()) . n)},{((pr1 ()) . n)}} is non empty set

(X,F,Bseq,n) is Element of F

B is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng m),F)

B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

(X,F,B,B9) is Element of F

(pr1 ()) . B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

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

m . ((pr1 ()) . B9) is Element of bool X

(pr2 ()) . B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,m,M1,((pr1 ()) . B9)),((pr2 ()) . B9)) is Element of F

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

M is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng m),F)

Bseq is set

Aseq . Bseq is set

M . Bseq is set

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,Aseq,B) is Element of F

(pr1 ()) . B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

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

m . ((pr1 ()) . B) is Element of bool X

(pr2 ()) . B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,m,M1,((pr1 ()) . B)),((pr2 ()) . B)) is Element of F

X is set

bool X is non empty set

bool (bool X) is non empty set

bool X is non empty Element of bool (bool X)

[:NAT,(bool X):] is non empty set

bool [:NAT,(bool X):] is non empty set

Funcs (NAT,(bool X)) is non empty functional FUNCTION_DOMAIN of NAT , bool X

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

[:F,ExtREAL:] is non empty ext-real-valued set

bool [:F,ExtREAL:] is non empty set

m is non empty Relation-like F -defined ExtREAL -valued Function-like V27(F) quasi_total ext-real-valued zeroed nonnegative V102(X,F) Element of bool [:F,ExtREAL:]

NAT --> {} is non empty T-Sequence-like Relation-like NAT -defined {{}} -valued Function-like V27( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,{{}}:]

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

[:NAT,{{}}:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:NAT,{{}}:] is non empty set

M1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

M + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr1 ()) . (M + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr2 ()) . (M + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

{ b

Cseq is set

Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr1 ()) . Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

Cseq + ((pr1 ()) . (M + 1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

Cseq is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

n is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

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

(X,F,n,n1) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X, union (rng n),F)

rng n is Element of bool (bool X)

bool (bool X) is non empty set

union (rng n) is Element of bool X

(X,F,m,(X,F,n,n1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Partial_Sums (X,F,m,(X,F,n,n1)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

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

(X,F,n,m,n1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Partial_Sums (X,F,n,m,n1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

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

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,n,n1,x) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . x,F)

n . x is Element of bool X

k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

k . k is set

(X,F,(X,F,n,n1,x),k) is Element of F

PSv1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

k . PSv1 is set

Aseq is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

Aseq . k is set

(X,F,(X,F,n,n1,x),k) is Element of F

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

Aseq . k is set

k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

[:NAT,(Funcs (NAT,(bool X))):] is non empty set

bool [:NAT,(Funcs (NAT,(bool X))):] is non empty set

x is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

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

M1 . k is Element of bool X

k is Relation-like Function-like set

dom k is set

rng k is set

k is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

PSv1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

k . PSv1 is Element of bool X

(X,F,n,n1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . k,F)

n . k is Element of bool X

(X,F,(X,F,n,n1,k),PSv1) is Element of F

rng k is Element of bool (bool X)

union (rng k) is Element of bool X

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,n,n1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . k,F)

n . k is Element of bool X

k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

PSv1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

k . PSv1 is set

(X,F,(X,F,n,n1,k),PSv1) is Element of F

PSv0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

k . PSv0 is set

Aseq is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

Aseq . k is set

(X,F,(X,F,n,n1,k),k) is Element of F

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

Aseq . k is set

k is Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of Funcs (NAT,(bool X))

k is non empty Relation-like NAT -defined Funcs (NAT,(bool X)) -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(Funcs (NAT,(bool X))):]

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

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

M1 . k is Element of bool X

k is Relation-like Function-like set

dom k is set

rng k is set

PSv1 is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total Element of bool [:NAT,(bool X):]

PSv0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real set

PSv1 . PSv0 is Element of bool X

(X,F,n,n1,k) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,n . k,F)

n . k is Element of bool X

(X,F,(X,F,n,n1,k),PSv0) is Element of F

rng PSv1 is Element of bool (bool X)

union (rng PSv1) is Element of bool X

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

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

rng M1 is Element of bool (bool X)

union (rng M1) is Element of bool X

(X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Partial_Sums (X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

(X,F,(X,F,M1,k),(M + 1)) is Element of F

(X,F,M1,k,((pr1 ()) . (M + 1))) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . (M + 1)),F)

M1 . ((pr1 ()) . (M + 1)) is Element of bool X

(X,F,(X,F,M1,k,((pr1 ()) . (M + 1))),((pr2 ()) . (M + 1))) is Element of F

(X,F,m,(X,F,M1,k)) . (M + 1) is ext-real Element of ExtREAL

m . {} is ext-real Element of ExtREAL

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

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

(X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Partial_Sums (X,F,m,(X,F,M1,k)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

Cseq is non empty V73() V74() V75() V76() V77() V78() Element of bool NAT

SOS is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() Element of Cseq

(pr2 ()) . SOS is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

[:Cseq,NAT:] is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

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

SOS is non empty Relation-like Cseq -defined NAT -valued Function-like V27(Cseq) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:Cseq,NAT:]

(X,F,M1,k,((pr1 ()) . (M + 1))) is non empty Relation-like NAT -defined bool X -valued Function-like V27( NAT ) quasi_total (X,M1 . ((pr1 ()) . (M + 1)),F)

(X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) is non empty Relation-like NAT -defined ExtREAL -valued Function-like V27( NAT ) quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

(X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) * SOS is non empty Relation-like Cseq -defined ExtREAL -valued Function-like V27(Cseq) quasi_total ext-real-valued Element of bool [:Cseq,ExtREAL:]

[:Cseq,ExtREAL:] is non empty ext-real-valued set

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

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,m,(X,F,M1,k)) . n is ext-real Element of ExtREAL

((X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) * SOS) . n is ext-real Element of ExtREAL

(X,F,(X,F,M1,k),n) is Element of F

m . (X,F,(X,F,M1,k),n) is ext-real Element of ExtREAL

(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

SOS . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,M1,k,((pr1 ()) . (M + 1))),(SOS . n)) is Element of F

m . (X,F,(X,F,M1,k,((pr1 ()) . (M + 1))),(SOS . n)) is ext-real Element of ExtREAL

s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr1 ()) . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,m,(X,F,M1,k,((pr1 ()) . (M + 1)))) . (SOS . n) is ext-real Element of ExtREAL

(pr1 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,M1,k),n) is Element of F

m . (X,F,(X,F,M1,k),n) is ext-real Element of ExtREAL

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

M1 . ((pr1 ()) . n) is Element of bool X

(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is Element of F

m . (X,F,(X,F,M1,k,((pr1 ()) . n)),((pr2 ()) . n)) is ext-real Element of ExtREAL

n is set

s is set

SOS . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

SOS . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

() . n is set

(pr1 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr2 ()) . n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

[((pr1 ()) . n),((pr2 ()) . n)] is set

{((pr1 ()) . n),((pr2 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set

{((pr1 ()) . n)} is non empty V73() V74() V75() V76() V77() V78() set

{{((pr1 ()) . n),((pr2 ()) . n)},{((pr1 ()) . n)}} is non empty set

() . s is set

(pr1 ()) . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr2 ()) . s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

[((pr1 ()) . s),((pr2 ()) . s)] is set

{((pr1 ()) . s),((pr2 ()) . s)} is non empty V73() V74() V75() V76() V77() V78() set

{((pr1 ()) . s)} is non empty V73() V74() V75() V76() V77() V78() set

{{((pr1 ()) . s),((pr2 ()) . s)},{((pr1 ()) . s)}} is non empty set

n2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

(pr1 ()) . n2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() Element of NAT

c

(pr1 ()) . c

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,