:: MESFUNC9 semantic presentation

REAL is non empty V29() 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 Relation-like ext-real-valued set

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

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

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

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

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

bool (bool REAL) is non empty set

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

bool RAT is non empty set

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

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-zero empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V73() V74() V75() V76() V77() V78() V79() set

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

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

[:COMPLEX,COMPLEX:] is non empty Relation-like complex-valued set

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

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like complex-valued set

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

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

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

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

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

[:RAT,RAT:] is non empty Relation-like RAT -valued complex-valued ext-real-valued real-valued set

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

[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued complex-valued ext-real-valued real-valued set

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

[:INT,INT:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

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

[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

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

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

[:[:NAT,NAT:],NAT:] is non empty Relation-like 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 V11() real Relation-like non-zero empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V73() V74() V75() V76() V77() V78() V79() Element of ExtREAL

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-zero empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V47() complex-valued ext-real-valued real-valued natural-valued V73() V74() V75() V76() V77() V78() V79() V82() Element of NAT

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

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

{-infty} is non empty V74() set

{+infty} is non empty V74() set

- 1 is non empty V11() real ext-real non positive negative Element of REAL

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

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

X is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom S is Element of bool X

bool X is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S + M) is Element of bool X

dom M is Element of bool X

(dom S) /\ (dom M) is Element of bool X

rng M is V74() Element of bool ExtREAL

M " {+infty} is Element of bool X

rng S is V74() Element of bool ExtREAL

S " {+infty} is Element of bool X

M " {-infty} is Element of bool X

(S " {+infty}) /\ (M " {-infty}) is Element of bool X

S " {-infty} is Element of bool X

(S " {-infty}) /\ (M " {+infty}) is Element of bool X

((S " {+infty}) /\ (M " {-infty})) \/ ((S " {-infty}) /\ (M " {+infty})) is Element of bool X

((dom S) /\ (dom M)) \ {} is Element of bool X

X is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom S is Element of bool X

bool X is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

S - M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S - M) is Element of bool X

dom M is Element of bool X

(dom S) /\ (dom M) is Element of bool X

rng S is V74() Element of bool ExtREAL

S " {+infty} is Element of bool X

rng M is V74() Element of bool ExtREAL

M " {-infty} is Element of bool X

M " {+infty} is Element of bool X

(M " {+infty}) /\ (S " {+infty}) is Element of bool X

S " {-infty} is Element of bool X

(M " {-infty}) /\ (S " {-infty}) is Element of bool X

((M " {+infty}) /\ (S " {+infty})) \/ ((M " {-infty}) /\ (S " {-infty})) is Element of bool X

((dom S) /\ (dom M)) \ {} is Element of bool X

X is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S + M) is Element of bool X

bool X is non empty set

dom S is Element of bool X

dom M is Element of bool X

(dom S) /\ (dom M) is Element of bool X

E is set

(S + M) . E is ext-real Element of ExtREAL

S . E is ext-real Element of ExtREAL

M . E is ext-real Element of ExtREAL

(S . E) + (M . E) is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S + M) is Element of bool X

bool X is non empty set

dom S is Element of bool X

dom M is Element of bool X

(dom S) /\ (dom M) is Element of bool X

E is set

(S + M) . E is ext-real Element of ExtREAL

S . E is ext-real Element of ExtREAL

M . E is ext-real Element of ExtREAL

(S . E) + (M . E) is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

S - M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S - M) is Element of bool X

bool X is non empty set

dom S is Element of bool X

dom M is Element of bool X

(dom S) /\ (dom M) is Element of bool X

E is set

(S - M) . E is ext-real Element of ExtREAL

S . E is ext-real Element of ExtREAL

M . E is ext-real Element of ExtREAL

(S . E) - (M . E) is ext-real Element of ExtREAL

K111((M . E)) is ext-real set

K110((S . E),K111((M . E))) is ext-real set

X is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

S - M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S - M) is Element of bool X

bool X is non empty set

dom S is Element of bool X

dom M is Element of bool X

(dom S) /\ (dom M) is Element of bool X

E is set

(S - M) . E is ext-real Element of ExtREAL

S . E is ext-real Element of ExtREAL

M . E is ext-real Element of ExtREAL

(S . E) - (M . E) is ext-real Element of ExtREAL

K111((M . E)) is ext-real set

K110((S . E),K111((M . E))) is ext-real set

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

lim X is ext-real Element of ExtREAL

S is V11() real ext-real set

M is V11() real ext-real set

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

S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

X . S is ext-real Element of ExtREAL

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

lim X is ext-real Element of ExtREAL

S is ext-real set

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

M is ext-real set

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

E is set

X . E is ext-real Element of ExtREAL

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

X . F is ext-real Element of ExtREAL

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

{ (X . b

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

M . 0 is ext-real Element of ExtREAL

E is non empty V74() Element of bool ExtREAL

sup E is ext-real set

F is set

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

L is set

X . L is ext-real Element of ExtREAL

inf M is ext-real Element of ExtREAL

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

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

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

M . F is ext-real Element of ExtREAL

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

F is set

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

X . L is ext-real Element of ExtREAL

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

lim_sup X is ext-real Element of ExtREAL

inf (superior_realsequence X) is ext-real Element of ExtREAL

rng (superior_realsequence X) is non empty V55() V74() Element of bool ExtREAL

inf (rng (superior_realsequence X)) is ext-real Element of ExtREAL

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

lim X is ext-real Element of ExtREAL

S is ext-real set

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

M is ext-real set

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

E is set

X . E is ext-real Element of ExtREAL

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

X . F is ext-real Element of ExtREAL

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

{ (X . b

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

M . 0 is ext-real Element of ExtREAL

E is non empty V74() Element of bool ExtREAL

inf E is ext-real set

F is set

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

L is set

X . L is ext-real Element of ExtREAL

sup M is ext-real Element of ExtREAL

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

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

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

M . F is ext-real Element of ExtREAL

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

F is set

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

X . L is ext-real Element of ExtREAL

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

lim_inf X is ext-real Element of ExtREAL

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

rng (inferior_realsequence X) is non empty V55() V74() Element of bool ExtREAL

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

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

lim X is ext-real Element of ExtREAL

S is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim S is ext-real Element of ExtREAL

(lim X) + (lim S) is ext-real Element of ExtREAL

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

lim M is ext-real Element of ExtREAL

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

E is set

M . E is ext-real Element of ExtREAL

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

S . F is ext-real Element of ExtREAL

M . F is ext-real Element of ExtREAL

X . F is ext-real Element of ExtREAL

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

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

S . E is ext-real Element of ExtREAL

E is V11() real ext-real set

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . L is ext-real Element of ExtREAL

X . L is ext-real Element of ExtREAL

S . L is ext-real Element of ExtREAL

R_EAL E is ext-real Element of ExtREAL

(R_EAL E) + 0. is ext-real Element of ExtREAL

(X . L) + (S . L) is ext-real Element of ExtREAL

E is V11() real ext-real set

F is V11() real ext-real set

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

E0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . E0 is ext-real Element of ExtREAL

S . E0 is ext-real Element of ExtREAL

X . E0 is ext-real Element of ExtREAL

R_EAL F is ext-real Element of ExtREAL

(R_EAL F) + 0. is ext-real Element of ExtREAL

(X . E0) + (S . E0) is ext-real Element of ExtREAL

F is V11() real ext-real set

E + F is V11() real ext-real set

R_EAL (E + F) is ext-real Element of ExtREAL

E1 is V11() real ext-real set

R_EAL F is ext-real Element of ExtREAL

L is V11() real ext-real Element of REAL

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

E1 / 2 is V11() real ext-real Element of REAL

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

max (I,H) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . G is ext-real Element of ExtREAL

(M . G) - (R_EAL (E + F)) is ext-real Element of ExtREAL

K111((R_EAL (E + F))) is ext-real set

K110((M . G),K111((R_EAL (E + F)))) is ext-real set

|.((M . G) - (R_EAL (E + F))).| is ext-real Element of ExtREAL

S . G is ext-real Element of ExtREAL

(S . G) - (lim S) is ext-real Element of ExtREAL

K111((lim S)) is ext-real set

K110((S . G),K111((lim S))) is ext-real set

|.((S . G) - (lim S)).| is ext-real Element of ExtREAL

(S . G) - (R_EAL F) is ext-real Element of ExtREAL

K111((R_EAL F)) is ext-real set

K110((S . G),K111((R_EAL F))) is ext-real set

X . G is ext-real Element of ExtREAL

(X . G) - (lim X) is ext-real Element of ExtREAL

K111((lim X)) is ext-real set

K110((X . G),K111((lim X))) is ext-real set

|.((X . G) - (lim X)).| is ext-real Element of ExtREAL

R_EAL E is ext-real Element of ExtREAL

(X . G) - (R_EAL E) is ext-real Element of ExtREAL

K111((R_EAL E)) is ext-real set

K110((X . G),K111((R_EAL E))) is ext-real set

G is V11() real ext-real Element of REAL

G is V11() real ext-real Element of REAL

|.((S . G) - (R_EAL F)).| is ext-real Element of ExtREAL

|.G.| is V11() real ext-real Element of REAL

|.((X . G) - (R_EAL E)).| is ext-real Element of ExtREAL

|.G.| is V11() real ext-real Element of REAL

|.((S . G) - (R_EAL F)).| + |.((X . G) - (R_EAL E)).| is ext-real Element of ExtREAL

|.G.| + |.G.| is V11() real ext-real Element of REAL

E0 is V11() real ext-real Element of REAL

(R_EAL E) + (R_EAL F) is ext-real Element of ExtREAL

(M . G) - (R_EAL F) is ext-real Element of ExtREAL

K110((M . G),K111((R_EAL F))) is ext-real set

((M . G) - (R_EAL F)) - (R_EAL E) is ext-real Element of ExtREAL

K110(((M . G) - (R_EAL F)),K111((R_EAL E))) is ext-real set

(X . G) + (S . G) is ext-real Element of ExtREAL

((X . G) + (S . G)) - (R_EAL F) is ext-real Element of ExtREAL

K110(((X . G) + (S . G)),K111((R_EAL F))) is ext-real set

(((X . G) + (S . G)) - (R_EAL F)) - (R_EAL E) is ext-real Element of ExtREAL

K110((((X . G) + (S . G)) - (R_EAL F)),K111((R_EAL E))) is ext-real set

(X . G) + ((S . G) - (R_EAL F)) is ext-real Element of ExtREAL

((X . G) + ((S . G) - (R_EAL F))) - (R_EAL E) is ext-real Element of ExtREAL

K110(((X . G) + ((S . G) - (R_EAL F))),K111((R_EAL E))) is ext-real set

((S . G) - (R_EAL F)) + ((X . G) - (R_EAL E)) is ext-real Element of ExtREAL

(E1 / 2) + (E1 / 2) is V11() real ext-real Element of REAL

E0 is V11() real ext-real Element of REAL

L is V11() real ext-real Element of REAL

E0 + L is V11() real ext-real Element of REAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

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

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

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

E is Element of X

M # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

S # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

F is set

L is V11() real ext-real set

E0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

E1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

(S # E) . E1 is ext-real Element of ExtREAL

(M # E) . E1 is ext-real Element of ExtREAL

M . E1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

(M . E1) . E is ext-real Element of ExtREAL

(M . E1) | F is Relation-like X -defined F -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((M . E1) | F) . E is ext-real Element of ExtREAL

S . E1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(S . E1) . E is ext-real Element of ExtREAL

(S # E) . E1 is ext-real Element of ExtREAL

L is V11() real ext-real set

E0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

E1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

(S # E) . E1 is ext-real Element of ExtREAL

(M # E) . E1 is ext-real Element of ExtREAL

M . E1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

(M . E1) . E is ext-real Element of ExtREAL

(M . E1) | F is Relation-like X -defined F -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((M . E1) | F) . E is ext-real Element of ExtREAL

S . E1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(S . E1) . E is ext-real Element of ExtREAL

(S # E) . E1 is ext-real Element of ExtREAL

lim (M # E) is ext-real Element of ExtREAL

L is V11() real ext-real set

R_EAL L is ext-real Element of ExtREAL

E0 is V11() real ext-real set

E1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

(S # E) . H is ext-real Element of ExtREAL

((S # E) . H) - (R_EAL L) is ext-real Element of ExtREAL

K111((R_EAL L)) is ext-real set

K110(((S # E) . H),K111((R_EAL L))) is ext-real set

|.(((S # E) . H) - (R_EAL L)).| is ext-real Element of ExtREAL

(M # E) . H is ext-real Element of ExtREAL

M . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

(M . H) . E is ext-real Element of ExtREAL

(M . H) | F is Relation-like X -defined F -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((M . H) | F) . E is ext-real Element of ExtREAL

S . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(S . H) . E is ext-real Element of ExtREAL

((M # E) . H) - (lim (M # E)) is ext-real Element of ExtREAL

K111((lim (M # E))) is ext-real set

K110(((M # E) . H),K111((lim (M # E)))) is ext-real set

|.(((M # E) . H) - (lim (M # E))).| is ext-real Element of ExtREAL

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is non empty compl-closed sigma-multiplicative V96() V97() V98() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

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

M is non empty Relation-like S -defined ExtREAL -valued Function-like total quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:S,ExtREAL:]

E is Element of S

F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom F is Element of bool X

eq_dom (F,+infty) is Element of bool X

E /\ (eq_dom (F,+infty)) is Element of bool X

M . (E /\ (eq_dom (F,+infty))) is ext-real Element of ExtREAL

Integral (M,F) is ext-real Element of ExtREAL

max+ F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max+ F)) is ext-real Element of ExtREAL

max- F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max- F)) is ext-real Element of ExtREAL

(integral+ (M,(max+ F))) - (integral+ (M,(max- F))) is ext-real Element of ExtREAL

K111((integral+ (M,(max- F)))) is ext-real set

K110((integral+ (M,(max+ F))),K111((integral+ (M,(max- F))))) is ext-real set

F | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (F | E) is Element of bool X

(dom F) /\ E is Element of bool X

L is Element of S

F | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(F | L)) is ext-real Element of ExtREAL

integral+ (M,(F | E)) is ext-real Element of ExtREAL

Integral (M,(F | E)) is ext-real Element of ExtREAL

max+ (F | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max+ (F | E))) is ext-real Element of ExtREAL

max- (F | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max- (F | E))) is ext-real Element of ExtREAL

(integral+ (M,(max+ (F | E)))) - (integral+ (M,(max- (F | E)))) is ext-real Element of ExtREAL

K111((integral+ (M,(max- (F | E))))) is ext-real set

K110((integral+ (M,(max+ (F | E)))),K111((integral+ (M,(max- (F | E)))))) is ext-real set

(dom F) /\ L is Element of bool X

chi (L,X) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(chi (L,X)) | L is Relation-like X -defined L -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

E1 is Relation-like Function-like set

dom E1 is set

H is set

rng E1 is set

I is set

E1 . I is set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

I (#) ((chi (L,X)) | L) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

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

H is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

H . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . I) is Element of bool X

dom (chi (L,X)) is Element of bool X

dom ((chi (L,X)) | L) is Element of bool X

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

I (#) ((chi (L,X)) | L) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

H is set

(H . I) . H is ext-real Element of ExtREAL

G is Element of X

(chi (L,X)) . G is ext-real Element of ExtREAL

1. is ext-real Element of ExtREAL

((chi (L,X)) | L) . G is ext-real Element of ExtREAL

R_EAL I is ext-real Element of ExtREAL

(R_EAL I) * 1. is ext-real Element of ExtREAL

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

H . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . I) is Element of bool X

I is set

(H . I) . I is ext-real Element of ExtREAL

I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

I . H is ext-real Element of ExtREAL

H . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral' (M,(H . H)) is ext-real Element of ExtREAL

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

H . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral' (M,(H . G)) is ext-real Element of ExtREAL

dom (F | L) is Element of bool X

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

H . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

H . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

G is Element of X

(H . H) . G is ext-real Element of ExtREAL

(H . G) . G is ext-real Element of ExtREAL

dom (H . H) is Element of bool X

dom (H . G) is Element of bool X

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

H . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . H) is Element of bool X

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

G is set

(H . H) . G is ext-real Element of ExtREAL

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

I . H is ext-real Element of ExtREAL

R_EAL H is ext-real Element of ExtREAL

H . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . H) is Element of bool X

M . (dom (H . H)) is ext-real Element of ExtREAL

(R_EAL H) * (M . (dom (H . H))) is ext-real Element of ExtREAL

G is set

(H . H) . G is ext-real Element of ExtREAL

integral' (M,(H . H)) is ext-real Element of ExtREAL

E0 is Element of S

M . E0 is ext-real Element of ExtREAL

M . L is ext-real Element of ExtREAL

rng I is non empty V55() V74() Element of bool ExtREAL

H is V11() real ext-real set

I . 1 is ext-real Element of ExtREAL

R_EAL 1 is ext-real Element of ExtREAL

H . 1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . 1) is Element of bool X

M . (dom (H . 1)) is ext-real Element of ExtREAL

(R_EAL 1) * (M . (dom (H . 1))) is ext-real Element of ExtREAL

(R_EAL 1) * (M . L) is ext-real Element of ExtREAL

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

G is V11() real ext-real Element of REAL

G is V11() real ext-real Element of REAL

G / G is V11() real ext-real Element of REAL

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

I . G is ext-real Element of ExtREAL

R_EAL G is ext-real Element of ExtREAL

H . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . G) is Element of bool X

M . (dom (H . G)) is ext-real Element of ExtREAL

(R_EAL G) * (M . (dom (H . G))) is ext-real Element of ExtREAL

(R_EAL G) * (M . L) is ext-real Element of ExtREAL

G * G is V11() real ext-real Element of REAL

(G / G) * G is V11() real ext-real Element of REAL

G / G is V11() real ext-real Element of REAL

G / (G / G) is V11() real ext-real Element of REAL

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

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

I . G is ext-real Element of ExtREAL

I . H is ext-real Element of ExtREAL

H . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . G) is Element of bool X

R_EAL G is ext-real Element of ExtREAL

(R_EAL G) * (M . L) is ext-real Element of ExtREAL

H . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . H) is Element of bool X

R_EAL H is ext-real Element of ExtREAL

(R_EAL H) * (M . L) is ext-real Element of ExtREAL

lim I is ext-real Element of ExtREAL

sup I is ext-real Element of ExtREAL

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

H is Element of X

H # H is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (H # H) is ext-real Element of ExtREAL

(F | L) . H is ext-real Element of ExtREAL

F . H is ext-real Element of ExtREAL

rng (H # H) is non empty V55() V74() Element of bool ExtREAL

G is V11() real ext-real set

G is V11() real ext-real Element of REAL

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

H . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . G) is Element of bool X

(H . G) . H is ext-real Element of ExtREAL

(H # H) . G is ext-real Element of ExtREAL

dom (H # H) is non empty V73() V74() V75() V76() V77() V78() Element of bool NAT

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

(H # H) . G is ext-real Element of ExtREAL

(H # H) . G is ext-real Element of ExtREAL

H . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . G) is Element of bool X

(H . G) . H is ext-real Element of ExtREAL

H . G is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (H . G) is Element of bool X

(H . G) . H is ext-real Element of ExtREAL

sup (rng (H # H)) is ext-real set

sup (H # H) is ext-real Element of ExtREAL

sup (rng (H # H)) is ext-real Element of ExtREAL

sup (rng I) is ext-real set

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

S is non empty compl-closed sigma-multiplicative V96() V97() V98() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

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

M is non empty Relation-like S -defined ExtREAL -valued Function-like total quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:S,ExtREAL:]

E is Element of S

chi (E,X) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

Integral (M,(chi (E,X))) is ext-real Element of ExtREAL

max+ (chi (E,X)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max+ (chi (E,X)))) is ext-real Element of ExtREAL

max- (chi (E,X)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max- (chi (E,X)))) is ext-real Element of ExtREAL

(integral+ (M,(max+ (chi (E,X))))) - (integral+ (M,(max- (chi (E,X))))) is ext-real Element of ExtREAL

K111((integral+ (M,(max- (chi (E,X)))))) is ext-real set

K110((integral+ (M,(max+ (chi (E,X))))),K111((integral+ (M,(max- (chi (E,X))))))) is ext-real set

M . E is ext-real Element of ExtREAL

(chi (E,X)) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

Integral (M,((chi (E,X)) | E)) is ext-real Element of ExtREAL

max+ ((chi (E,X)) | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max+ ((chi (E,X)) | E))) is ext-real Element of ExtREAL

max- ((chi (E,X)) | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max- ((chi (E,X)) | E))) is ext-real Element of ExtREAL

(integral+ (M,(max+ ((chi (E,X)) | E)))) - (integral+ (M,(max- ((chi (E,X)) | E)))) is ext-real Element of ExtREAL

K111((integral+ (M,(max- ((chi (E,X)) | E))))) is ext-real set

K110((integral+ (M,(max+ ((chi (E,X)) | E)))),K111((integral+ (M,(max- ((chi (E,X)) | E)))))) is ext-real set

F is Element of S

F \ E is Element of S

E0 is Element of X

dom (max- (chi (E,X))) is Element of bool X

(chi (E,X)) . E0 is ext-real Element of ExtREAL

- ((chi (E,X)) . E0) is ext-real Element of ExtREAL

max ((- ((chi (E,X)) . E0)),0.) is ext-real set

(max- (chi (E,X))) . E0 is ext-real Element of ExtREAL

(chi (E,X)) . E0 is ext-real Element of ExtREAL

- ((chi (E,X)) . E0) is ext-real Element of ExtREAL

max ((- ((chi (E,X)) . E0)),0.) is ext-real set

(max- (chi (E,X))) . E0 is ext-real Element of ExtREAL

dom (chi (E,X)) is Element of bool X

dom (max+ (chi (E,X))) is Element of bool X

F /\ (F \ E) is Element of S

(max+ (chi (E,X))) | (F \ E) is Relation-like X -defined F \ E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom ((max+ (chi (E,X))) | (F \ E)) is Element of bool X

E0 is Element of X

(chi (E,X)) . E0 is ext-real Element of ExtREAL

(max+ (chi (E,X))) . E0 is ext-real Element of ExtREAL

((max+ (chi (E,X))) | (F \ E)) . E0 is ext-real Element of ExtREAL

integral+ (M,((max+ (chi (E,X))) | (F \ E))) is ext-real Element of ExtREAL

F /\ E is Element of S

(max+ (chi (E,X))) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom ((max+ (chi (E,X))) | E) is Element of bool X

E \/ (F \ E) is Element of S

(max+ (chi (E,X))) | (E \/ (F \ E)) is Relation-like X -defined E \/ (F \ E) -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

E0 is set

(max+ (chi (E,X))) . E0 is ext-real Element of ExtREAL

integral+ (M,((max+ (chi (E,X))) | (E \/ (F \ E)))) is ext-real Element of ExtREAL

integral+ (M,((max+ (chi (E,X))) | E)) is ext-real Element of ExtREAL

(integral+ (M,((max+ (chi (E,X))) | E))) + (integral+ (M,((max+ (chi (E,X))) | (F \ E)))) is ext-real Element of ExtREAL

E0 is set

(chi (E,X)) . E0 is ext-real Element of ExtREAL

(max+ (chi (E,X))) . E0 is ext-real Element of ExtREAL

((max+ (chi (E,X))) | E) . E0 is ext-real Element of ExtREAL

integral' (M,((max+ (chi (E,X))) | E)) is ext-real Element of ExtREAL

R_EAL 1 is ext-real Element of ExtREAL

M . (dom ((max+ (chi (E,X))) | E)) is ext-real Element of ExtREAL

(R_EAL 1) * (M . (dom ((max+ (chi (E,X))) | E))) is ext-real Element of ExtREAL

dom ((chi (E,X)) | E) is Element of bool X

integral+ (M,((chi (E,X)) | E)) is ext-real Element of ExtREAL

(R_EAL 1) * (M . E) is ext-real Element of ExtREAL

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

S is non empty compl-closed sigma-multiplicative V96() V97() V98() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty Relation-like ext-real-valued set

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

M is non empty Relation-like S -defined ExtREAL -valued Function-like total quasi_total ext-real-valued zeroed nonnegative sigma-additive Element of bool [:S,ExtREAL:]

E is Element of S

F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom F is Element of bool X

F | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

Integral (M,(F | E)) is ext-real Element of ExtREAL

max+ (F | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max+ (F | E))) is ext-real Element of ExtREAL

max- (F | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max- (F | E))) is ext-real Element of ExtREAL

(integral+ (M,(max+ (F | E)))) - (integral+ (M,(max- (F | E)))) is ext-real Element of ExtREAL

K111((integral+ (M,(max- (F | E))))) is ext-real set

K110((integral+ (M,(max+ (F | E)))),K111((integral+ (M,(max- (F | E)))))) is ext-real set

L is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom L is Element of bool X

L | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

Integral (M,(L | E)) is ext-real Element of ExtREAL

max+ (L | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max+ (L | E))) is ext-real Element of ExtREAL

max- (L | E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

integral+ (M,(max- (L | E))) is ext-real Element of ExtREAL

(integral+ (M,(max+ (L | E)))) - (integral+ (M,(max- (L | E)))) is ext-real Element of ExtREAL

K111((integral+ (M,(max- (L | E))))) is ext-real set

K110((integral+ (M,(max+ (L | E)))),K111((integral+ (M,(max- (L | E)))))) is ext-real set

dom (F | E) is Element of bool X

dom (L | E) is Element of bool X

H is Element of X

(F | E) . H is ext-real Element of ExtREAL

(L | E) . H is ext-real Element of ExtREAL

F . H is ext-real Element of ExtREAL

L . H is ext-real Element of ExtREAL

H is set

(L | E) . H is ext-real Element of ExtREAL

(F | E) . H is ext-real Element of ExtREAL

(dom L) /\ E is Element of bool X

(dom F) /\ E is Element of bool X

integral+ (M,(F | E)) is ext-real Element of ExtREAL

integral+ (M,(L | E)) is ext-real Element of ExtREAL

X is Relation-like Function-like ext-real-valued set

S is set

X . S is ext-real set

X is Relation-like Function-like ext-real-valued set

(X,0) is ext-real Element of ExtREAL

S is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

(S,0) is ext-real Element of ExtREAL

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

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

(S,(M + 1)) is ext-real Element of ExtREAL

(S,M) is ext-real Element of ExtREAL

(X,(M + 1)) is ext-real Element of ExtREAL

(S,M) + (X,(M + 1)) is ext-real Element of ExtREAL

S is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

(S,0) is ext-real Element of ExtREAL

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

(M,0) is ext-real Element of ExtREAL

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

(S,E) is ext-real Element of ExtREAL

(M,E) is ext-real Element of ExtREAL

E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

(S,(E + 1)) is ext-real Element of ExtREAL

(M,(E + 1)) is ext-real Element of ExtREAL

(X,(E + 1)) is ext-real Element of ExtREAL

(M,E) + (X,(E + 1)) is ext-real Element of ExtREAL

X is Relation-like Function-like ext-real-valued set

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

lim (X) is ext-real Element of ExtREAL

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

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

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

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

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

((X),(M + 1)) is ext-real Element of ExtREAL

(X,(M + 1)) is ext-real Element of ExtREAL

((X),M) + (X,(M + 1)) is ext-real Element of ExtREAL

((X),0) is ext-real Element of ExtREAL

(X,0) is ext-real Element of ExtREAL

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

M is set

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

E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

((X),E) is ext-real Element of ExtREAL

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

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

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

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

((X),L) is ext-real Element of ExtREAL

L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

((X),(L + 1)) is ext-real Element of ExtREAL

(X,(L + 1)) is ext-real Element of ExtREAL

((X),L) + (X,(L + 1)) is ext-real Element of ExtREAL

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

((X),L) is ext-real Element of ExtREAL

F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

L - 1 is V11() real ext-real Element of REAL

L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

E0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

E0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

((X),E0) is ext-real Element of ExtREAL

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

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

S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

((X),S) is ext-real Element of ExtREAL

S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

((X),(S + 1)) is ext-real Element of ExtREAL

(X,(S + 1)) is ext-real Element of ExtREAL

((X),S) + (X,(S + 1)) is ext-real Element of ExtREAL

((X),0) is ext-real Element of ExtREAL

(X,0) is ext-real Element of ExtREAL

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

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

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

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

E is set

F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

dom (M . F) is Element of bool X

bool X is non empty set

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

M . L is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . L) is Element of bool X

S . L is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(S . L) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . L) is Element of bool X

(dom (S . L)) /\ E is Element of bool X

S . F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(S . F) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (S . F) is Element of bool X

(dom (S . F)) /\ E is Element of bool X

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

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

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

dom (S . 0) is Element of bool X

bool X is non empty set

lim S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

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

lim M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

E is set

(lim S) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

M . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(S . 0) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (M . 0) is Element of bool X

dom ((lim S) | E) is Element of bool X

dom (lim S) is Element of bool X

(dom (lim S)) /\ E is Element of bool X

(dom (S . 0)) /\ E is Element of bool X

dom (lim M) is Element of bool X

F is Element of X

(((lim S) | E),F) is ext-real Element of ExtREAL

((lim S),F) is ext-real Element of ExtREAL

S # F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (S # F) is ext-real Element of ExtREAL

M # F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (M # F) is ext-real Element of ExtREAL

((lim M),F) is ext-real Element of ExtREAL

M # F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

lim (M # F) is ext-real Element of ExtREAL

((lim M),F) is ext-real Element of ExtREAL

L is V11() real ext-real set

E0 is V11() real ext-real set

E1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

((S # F),I) is ext-real Element of ExtREAL

S . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((S . I),F) is ext-real Element of ExtREAL

(S . I) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(((S . I) | E),F) is ext-real Element of ExtREAL

M . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

((M . I),F) is ext-real Element of ExtREAL

H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

((S # F),I) - (lim (S # F)) is ext-real Element of ExtREAL

K111((lim (S # F))) is ext-real set

K110(((S # F),I),K111((lim (S # F)))) is ext-real set

|.(((S # F),I) - (lim (S # F))).| is ext-real Element of ExtREAL

M # F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

((M # F),I) is ext-real Element of ExtREAL

R_EAL L is ext-real Element of ExtREAL

((M # F),I) - (R_EAL L) is ext-real Element of ExtREAL

K111((R_EAL L)) is ext-real set

K110(((M # F),I),K111((R_EAL L))) is ext-real set

|.(((M # F),I) - (R_EAL L)).| is ext-real Element of ExtREAL

lim (M # F) is ext-real Element of ExtREAL

((lim M),F) is ext-real Element of ExtREAL

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

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

S is non empty compl-closed sigma-multiplicative V96() V97() V98() sigma-additive Element of bool (bool X)

M is Element of S

E is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

E . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

dom (E . 0) is Element of bool X

F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

F . L is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

E . L is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (E . L) is Element of bool X

(dom (E . L)) /\ M is Element of bool X

(E . L) | M is Relation-like X -defined M -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

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

S is non empty compl-closed sigma-multiplicative V96() V97() V98() sigma-additive Element of bool (bool X)

M is Element of S

E is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

E . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

dom (E . 0) is Element of bool X

F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

L is Element of X

F # L is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

(E . 0) | M is Relation-like X -defined M -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom ((E . 0) | M) is Element of bool X

F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (F . 0) is Element of bool X

E # L is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

E0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

((E # L),E0) is ext-real Element of ExtREAL

((F # L),E0) is ext-real Element of ExtREAL

F . E0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom (F . E0) is Element of bool X

E . E0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

(E . E0) | M is Relation-like X -defined M -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

dom ((E . E0) | M) is Element of bool X

(((E . E0) | M),L) is ext-real Element of ExtREAL

((E . E0),L) is ext-real Element of ExtREAL

((F . E0),L) is ext-real Element of ExtREAL

((E # L)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total quasi_total ext-real-valued Element of bool [:NAT,ExtREAL:]

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

X is non empty set

PFuncs (X,ExtREAL) is non empty functional set

[:NAT,(PFuncs (X,ExtREAL)):] is non empty Relation-like set

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

S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total Element of bool [:NAT,(PFuncs (X,ExtREAL)):]

S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

[:X,ExtREAL:] is non empty Relation-like ext-real-valued set

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

M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

S . M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

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

S . (M + 1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

E is set

F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

L is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

L + (S . (M + 1)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

F + (S . (M + 1)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

L is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

E0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

E0 + (S . (M + 1)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]

M is Relation-like Function-like set

dom M is set

M . 0 is set

E is set

rng M is set

F is set

M . F is set

E0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

M . E0 is set

E0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V47() V73() V74() V75() V76() V77() V78() V82() Element of NAT

M . (E0 + 1) is set

E1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of