:: MESFUN10 semantic presentation

REAL is non empty V29() V66() V67() V68() V72() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V66() V67() V68() V69() V70() V71() V72() Element of K6(REAL)
K6(REAL) is set
ExtREAL is non empty V67() set
K7(NAT,ExtREAL) is Relation-like ext-real-valued set
K6(K7(NAT,ExtREAL)) is set
K6(ExtREAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V66() V67() V68() V69() V70() V71() V72() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
K6(K6(REAL)) is set
RAT is non empty V29() V66() V67() V68() V69() V72() set
K6(RAT) is set
COMPLEX is non empty V29() V66() V72() set
INT is non empty V29() V66() V67() V68() V69() V70() V72() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V66() V67() V68() V69() V70() V71() V72() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{{},1} is non empty V66() V67() V68() V69() V70() V71() set
K7(COMPLEX,COMPLEX) is Relation-like complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is Relation-like complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V66() V67() V68() V69() V70() V71() V72() Element of ExtREAL
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V66() V67() V68() V69() V70() V71() V72() V75() V76() Element of NAT
+infty is non empty non real ext-real positive non negative Element of ExtREAL
|.+infty.| is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
|.-infty.| is ext-real Element of ExtREAL
{-infty} is non empty V67() set
{+infty} is non empty V67() set
- 1 is V11() real ext-real non positive 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 Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
rng X is non empty V50() V67() Element of K6(ExtREAL)
inf (rng X) is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
rng F is non empty V50() V67() Element of K6(ExtREAL)
inf (rng F) is ext-real Element of ExtREAL
dom X is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . M is ext-real Element of ExtREAL
F . M is ext-real Element of ExtREAL
S is ext-real set
dom F is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
M is set
F . M is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
inferior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
superior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
inferior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
superior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(inferior_realsequence X) . S is ext-real Element of ExtREAL
(inferior_realsequence F) . S is ext-real Element of ExtREAL
(superior_realsequence X) . S is ext-real Element of ExtREAL
(superior_realsequence F) . S is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F ^\ M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(F ^\ M) . E is ext-real Element of ExtREAL
E + S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . (E + S) is ext-real Element of ExtREAL
X ^\ M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of X
(X ^\ M) . E is ext-real Element of ExtREAL
X . (E + S) is ext-real Element of ExtREAL
sup (X ^\ M) is ext-real Element of ExtREAL
rng (X ^\ M) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (X ^\ M)) is ext-real Element of ExtREAL
sup (F ^\ M) is ext-real Element of ExtREAL
rng (F ^\ M) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (F ^\ M)) is ext-real Element of ExtREAL
inf (X ^\ M) is ext-real Element of ExtREAL
inf (rng (X ^\ M)) is ext-real Element of ExtREAL
inf (F ^\ M) is ext-real Element of ExtREAL
inf (rng (F ^\ M)) is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf X is ext-real Element of ExtREAL
inferior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence X) is ext-real Element of ExtREAL
rng (inferior_realsequence X) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence X)) is ext-real Element of ExtREAL
lim_sup X is ext-real Element of ExtREAL
superior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence X) is ext-real Element of ExtREAL
rng (superior_realsequence X) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence X)) is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf F is ext-real Element of ExtREAL
inferior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence F) is ext-real Element of ExtREAL
rng (inferior_realsequence F) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence F)) is ext-real Element of ExtREAL
lim_sup F is ext-real Element of ExtREAL
superior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence F) is ext-real Element of ExtREAL
rng (superior_realsequence F) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence F)) is ext-real Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(inferior_realsequence X) . S is ext-real Element of ExtREAL
(inferior_realsequence F) . S is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(superior_realsequence X) . M is ext-real Element of ExtREAL
(superior_realsequence F) . M is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
inf X is ext-real Element of ExtREAL
rng X is non empty V50() V67() Element of K6(ExtREAL)
inf (rng X) is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
S is ext-real set
dom X is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
M is set
X . M is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
sup X is ext-real Element of ExtREAL
rng X is non empty V50() V67() Element of K6(ExtREAL)
sup (rng X) is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
S is ext-real set
dom X is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
M is set
X . M is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
S is Element of X
F # S is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F ^\ M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom subsequence of F
inf (F ^\ M) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
dom (inf (F ^\ M)) is Element of K6(X)
K6(X) is set
(inf (F ^\ M)) . S is ext-real Element of ExtREAL
(F # S) ^\ M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F # S
inf ((F # S) ^\ M) is ext-real Element of ExtREAL
rng ((F # S) ^\ M) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng ((F # S) ^\ M)) is ext-real Element of ExtREAL
(F ^\ M) # S is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
((F ^\ M) # S) . f is ext-real Element of ExtREAL
(F ^\ M) . f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((F ^\ M) . f) . S is ext-real Element of ExtREAL
E is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
M + f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
E . (M + f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(E . (M + f)) . S is ext-real Element of ExtREAL
(F # S) . (M + f) is ext-real Element of ExtREAL
((F # S) ^\ M) . f is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K6(X) is set
K6(K6(X)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
dom (F . 0) is Element of K6(X)
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is Relation-like ext-real-valued set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V41(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
Integral (M,(lim_inf F)) is ext-real Element of ExtREAL
E is Element of S
inferior_realsequence F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
N is Relation-like Function-like set
dom N is set
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
N . N1 is set
F ^\ N1 is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom subsequence of F
inf (F ^\ N1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
N1 is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
N1 . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(inferior_realsequence F) . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F ^\ h is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom subsequence of F
inf (F ^\ h) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(inferior_realsequence F) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((inferior_realsequence F) . 0) is Element of K6(X)
h is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
h . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (h . 0) is Element of K6(X)
AFN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
h . AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
h . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I is Element of X
(h . AFN) . I is ext-real Element of ExtREAL
(h . J) . I is ext-real Element of ExtREAL
h # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(h # I) . AFN is ext-real Element of ExtREAL
(h # I) . J is ext-real Element of ExtREAL
(inferior_realsequence F) # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
inferior_realsequence (F # I) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
((inferior_realsequence F) # I) . I is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
((inferior_realsequence F) # I) . n is ext-real Element of ExtREAL
(inferior_realsequence F) . AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((inferior_realsequence F) . AFN) . I is ext-real Element of ExtREAL
((inferior_realsequence F) # I) . J is ext-real Element of ExtREAL
AFN is Element of X
h # AFN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
(h # AFN) . I is ext-real Element of ExtREAL
(h # AFN) . J is ext-real Element of ExtREAL
AFN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
h . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (lim h) is Element of K6(X)
J is set
(h . 0) . J is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I is Element of X
(F . I) . I is ext-real Element of ExtREAL
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
0 + I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
(F # I) . (0 + I) is ext-real Element of ExtREAL
(F # I) ^\ 0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F # I
((F # I) ^\ 0) . I is ext-real Element of ExtREAL
F ^\ 0 is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom subsequence of F
(F ^\ 0) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V66() V67() V68() V69() V70() V71() V72() V75() V76() Element of NAT
F . (0 + 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
inf (F ^\ 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (inf (F ^\ 0)) is Element of K6(X)
(inf (F ^\ 0)) . I is ext-real Element of ExtREAL
inf ((F # I) ^\ 0) is ext-real Element of ExtREAL
rng ((F # I) ^\ 0) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng ((F # I) ^\ 0)) is ext-real Element of ExtREAL
(h . 0) . I is ext-real Element of ExtREAL
J 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 Element of X
h . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(h . J) . I is ext-real Element of ExtREAL
h . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(h . I) . I is ext-real Element of ExtREAL
Integral (M,(lim h)) is ext-real Element of ExtREAL
J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim J is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
J . I is ext-real Element of ExtREAL
I . I is ext-real Element of ExtREAL
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . I) is Element of K6(X)
n is Element of X
h . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (h . I) is Element of K6(X)
F # n is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
inferior_realsequence (F # n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(inferior_realsequence (F # n)) . I is ext-real Element of ExtREAL
(F # n) . I is ext-real Element of ExtREAL
(inferior_realsequence F) . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((inferior_realsequence F) . I) . n is ext-real Element of ExtREAL
(F . I) . n is ext-real Element of ExtREAL
(h . I) . n is ext-real Element of ExtREAL
n is set
(h . 0) . n is ext-real Element of ExtREAL
(h . I) . n is ext-real Element of ExtREAL
integral+ (M,(h . I)) is ext-real Element of ExtREAL
integral+ (M,(F . I)) is ext-real Element of ExtREAL
Integral (M,(h . I)) is ext-real Element of ExtREAL
Integral (M,(F . I)) is ext-real Element of ExtREAL
lim_inf J is ext-real Element of ExtREAL
inferior_realsequence J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence J) is ext-real Element of ExtREAL
rng (inferior_realsequence J) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence J)) is ext-real Element of ExtREAL
lim_inf I is ext-real Element of ExtREAL
inferior_realsequence I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence I) is ext-real Element of ExtREAL
rng (inferior_realsequence I) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence I)) is ext-real Element of ExtREAL
sup h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (sup h) is Element of K6(X)
I is Element of X
h # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
(h # I) . e1 is ext-real Element of ExtREAL
(h # I) . n is ext-real Element of ExtREAL
lim (h # I) is ext-real Element of ExtREAL
sup (h # I) is ext-real Element of ExtREAL
rng (h # I) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (h # I)) is ext-real Element of ExtREAL
(sup h) . I is ext-real Element of ExtREAL
(lim h) . I is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
I . I is ext-real Element of ExtREAL
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(F . I)) is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
I . I is ext-real Element of ExtREAL
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(F . I)) is ext-real Element of ExtREAL
X is non empty V67() Element of K6(ExtREAL)
sup X is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
{F} is non empty V67() Element of K6(ExtREAL)
{F} + X is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {F} & b₂ in X ) } is set
sup ({F} + X) is ext-real Element of ExtREAL
sup {F} is ext-real Element of ExtREAL
(sup {F}) + (sup X) is ext-real Element of ExtREAL
- F is ext-real Element of ExtREAL
E is set
- {F} is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in {F} } is set
(- {F}) + ({F} + X) is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in - {F} & b₂ in {F} + X ) } is set
f is ext-real Element of ExtREAL
N is ext-real Element of ExtREAL
f + N is ext-real Element of ExtREAL
N1 is ext-real Element of ExtREAL
h is ext-real Element of ExtREAL
N1 + h is ext-real Element of ExtREAL
- f is ext-real Element of ExtREAL
- (- {F}) is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in - {F} } is set
F + h is ext-real Element of ExtREAL
(- F) + (F + h) is ext-real Element of ExtREAL
(- F) + F is ext-real Element of ExtREAL
((- F) + F) + h is ext-real Element of ExtREAL
0. + h is ext-real Element of ExtREAL
E is set
f is ext-real Element of ExtREAL
F + f is ext-real Element of ExtREAL
(F + f) - F is ext-real Element of ExtREAL
K152(F) is ext-real set
K151((F + f),K152(F)) is ext-real set
((- F) + F) + f is ext-real Element of ExtREAL
0. + f is ext-real Element of ExtREAL
sup (- {F}) is ext-real Element of ExtREAL
(sup ({F} + X)) + (sup (- {F})) is ext-real Element of ExtREAL
inf {F} is ext-real Element of ExtREAL
- (inf {F}) is ext-real Element of ExtREAL
(sup ({F} + X)) + (- (inf {F})) is ext-real Element of ExtREAL
(sup ({F} + X)) - F is ext-real Element of ExtREAL
K151((sup ({F} + X)),K152(F)) is ext-real set
F + (sup X) is ext-real Element of ExtREAL
X is non empty V67() Element of K6(ExtREAL)
inf X is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
{F} is non empty V67() Element of K6(ExtREAL)
{F} + X is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {F} & b₂ in X ) } is set
inf ({F} + X) is ext-real Element of ExtREAL
inf {F} is ext-real Element of ExtREAL
(inf {F}) + (inf X) is ext-real Element of ExtREAL
- {F} is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in {F} } is set
- F is ext-real Element of ExtREAL
f is set
(- {F}) + ({F} + X) is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in - {F} & b₂ in {F} + X ) } is set
N is ext-real Element of ExtREAL
N1 is ext-real Element of ExtREAL
N + N1 is ext-real Element of ExtREAL
h is ext-real Element of ExtREAL
AFN is ext-real Element of ExtREAL
h + AFN is ext-real Element of ExtREAL
- N is ext-real Element of ExtREAL
- (- {F}) is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in - {F} } is set
F + AFN is ext-real Element of ExtREAL
(- F) + (F + AFN) is ext-real Element of ExtREAL
(- F) + F is ext-real Element of ExtREAL
((- F) + F) + AFN is ext-real Element of ExtREAL
0. + AFN is ext-real Element of ExtREAL
f is set
N is ext-real Element of ExtREAL
F + N is ext-real Element of ExtREAL
(F + N) - F is ext-real Element of ExtREAL
K152(F) is ext-real set
K151((F + N),K152(F)) is ext-real set
((- F) + F) + N is ext-real Element of ExtREAL
0. + N is ext-real Element of ExtREAL
inf (- {F}) is ext-real Element of ExtREAL
(inf ({F} + X)) + (inf (- {F})) is ext-real Element of ExtREAL
sup {F} is ext-real Element of ExtREAL
- (sup {F}) is ext-real Element of ExtREAL
(inf ({F} + X)) + (- (sup {F})) is ext-real Element of ExtREAL
(inf ({F} + X)) - F is ext-real Element of ExtREAL
K151((inf ({F} + X)),K152(F)) is ext-real set
F + (inf X) is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf X is ext-real Element of ExtREAL
inferior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence X) is ext-real Element of ExtREAL
rng (inferior_realsequence X) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence X)) is ext-real Element of ExtREAL
lim_sup X is ext-real Element of ExtREAL
superior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence X) is ext-real Element of ExtREAL
rng (superior_realsequence X) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence X)) is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf F is ext-real Element of ExtREAL
inferior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence F) is ext-real Element of ExtREAL
rng (inferior_realsequence F) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence F)) is ext-real Element of ExtREAL
lim_sup F is ext-real Element of ExtREAL
superior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence F) is ext-real Element of ExtREAL
rng (superior_realsequence F) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence F)) is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
S + (lim_inf F) is ext-real Element of ExtREAL
S + (lim_sup F) is ext-real Element of ExtREAL
N1 is set
{S} is non empty V67() Element of K6(ExtREAL)
E is non empty V67() Element of K6(ExtREAL)
{S} + E is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {S} & b₂ in E ) } is set
h is ext-real Element of ExtREAL
AFN is ext-real Element of ExtREAL
h + AFN is ext-real Element of ExtREAL
J is set
(inferior_realsequence F) . J is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : I <= b₁ } is set
I is non empty V67() Element of K6(ExtREAL)
inf I is ext-real Element of ExtREAL
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : I <= b₁ } is set
(inferior_realsequence X) . I is ext-real Element of ExtREAL
n is non empty V67() Element of K6(ExtREAL)
inf n is ext-real Element of ExtREAL
e1 is set
F1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . F1 is ext-real Element of ExtREAL
F . F1 is ext-real Element of ExtREAL
H is ext-real Element of ExtREAL
S + (F . F1) is ext-real Element of ExtREAL
{S} + I is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {S} & b₂ in I ) } is set
e1 is set
F1 is ext-real Element of ExtREAL
H is ext-real Element of ExtREAL
F1 + H is ext-real Element of ExtREAL
H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . H is ext-real Element of ExtREAL
X . H is ext-real Element of ExtREAL
inf {S} is ext-real Element of ExtREAL
(inf {S}) + (inf I) is ext-real Element of ExtREAL
S + (inf I) is ext-real Element of ExtREAL
M is non empty V67() Element of K6(ExtREAL)
N1 is set
N is non empty V67() Element of K6(ExtREAL)
{S} + N is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {S} & b₂ in N ) } is set
h is ext-real Element of ExtREAL
AFN is ext-real Element of ExtREAL
h + AFN is ext-real Element of ExtREAL
J is set
(superior_realsequence F) . J is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : I <= b₁ } is set
I is non empty V67() Element of K6(ExtREAL)
sup I is ext-real Element of ExtREAL
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : I <= b₁ } is set
(superior_realsequence X) . I is ext-real Element of ExtREAL
n is non empty V67() Element of K6(ExtREAL)
sup n is ext-real Element of ExtREAL
e1 is set
F1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . F1 is ext-real Element of ExtREAL
F . F1 is ext-real Element of ExtREAL
H is ext-real Element of ExtREAL
S + (F . F1) is ext-real Element of ExtREAL
{S} + I is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {S} & b₂ in I ) } is set
e1 is set
F1 is ext-real Element of ExtREAL
H is ext-real Element of ExtREAL
F1 + H is ext-real Element of ExtREAL
H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . H is ext-real Element of ExtREAL
X . H is ext-real Element of ExtREAL
sup {S} is ext-real Element of ExtREAL
(sup {S}) + (sup I) is ext-real Element of ExtREAL
S + (sup I) is ext-real Element of ExtREAL
f is non empty V67() Element of K6(ExtREAL)
N1 is set
h is set
(inferior_realsequence X) . h is ext-real Element of ExtREAL
AFN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : AFN <= b₁ } is set
J is non empty V67() Element of K6(ExtREAL)
inf J is ext-real Element of ExtREAL
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : AFN <= b₁ } is set
(inferior_realsequence F) . AFN is ext-real Element of ExtREAL
I is non empty V67() Element of K6(ExtREAL)
inf I is ext-real Element of ExtREAL
I is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . n is ext-real Element of ExtREAL
F . n is ext-real Element of ExtREAL
e1 is ext-real Element of ExtREAL
S + (F . n) is ext-real Element of ExtREAL
{S} + I is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {S} & b₂ in I ) } is set
I is set
n is ext-real Element of ExtREAL
e1 is ext-real Element of ExtREAL
n + e1 is ext-real Element of ExtREAL
F1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . F1 is ext-real Element of ExtREAL
X . F1 is ext-real Element of ExtREAL
(inf {S}) + (inf I) is ext-real Element of ExtREAL
S + (inf I) is ext-real Element of ExtREAL
sup M is ext-real Element of ExtREAL
sup E is ext-real Element of ExtREAL
(sup {S}) + (sup E) is ext-real Element of ExtREAL
N1 is set
h is set
(superior_realsequence X) . h is ext-real Element of ExtREAL
AFN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : AFN <= b₁ } is set
J is non empty V67() Element of K6(ExtREAL)
sup J is ext-real Element of ExtREAL
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : AFN <= b₁ } is set
(superior_realsequence F) . AFN is ext-real Element of ExtREAL
I is non empty V67() Element of K6(ExtREAL)
sup I is ext-real Element of ExtREAL
I is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . n is ext-real Element of ExtREAL
F . n is ext-real Element of ExtREAL
e1 is ext-real Element of ExtREAL
S + (F . n) is ext-real Element of ExtREAL
{S} + I is non empty V67() Element of K6(ExtREAL)
{ K151(b₁,b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {S} & b₂ in I ) } is set
I is set
n is ext-real Element of ExtREAL
e1 is ext-real Element of ExtREAL
n + e1 is ext-real Element of ExtREAL
F1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . F1 is ext-real Element of ExtREAL
X . F1 is ext-real Element of ExtREAL
(sup {S}) + (sup I) is ext-real Element of ExtREAL
S + (sup I) is ext-real Element of ExtREAL
inf f is ext-real Element of ExtREAL
inf N is ext-real Element of ExtREAL
(inf {S}) + (inf N) is ext-real Element of ExtREAL
{+infty} is non empty V67() Element of K6(ExtREAL)
{-infty} is non empty V67() Element of K6(ExtREAL)
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . 0) is Element of K6(X)
K6(X) is set
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (S . 0) is Element of K6(X)
lim_inf S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim_sup S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M " {+infty} is Element of K6(X)
M " {-infty} is Element of K6(X)
M + (lim_inf S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M + (lim_sup S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M + (S . 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (M + (S . 0)) is Element of K6(X)
dom M is Element of K6(X)
(dom M) /\ (dom (S . 0)) is Element of K6(X)
(S . 0) " {+infty} is Element of K6(X)
(M " {-infty}) /\ ((S . 0) " {+infty}) is Element of K6(X)
(S . 0) " {-infty} is Element of K6(X)
(M " {+infty}) /\ ((S . 0) " {-infty}) is Element of K6(X)
((M " {-infty}) /\ ((S . 0) " {+infty})) \/ ((M " {+infty}) /\ ((S . 0) " {-infty})) is Element of K6(X)
((dom M) /\ (dom (S . 0))) \ (((M " {-infty}) /\ ((S . 0) " {+infty})) \/ ((M " {+infty}) /\ ((S . 0) " {-infty}))) is Element of K6(X)
dom (M + (lim_sup S)) is Element of K6(X)
dom (lim_sup S) is Element of K6(X)
(dom M) /\ (dom (lim_sup S)) is Element of K6(X)
(lim_sup S) " {+infty} is Element of K6(X)
(M " {-infty}) /\ ((lim_sup S) " {+infty}) is Element of K6(X)
(lim_sup S) " {-infty} is Element of K6(X)
(M " {+infty}) /\ ((lim_sup S) " {-infty}) is Element of K6(X)
((M " {-infty}) /\ ((lim_sup S) " {+infty})) \/ ((M " {+infty}) /\ ((lim_sup S) " {-infty})) is Element of K6(X)
((dom M) /\ (dom (lim_sup S))) \ (((M " {-infty}) /\ ((lim_sup S) " {+infty})) \/ ((M " {+infty}) /\ ((lim_sup S) " {-infty}))) is Element of K6(X)
dom (lim_sup F) is Element of K6(X)
dom (M + (lim_inf S)) is Element of K6(X)
dom (lim_inf S) is Element of K6(X)
(dom M) /\ (dom (lim_inf S)) is Element of K6(X)
(lim_inf S) " {+infty} is Element of K6(X)
(M " {-infty}) /\ ((lim_inf S) " {+infty}) is Element of K6(X)
(lim_inf S) " {-infty} is Element of K6(X)
(M " {+infty}) /\ ((lim_inf S) " {-infty}) is Element of K6(X)
((M " {-infty}) /\ ((lim_inf S) " {+infty})) \/ ((M " {+infty}) /\ ((lim_inf S) " {-infty})) is Element of K6(X)
((dom M) /\ (dom (lim_inf S))) \ (((M " {-infty}) /\ ((lim_inf S) " {+infty})) \/ ((M " {+infty}) /\ ((lim_inf S) " {-infty}))) is Element of K6(X)
dom (lim_inf F) is Element of K6(X)
E is Element of X
(lim_inf F) . E is ext-real Element of ExtREAL
(M + (lim_inf S)) . E is ext-real Element of ExtREAL
F # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf (F # E) is ext-real Element of ExtREAL
inferior_realsequence (F # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence (F # E)) is ext-real Element of ExtREAL
rng (inferior_realsequence (F # E)) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (F # E))) is ext-real Element of ExtREAL
M . E is ext-real Element of ExtREAL
S # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(F # E) . f is ext-real Element of ExtREAL
(S # E) . f is ext-real Element of ExtREAL
(M . E) + ((S # E) . f) is ext-real Element of ExtREAL
F . f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S . f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M + (S . f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (M + (S . f)) is Element of K6(X)
(F . f) . E is ext-real Element of ExtREAL
(M + (S . f)) . E is ext-real Element of ExtREAL
(S . f) . E is ext-real Element of ExtREAL
(M . E) + ((S . f) . E) is ext-real Element of ExtREAL
(lim_inf S) . E is ext-real Element of ExtREAL
(M . E) + ((lim_inf S) . E) is ext-real Element of ExtREAL
lim_inf (S # E) is ext-real Element of ExtREAL
inferior_realsequence (S # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence (S # E)) is ext-real Element of ExtREAL
rng (inferior_realsequence (S # E)) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (S # E))) is ext-real Element of ExtREAL
E is Element of X
(lim_sup F) . E is ext-real Element of ExtREAL
(M + (lim_sup S)) . E is ext-real Element of ExtREAL
F # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_sup (F # E) is ext-real Element of ExtREAL
superior_realsequence (F # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence (F # E)) is ext-real Element of ExtREAL
rng (superior_realsequence (F # E)) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence (F # E))) is ext-real Element of ExtREAL
M . E is ext-real Element of ExtREAL
S # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(F # E) . f is ext-real Element of ExtREAL
(S # E) . f is ext-real Element of ExtREAL
(M . E) + ((S # E) . f) is ext-real Element of ExtREAL
F . f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S . f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M + (S . f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (M + (S . f)) is Element of K6(X)
(F . f) . E is ext-real Element of ExtREAL
(M + (S . f)) . E is ext-real Element of ExtREAL
(S . f) . E is ext-real Element of ExtREAL
(M . E) + ((S . f) . E) is ext-real Element of ExtREAL
(lim_sup S) . E is ext-real Element of ExtREAL
(M . E) + ((lim_sup S) . E) is ext-real Element of ExtREAL
lim_sup (S # E) is ext-real Element of ExtREAL
superior_realsequence (S # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence (S # E)) is ext-real Element of ExtREAL
rng (superior_realsequence (S # E)) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence (S # E))) is ext-real Element of ExtREAL
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(F,ExtREAL) is Relation-like ext-real-valued set
K6(K7(F,ExtREAL)) is set
S is non empty Relation-like F -defined ExtREAL -valued Function-like total V41(F, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(F,ExtREAL))
M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M - E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(- 1) (#) E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M + (- E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(F,ExtREAL) is Relation-like ext-real-valued set
K6(K7(F,ExtREAL)) is set
S is non empty Relation-like F -defined ExtREAL -valued Function-like total V41(F, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(F,ExtREAL))
M is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom M is Element of K6(X)
E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom E is Element of K6(X)
(dom M) /\ (dom E) is Element of K6(X)
M - E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (S,(M - E)) is ext-real Element of ExtREAL
- E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(- 1) (#) E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (- E) is Element of K6(X)
(dom M) /\ (dom (- E)) is Element of K6(X)
M + (- E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (S,(M + (- E))) is ext-real Element of ExtREAL
f is Element of F
M | f is Relation-like X -defined f -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (S,(M | f)) is ext-real Element of ExtREAL
(- E) | f is Relation-like X -defined f -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (S,((- E) | f)) is ext-real Element of ExtREAL
(Integral (S,(M | f))) + (Integral (S,((- E) | f))) is ext-real Element of ExtREAL
X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_sup X is ext-real Element of ExtREAL
superior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence X) is ext-real Element of ExtREAL
rng (superior_realsequence X) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence X)) is ext-real Element of ExtREAL
- (lim_sup X) is ext-real Element of ExtREAL
lim_inf X is ext-real Element of ExtREAL
inferior_realsequence X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence X) is ext-real Element of ExtREAL
rng (inferior_realsequence X) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence X)) is ext-real Element of ExtREAL
- (lim_inf X) is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf F is ext-real Element of ExtREAL
inferior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence F) is ext-real Element of ExtREAL
rng (inferior_realsequence F) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence F)) is ext-real Element of ExtREAL
lim_sup F is ext-real Element of ExtREAL
superior_realsequence F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence F) is ext-real Element of ExtREAL
rng (superior_realsequence F) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence F)) is ext-real Element of ExtREAL
S is set
dom (inferior_realsequence F) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
M is set
(inferior_realsequence F) . M is ext-real Element of ExtREAL
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : E <= b₁ } is set
f is non empty V67() Element of K6(ExtREAL)
inf f is ext-real Element of ExtREAL
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : E <= b₁ } is set
N is ext-real Element of ExtREAL
- N is ext-real Element of ExtREAL
(superior_realsequence X) . E is ext-real Element of ExtREAL
J is set
h is non empty V67() Element of K6(ExtREAL)
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . I is ext-real Element of ExtREAL
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
F . I is ext-real Element of ExtREAL
- (F . I) is ext-real Element of ExtREAL
- (- (F . I)) is ext-real Element of ExtREAL
- (- I) is ext-real Element of ExtREAL
- f is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in f } is set
J is set
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . I is ext-real Element of ExtREAL
X . I is ext-real Element of ExtREAL
- (F . I) is ext-real Element of ExtREAL
J is non empty V67() Element of K6(ExtREAL)
sup J is ext-real Element of ExtREAL
- (- N) is ext-real Element of ExtREAL
- (rng (superior_realsequence X)) is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in rng (superior_realsequence X) } is set
S is set
dom (superior_realsequence F) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
M is set
(superior_realsequence F) . M is ext-real Element of ExtREAL
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : E <= b₁ } is set
f is non empty V67() Element of K6(ExtREAL)
sup f is ext-real Element of ExtREAL
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : E <= b₁ } is set
N is ext-real Element of ExtREAL
- N is ext-real Element of ExtREAL
(inferior_realsequence X) . E is ext-real Element of ExtREAL
J is set
h is non empty V67() Element of K6(ExtREAL)
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . I is ext-real Element of ExtREAL
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
F . I is ext-real Element of ExtREAL
- (F . I) is ext-real Element of ExtREAL
- (- (F . I)) is ext-real Element of ExtREAL
- (- I) is ext-real Element of ExtREAL
- f is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in f } is set
J is set
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . I is ext-real Element of ExtREAL
X . I is ext-real Element of ExtREAL
- (F . I) is ext-real Element of ExtREAL
J is non empty V67() Element of K6(ExtREAL)
inf J is ext-real Element of ExtREAL
- (- N) is ext-real Element of ExtREAL
- (rng (inferior_realsequence X)) is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in rng (inferior_realsequence X) } is set
S is set
M is ext-real Element of ExtREAL
- M is ext-real Element of ExtREAL
dom (superior_realsequence X) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
E is set
(superior_realsequence X) . E is ext-real Element of ExtREAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : f <= b₁ } is set
N is non empty V67() Element of K6(ExtREAL)
sup N is ext-real Element of ExtREAL
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : f <= b₁ } is set
(inferior_realsequence F) . f is ext-real Element of ExtREAL
J is set
AFN is non empty V67() Element of K6(ExtREAL)
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . I is ext-real Element of ExtREAL
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
X . I is ext-real Element of ExtREAL
- (X . I) is ext-real Element of ExtREAL
- (- (X . I)) is ext-real Element of ExtREAL
- (- I) is ext-real Element of ExtREAL
- N is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in N } is set
J is set
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . I is ext-real Element of ExtREAL
F . I is ext-real Element of ExtREAL
- (F . I) is ext-real Element of ExtREAL
N1 is ext-real Element of ExtREAL
J is non empty V67() Element of K6(ExtREAL)
inf J is ext-real Element of ExtREAL
S is set
M is ext-real Element of ExtREAL
- M is ext-real Element of ExtREAL
dom (inferior_realsequence X) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
E is set
(inferior_realsequence X) . E is ext-real Element of ExtREAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
{ (X . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : f <= b₁ } is set
N is non empty V67() Element of K6(ExtREAL)
inf N is ext-real Element of ExtREAL
{ (F . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT : f <= b₁ } is set
(superior_realsequence F) . f is ext-real Element of ExtREAL
J is set
AFN is non empty V67() Element of K6(ExtREAL)
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . I is ext-real Element of ExtREAL
X . I is ext-real Element of ExtREAL
- (F . I) is ext-real Element of ExtREAL
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
- (- I) is ext-real Element of ExtREAL
- N is non empty V67() Element of K6(ExtREAL)
{ K244(b₁) where b₁ is ext-real Element of ExtREAL : b₁ in N } is set
J is set
I is ext-real Element of ExtREAL
- I is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
X . I is ext-real Element of ExtREAL
F . I is ext-real Element of ExtREAL
- (F . I) is ext-real Element of ExtREAL
N1 is ext-real Element of ExtREAL
J is non empty V67() Element of K6(ExtREAL)
sup J is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
dom (F . 0) is Element of K6(X)
K6(X) is set
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
S . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (S . 0) is Element of K6(X)
lim_sup S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (lim_sup S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim_inf S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (lim_inf S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (lim_inf F) is Element of K6(X)
dom (lim_sup S) is Element of K6(X)
M is Element of X
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . E) is Element of K6(X)
S . E is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (S . E) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (- (S . E)) is Element of K6(X)
(F . E) . M is ext-real Element of ExtREAL
(- (S . E)) . M is ext-real Element of ExtREAL
(S . E) . M is ext-real Element of ExtREAL
- ((S . E) . M) is ext-real Element of ExtREAL
F # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(F # M) . E is ext-real Element of ExtREAL
S # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(S # M) . E is ext-real Element of ExtREAL
- ((F # M) . E) is ext-real Element of ExtREAL
M is Element of X
(lim_inf F) . M is ext-real Element of ExtREAL
F # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf (F # M) is ext-real Element of ExtREAL
inferior_realsequence (F # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence (F # M)) is ext-real Element of ExtREAL
rng (inferior_realsequence (F # M)) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (F # M))) is ext-real Element of ExtREAL
dom (- (lim_sup S)) is Element of K6(X)
(- (lim_sup S)) . M is ext-real Element of ExtREAL
(lim_sup S) . M is ext-real Element of ExtREAL
- ((lim_sup S) . M) is ext-real Element of ExtREAL
S # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(S # M) . E is ext-real Element of ExtREAL
(F # M) . E is ext-real Element of ExtREAL
- ((F # M) . E) is ext-real Element of ExtREAL
lim_sup (S # M) is ext-real Element of ExtREAL
superior_realsequence (S # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence (S # M)) is ext-real Element of ExtREAL
rng (superior_realsequence (S # M)) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence (S # M))) is ext-real Element of ExtREAL
dom (lim_sup F) is Element of K6(X)
dom (lim_inf S) is Element of K6(X)
M is Element of X
(lim_sup F) . M is ext-real Element of ExtREAL
(- (lim_inf S)) . M is ext-real Element of ExtREAL
F # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_sup (F # M) is ext-real Element of ExtREAL
superior_realsequence (F # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence (F # M)) is ext-real Element of ExtREAL
rng (superior_realsequence (F # M)) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence (F # M))) is ext-real Element of ExtREAL
dom (- (lim_inf S)) is Element of K6(X)
(lim_inf S) . M is ext-real Element of ExtREAL
- ((lim_inf S) . M) is ext-real Element of ExtREAL
S # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(S # M) . E is ext-real Element of ExtREAL
(F # M) . E is ext-real Element of ExtREAL
- ((F # M) . E) is ext-real Element of ExtREAL
lim_inf (S # M) is ext-real Element of ExtREAL
inferior_realsequence (S # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence (S # M)) is ext-real Element of ExtREAL
rng (inferior_realsequence (S # M)) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (S # M))) is ext-real Element of ExtREAL
dom (- (lim_inf S)) is Element of K6(X)
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K6(X) is set
K6(K6(X)) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . 0) is Element of K6(X)
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(lim_inf F).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(lim_sup F).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is Relation-like ext-real-valued set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V41(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . N is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . N) is Element of K6(X)
N1 is Element of X
|.(F . N).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(F . N).| is Element of K6(X)
|.(F . N).| . N1 is ext-real Element of ExtREAL
f . N1 is ext-real Element of ExtREAL
(F . N) . N1 is ext-real Element of ExtREAL
|.((F . N) . N1).| is ext-real Element of ExtREAL
dom (lim_inf F) is Element of K6(X)
N is Element of X
f . N is ext-real Element of ExtREAL
- (f . N) is ext-real Element of ExtREAL
F # N is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(F # N) . N1 is ext-real Element of ExtREAL
F . N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . N1) is Element of K6(X)
|.(F . N1).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(F . N1).| is Element of K6(X)
|.(F . N1).| . N is ext-real Element of ExtREAL
(F . N1) . N is ext-real Element of ExtREAL
|.((F . N1) . N).| is ext-real Element of ExtREAL
N is Element of X
F # N is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
inferior_realsequence (F # N) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
f . N is ext-real Element of ExtREAL
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(inferior_realsequence (F # N)) . N1 is ext-real Element of ExtREAL
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
(inferior_realsequence (F # N)) . h is ext-real Element of ExtREAL
(F # N) . h is ext-real Element of ExtREAL
(F # N) . N1 is ext-real Element of ExtREAL
lim_inf (F # N) is ext-real Element of ExtREAL
sup (inferior_realsequence (F # N)) is ext-real Element of ExtREAL
rng (inferior_realsequence (F # N)) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (F # N))) is ext-real Element of ExtREAL
(lim_inf F) . N is ext-real Element of ExtREAL
N1 is ext-real set
rng (F # N) is non empty V50() V67() Element of K6(ExtREAL)
dom (F # N) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
- (f . N) is ext-real Element of ExtREAL
h is set
(F # N) . h is ext-real Element of ExtREAL
inf (F # N) is ext-real Element of ExtREAL
inf (rng (F # N)) is ext-real Element of ExtREAL
(F # N) ^\ 0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F # N
inf ((F # N) ^\ 0) is ext-real Element of ExtREAL
rng ((F # N) ^\ 0) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng ((F # N) ^\ 0)) is ext-real Element of ExtREAL
(inferior_realsequence (F # N)) . 0 is ext-real Element of ExtREAL
|.((lim_inf F) . N).| is ext-real Element of ExtREAL
dom (lim_sup F) is Element of K6(X)
N is Element of X
f . N is ext-real Element of ExtREAL
- (f . N) is ext-real Element of ExtREAL
F # N is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
superior_realsequence (F # N) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(superior_realsequence (F # N)) . N1 is ext-real Element of ExtREAL
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
(F # N) . h is ext-real Element of ExtREAL
(superior_realsequence (F # N)) . h is ext-real Element of ExtREAL
(F # N) . N1 is ext-real Element of ExtREAL
lim_sup (F # N) is ext-real Element of ExtREAL
inf (superior_realsequence (F # N)) is ext-real Element of ExtREAL
rng (superior_realsequence (F # N)) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence (F # N))) is ext-real Element of ExtREAL
(lim_sup F) . N is ext-real Element of ExtREAL
N1 is ext-real set
rng (F # N) is non empty V50() V67() Element of K6(ExtREAL)
dom (F # N) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
h is set
(F # N) . h is ext-real Element of ExtREAL
sup (rng (F # N)) is ext-real Element of ExtREAL
(F # N) ^\ 0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F # N
sup ((F # N) ^\ 0) is ext-real Element of ExtREAL
rng ((F # N) ^\ 0) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng ((F # N) ^\ 0)) is ext-real Element of ExtREAL
(superior_realsequence (F # N)) . 0 is ext-real Element of ExtREAL
|.((lim_sup F) . N).| is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K6(X) is set
K6(K6(X)) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . 0) is Element of K6(X)
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is Relation-like ext-real-valued set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V41(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
Integral (M,(lim_inf F)) is ext-real Element of ExtREAL
Integral (M,(lim_sup F)) is ext-real Element of ExtREAL
Integral (M,(lim F)) is ext-real Element of ExtREAL
E is Element of S
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
eq_dom (f,+infty) is Element of K6(X)
dom (lim_inf F) is Element of K6(X)
(lim_inf F) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
N is Relation-like Function-like set
dom N is set
N1 is Element of X
f . N1 is ext-real Element of ExtREAL
- (f . N1) is ext-real Element of ExtREAL
F # N1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(F # N1) . h is ext-real Element of ExtREAL
F . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . h) is Element of K6(X)
|.(F . h).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(F . h).| is Element of K6(X)
|.(F . h).| . N1 is ext-real Element of ExtREAL
(F . h) . N1 is ext-real Element of ExtREAL
|.((F . h) . N1).| is ext-real Element of ExtREAL
N1 is Element of X
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F # N1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
inferior_realsequence (F # N1) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(inferior_realsequence (F # N1)) . h is ext-real Element of ExtREAL
(F # N1) . h is ext-real Element of ExtREAL
f . N1 is ext-real Element of ExtREAL
lim_inf (F # N1) is ext-real Element of ExtREAL
sup (inferior_realsequence (F # N1)) is ext-real Element of ExtREAL
rng (inferior_realsequence (F # N1)) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (F # N1))) is ext-real Element of ExtREAL
(lim_inf F) . N1 is ext-real Element of ExtREAL
h is ext-real set
rng (F # N1) is non empty V50() V67() Element of K6(ExtREAL)
dom (F # N1) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
- (f . N1) is ext-real Element of ExtREAL
AFN is set
(F # N1) . AFN is ext-real Element of ExtREAL
inf (rng (F # N1)) is ext-real Element of ExtREAL
(F # N1) ^\ 0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F # N1
inf ((F # N1) ^\ 0) is ext-real Element of ExtREAL
rng ((F # N1) ^\ 0) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng ((F # N1) ^\ 0)) is ext-real Element of ExtREAL
(inferior_realsequence (F # N1)) . 0 is ext-real Element of ExtREAL
|.((lim_inf F) . N1).| is ext-real Element of ExtREAL
(dom f) /\ (dom (lim_inf F)) is Element of K6(X)
f + (lim_inf F) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f + (lim_inf F))) is ext-real Element of ExtREAL
f | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,f) is ext-real Element of ExtREAL
N1 is set
f " {-infty} is Element of K6(X)
f . N1 is ext-real Element of ExtREAL
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
N . N1 is set
F . N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (F . N1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N . N1 is set
F . N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (F . N1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f " {+infty} is Element of K6(X)
N1 is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N1 . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (N1 . h) is Element of K6(X)
F . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (F . h) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (f + (F . h)) is Element of K6(X)
dom (F . h) is Element of K6(X)
(dom f) /\ (dom (F . h)) is Element of K6(X)
(F . h) " {+infty} is Element of K6(X)
(f " {-infty}) /\ ((F . h) " {+infty}) is Element of K6(X)
(F . h) " {-infty} is Element of K6(X)
(f " {+infty}) /\ ((F . h) " {-infty}) is Element of K6(X)
((f " {-infty}) /\ ((F . h) " {+infty})) \/ ((f " {+infty}) /\ ((F . h) " {-infty})) is Element of K6(X)
((dom f) /\ (dom (F . h))) \ (((f " {-infty}) /\ ((F . h) " {+infty})) \/ ((f " {+infty}) /\ ((F . h) " {-infty}))) is Element of K6(X)
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N1 . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (N1 . h) is Element of K6(X)
AFN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N1 . AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (N1 . AFN) is Element of K6(X)
h is Relation-like Function-like set
dom h is set
AFN is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
AFN . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (AFN . 0) is Element of K6(X)
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . J) is Element of K6(X)
I is Element of X
|.(F . J).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(F . J).| is Element of K6(X)
|.(F . J).| . I is ext-real Element of ExtREAL
f . I is ext-real Element of ExtREAL
(F . J) . I is ext-real Element of ExtREAL
|.((F . J) . I).| is ext-real Element of ExtREAL
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
AFN . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (F . J) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I is set
dom (f + (F . J)) is Element of K6(X)
f . I is ext-real Element of ExtREAL
- (f . I) is ext-real Element of ExtREAL
I is Element of X
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(F # I) . J is ext-real Element of ExtREAL
(F . J) . I is ext-real Element of ExtREAL
(- (f . I)) + (f . I) is ext-real Element of ExtREAL
((F . J) . I) + (f . I) is ext-real Element of ExtREAL
(f + (F . J)) . I is ext-real Element of ExtREAL
dom (AFN . J) is Element of K6(X)
I is Element of S
lim_inf AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_inf AFN)) is ext-real Element of ExtREAL
J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf J is ext-real Element of ExtREAL
inferior_realsequence J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence J) is ext-real Element of ExtREAL
rng (inferior_realsequence J) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence J)) is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
I . n is ext-real Element of ExtREAL
F . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(F . n)) is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
AFN . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (F . n) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . n) is Element of K6(X)
(dom f) /\ (dom (F . n)) is Element of K6(X)
Integral (M,(AFN . n)) is ext-real Element of ExtREAL
(F . n) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I . n is ext-real Element of ExtREAL
(Integral (M,f)) + (I . n) is ext-real Element of ExtREAL
e1 is Element of S
f | e1 is Relation-like X -defined e1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f | e1)) is ext-real Element of ExtREAL
(F . n) | e1 is Relation-like X -defined e1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((F . n) | e1)) is ext-real Element of ExtREAL
(Integral (M,(f | e1))) + (Integral (M,((F . n) | e1))) is ext-real Element of ExtREAL
J . n is ext-real Element of ExtREAL
lim_inf I is ext-real Element of ExtREAL
inferior_realsequence I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence I) is ext-real Element of ExtREAL
rng (inferior_realsequence I) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence I)) is ext-real Element of ExtREAL
(Integral (M,f)) + (lim_inf I) is ext-real Element of ExtREAL
(Integral (M,f)) + (Integral (M,(lim_inf F))) is ext-real Element of ExtREAL
n is Element of S
f | n is Relation-like X -defined n -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f | n)) is ext-real Element of ExtREAL
(lim_inf F) | n is Relation-like X -defined n -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((lim_inf F) | n)) is ext-real Element of ExtREAL
(Integral (M,(f | n))) + (Integral (M,((lim_inf F) | n))) is ext-real Element of ExtREAL
(lim_inf I) + (Integral (M,f)) is ext-real Element of ExtREAL
((lim_inf I) + (Integral (M,f))) - (Integral (M,f)) is ext-real Element of ExtREAL
K152((Integral (M,f))) is ext-real set
K151(((lim_inf I) + (Integral (M,f))),K152((Integral (M,f)))) is ext-real set
(Integral (M,f)) - (Integral (M,f)) is ext-real Element of ExtREAL
K151((Integral (M,f)),K152((Integral (M,f)))) is ext-real set
(lim_inf I) + ((Integral (M,f)) - (Integral (M,f))) is ext-real Element of ExtREAL
(lim_inf I) + 0. is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
h . n is set
F . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f - (F . n) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
h . n is set
F . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f - (F . n) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (lim_sup F) is Element of K6(X)
n is Element of X
f . n is ext-real Element of ExtREAL
- (f . n) is ext-real Element of ExtREAL
F # n is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
superior_realsequence (F # n) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(superior_realsequence (F # n)) . e1 is ext-real Element of ExtREAL
(F # n) . e1 is ext-real Element of ExtREAL
lim_sup (F # n) is ext-real Element of ExtREAL
inf (superior_realsequence (F # n)) is ext-real Element of ExtREAL
rng (superior_realsequence (F # n)) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence (F # n))) is ext-real Element of ExtREAL
(lim_sup F) . n is ext-real Element of ExtREAL
e1 is ext-real set
rng (F # n) is non empty V50() V67() Element of K6(ExtREAL)
dom (F # n) is non empty V66() V67() V68() V69() V70() V71() Element of K6(NAT)
F1 is set
(F # n) . F1 is ext-real Element of ExtREAL
sup (rng (F # n)) is ext-real Element of ExtREAL
(F # n) ^\ 0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F # n
sup ((F # n) ^\ 0) is ext-real Element of ExtREAL
rng ((F # n) ^\ 0) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng ((F # n) ^\ 0)) is ext-real Element of ExtREAL
(superior_realsequence (F # n)) . 0 is ext-real Element of ExtREAL
|.((lim_sup F) . n).| is ext-real Element of ExtREAL
(dom f) /\ (dom (lim_sup F)) is Element of K6(X)
f - (lim_sup F) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f - (lim_sup F))) is ext-real Element of ExtREAL
- (lim_sup F) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (Integral (M,(lim_sup F))) is ext-real Element of ExtREAL
e1 is V11() real ext-real Element of REAL
- e1 is V11() real ext-real Element of REAL
F1 is Relation-like Function-like set
dom F1 is set
H is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
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 K6(K7(X,ExtREAL))
dom (H . H) is Element of K6(X)
F . H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f - (F . H) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (f - (F . H)) is Element of K6(X)
dom (F . H) is Element of K6(X)
E /\ E is M9(X,S)
(F . H) " {+infty} is Element of K6(X)
{} /\ ((F . H) " {+infty}) is Relation-like V66() V67() V68() V69() V70() V71() Element of K6(X)
(F . H) " {-infty} is Element of K6(X)
{} /\ ((F . H) " {-infty}) is Relation-like V66() V67() V68() V69() V70() V71() Element of K6(X)
({} /\ ((F . H) " {+infty})) \/ ({} /\ ((F . H) " {-infty})) is Relation-like V66() V67() V68() V69() V70() V71() Element of K6(X)
(E /\ E) \ (({} /\ ((F . H) " {+infty})) \/ ({} /\ ((F . H) " {-infty}))) is Element of K6(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 K6(K7(X,ExtREAL))
dom (H . H) is Element of K6(X)
IH is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
H . IH is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (H . IH) is Element of K6(X)
H is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
IH is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
H . IH is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . IH is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f - (F . IH) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F1 is Element of X
dom (F . IH) is Element of K6(X)
F # F1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(F # F1) . IH is ext-real Element of ExtREAL
f . F1 is ext-real Element of ExtREAL
(F . IH) . F1 is ext-real Element of ExtREAL
dom (H . IH) is Element of K6(X)
F1 is Element of S
H . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (H . 0) is Element of K6(X)
lim_inf H is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_inf H)) is ext-real Element of ExtREAL
IH is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf IH is ext-real Element of ExtREAL
inferior_realsequence IH is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence IH) is ext-real Element of ExtREAL
rng (inferior_realsequence IH) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence IH)) is ext-real Element of ExtREAL
F1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F1 . F1 is set
F . F1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (F . F1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F1 is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F1 . F1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . F1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (F . F1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F1 . I1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . I1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (F . I1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F1 . I1) is Element of K6(X)
dom (F . I1) is Element of K6(X)
F1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F1 . F1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . F1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (F . F1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F1 . F1) is Element of K6(X)
dom (F . F1) is Element of K6(X)
Integral (M,(- (lim_sup F))) is ext-real Element of ExtREAL
(- 1) (#) (lim_sup F) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((- 1) (#) (lim_sup F))) is ext-real Element of ExtREAL
I1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
H . I1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . I1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f - (F . I1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (F . I1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (- (F . I1)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F1 is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F1 . I1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (F1 . I1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F1 . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (F . 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F1 . 0) is Element of K6(X)
lim_inf F1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (lim_inf F1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f + (- (lim_sup F)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (- (lim_sup F)) is Element of K6(X)
(- (lim_sup F)) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
I1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
I1 . x is ext-real Element of ExtREAL
I . x is ext-real Element of ExtREAL
- (I . x) is ext-real Element of ExtREAL
lim_inf I1 is ext-real Element of ExtREAL
inferior_realsequence I1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence I1) is ext-real Element of ExtREAL
rng (inferior_realsequence I1) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence I1)) is ext-real Element of ExtREAL
- (lim_inf I1) is ext-real Element of ExtREAL
lim_sup I is ext-real Element of ExtREAL
superior_realsequence I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence I) is ext-real Element of ExtREAL
rng (superior_realsequence I) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence I)) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . x is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
- (F . x) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(- (F . x))) is ext-real Element of ExtREAL
(- 1) (#) (F . x) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((- 1) (#) (F . x))) is ext-real Element of ExtREAL
R_EAL (- 1) is ext-real Element of ExtREAL
Integral (M,(F . x)) is ext-real Element of ExtREAL
(R_EAL (- 1)) * (Integral (M,(F . x))) is ext-real Element of ExtREAL
dom (F . x) is Element of K6(X)
dom (- (F . x)) is Element of K6(X)
(- (F . x)) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
H . x is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f - (F . x) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(dom f) /\ (dom (F . x)) is Element of K6(X)
Integral (M,(H . x)) is ext-real Element of ExtREAL
I . x is ext-real Element of ExtREAL
(R_EAL (- 1)) * (I . x) is ext-real Element of ExtREAL
In is V11() real ext-real Element of REAL
(- 1) * In is V11() real ext-real Element of REAL
- (I . x) is ext-real Element of ExtREAL
- In is V11() real ext-real Element of REAL
(Integral (M,f)) + (- (I . x)) is ext-real Element of ExtREAL
c₂₆ is Element of S
f | c₂₆ is Relation-like X -defined c₂₆ -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f | c₂₆)) is ext-real Element of ExtREAL
(- (F . x)) | c₂₆ is Relation-like X -defined c₂₆ -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((- (F . x)) | c₂₆)) is ext-real Element of ExtREAL
(Integral (M,(f | c₂₆))) + (Integral (M,((- (F . x)) | c₂₆))) is ext-real Element of ExtREAL
IH . x is ext-real Element of ExtREAL
I1 . x is ext-real Element of ExtREAL
(Integral (M,f)) + (I1 . x) is ext-real Element of ExtREAL
(Integral (M,f)) + (lim_inf I1) is ext-real Element of ExtREAL
(R_EAL (- 1)) * (Integral (M,(lim_sup F))) is ext-real Element of ExtREAL
(Integral (M,f)) + ((R_EAL (- 1)) * (Integral (M,(lim_sup F)))) is ext-real Element of ExtREAL
- (lim_sup I) is ext-real Element of ExtREAL
(Integral (M,f)) + (- (lim_sup I)) is ext-real Element of ExtREAL
x is Element of S
f | x is Relation-like X -defined x -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f | x)) is ext-real Element of ExtREAL
(- (lim_sup F)) | x is Relation-like X -defined x -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((- (lim_sup F)) | x)) is ext-real Element of ExtREAL
(Integral (M,(f | x))) + (Integral (M,((- (lim_sup F)) | x))) is ext-real Element of ExtREAL
(- (lim_sup I)) + (Integral (M,f)) is ext-real Element of ExtREAL
((- (lim_sup I)) + (Integral (M,f))) - (Integral (M,f)) is ext-real Element of ExtREAL
K151(((- (lim_sup I)) + (Integral (M,f))),K152((Integral (M,f)))) is ext-real set
(- (lim_sup I)) + ((Integral (M,f)) - (Integral (M,f))) is ext-real Element of ExtREAL
(- (lim_sup I)) + 0. is ext-real Element of ExtREAL
(- 1) * e1 is V11() real ext-real Element of REAL
dom (lim F) is Element of K6(X)
x is Element of X
(lim F) . x is ext-real Element of ExtREAL
(lim_inf F) . x is ext-real Element of ExtREAL
F # x is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
x is Element of X
(lim F) . x is ext-real Element of ExtREAL
(lim_sup F) . x is ext-real Element of ExtREAL
F # x is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim I is ext-real Element of ExtREAL
x is Element of X
F # x is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K6(X) is set
K6(K6(X)) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . 0) is Element of K6(X)
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
lim F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is Relation-like ext-real-valued set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V41(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
Integral (M,(lim_inf F)) is ext-real Element of ExtREAL
Integral (M,(lim_sup F)) is ext-real Element of ExtREAL
Integral (M,(lim F)) is ext-real Element of ExtREAL
E is Element of S
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
eq_dom (f,+infty) is Element of K6(X)
N is set
E /\ (eq_dom (f,+infty)) is Element of K6(X)
N1 is Element of S
N is Element of S
E \ N is M9(X,S)
N1 is Element of S
h is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
AFN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . AFN) is Element of K6(X)
(F . AFN) | N1 is Relation-like X -defined N1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((F . AFN) | N1) is Element of K6(X)
h . AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (h . AFN) is Element of K6(X)
h . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (h . 0) is Element of K6(X)
AFN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
h . AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (h . AFN) is Element of K6(X)
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
h . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (h . J) is Element of K6(X)
f | N1 is Relation-like X -defined N1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I is Element of X
(f | N1) . I is ext-real Element of ExtREAL
f . I is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . I) is Element of K6(X)
|.(F . I).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(F . I).| is Element of K6(X)
|.(F . I).| . I is ext-real Element of ExtREAL
(F . I) . I is ext-real Element of ExtREAL
|.((F . I) . I).| is ext-real Element of ExtREAL
AFN is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
AFN . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (AFN . I) is Element of K6(X)
|.(AFN . I).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(AFN . I).| is Element of K6(X)
(F . I) | N1 is Relation-like X -defined N1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(AFN . I) . I is ext-real Element of ExtREAL
|.(AFN . I).| . I is ext-real Element of ExtREAL
dom (lim F) is Element of K6(X)
dom (lim_inf F) is Element of K6(X)
I is Element of X
lim_inf AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (lim_inf AFN) is Element of K6(X)
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . I) | N1 is Relation-like X -defined N1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((F . I) | N1) . I is ext-real Element of ExtREAL
(F . I) . I is ext-real Element of ExtREAL
AFN . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(AFN . I) . I is ext-real Element of ExtREAL
AFN # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(AFN # I) . I is ext-real Element of ExtREAL
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(F # I) . I is ext-real Element of ExtREAL
lim_inf (F # I) is ext-real Element of ExtREAL
inferior_realsequence (F # I) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence (F # I)) is ext-real Element of ExtREAL
rng (inferior_realsequence (F # I)) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (F # I))) is ext-real Element of ExtREAL
(lim_inf F) . I is ext-real Element of ExtREAL
(lim_inf AFN) . I is ext-real Element of ExtREAL
(lim_inf F) | (E \ N) is Relation-like X -defined E \ N -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((lim_inf F) | (E \ N)) . I is ext-real Element of ExtREAL
dom ((lim_inf F) | (E \ N)) is Element of K6(X)
dom (lim_sup F) is Element of K6(X)
I is Element of X
lim_sup AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (lim_sup AFN) is Element of K6(X)
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . I) | N1 is Relation-like X -defined N1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((F . I) | N1) . I is ext-real Element of ExtREAL
(F . I) . I is ext-real Element of ExtREAL
AFN . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(AFN . I) . I is ext-real Element of ExtREAL
AFN # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(AFN # I) . I is ext-real Element of ExtREAL
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(F # I) . I is ext-real Element of ExtREAL
lim_sup (F # I) is ext-real Element of ExtREAL
superior_realsequence (F # I) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence (F # I)) is ext-real Element of ExtREAL
rng (superior_realsequence (F # I)) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence (F # I))) is ext-real Element of ExtREAL
(lim_sup F) . I is ext-real Element of ExtREAL
(lim_sup AFN) . I is ext-real Element of ExtREAL
(lim_sup F) | (E \ N) is Relation-like X -defined E \ N -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((lim_sup F) | (E \ N)) . I is ext-real Element of ExtREAL
dom ((lim_sup F) | (E \ N)) is Element of K6(X)
dom (f | N1) is Element of K6(X)
eq_dom ((f | N1),+infty) is Element of K6(X)
I is set
I is Element of X
(f | N1) . I is ext-real Element of ExtREAL
n is ext-real Element of ExtREAL
f . I is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
AFN . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . I) is Element of K6(X)
(dom (F . I)) /\ N1 is Element of K6(X)
(F . I) | N1 is Relation-like X -defined N1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_inf AFN)) is ext-real Element of ExtREAL
Integral (M,(lim_sup AFN)) is ext-real Element of ExtREAL
lim AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim AFN)) is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf I is ext-real Element of ExtREAL
inferior_realsequence I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence I) is ext-real Element of ExtREAL
rng (inferior_realsequence I) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence I)) is ext-real Element of ExtREAL
lim_sup I is ext-real Element of ExtREAL
superior_realsequence I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence I) is ext-real Element of ExtREAL
rng (superior_realsequence I) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence I)) is ext-real Element of ExtREAL
lim I is ext-real Element of ExtREAL
f " {+infty} is Element of K6(X)
M . N is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
I . I is ext-real Element of ExtREAL
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(F . I)) is ext-real Element of ExtREAL
dom (F . I) is Element of K6(X)
|.(F . I).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . I) | N is Relation-like X -defined N -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((F . I) | N)) is ext-real Element of ExtREAL
(F . I) | N1 is Relation-like X -defined N1 -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((F . I) | N1)) is ext-real Element of ExtREAL
(Integral (M,((F . I) | N))) + (Integral (M,((F . I) | N1))) is ext-real Element of ExtREAL
0. + (Integral (M,((F . I) | N1))) is ext-real Element of ExtREAL
AFN . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(AFN . I)) is ext-real Element of ExtREAL
Integral (M,((lim_inf F) | (E \ N))) is ext-real Element of ExtREAL
Integral (M,((lim_sup F) | (E \ N))) is ext-real Element of ExtREAL
I is Element of X
(lim F) . I is ext-real Element of ExtREAL
(lim_inf F) . I is ext-real Element of ExtREAL
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
I is Element of X
(lim F) . I is ext-real Element of ExtREAL
(lim_sup F) . I is ext-real Element of ExtREAL
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
I is Element of X
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K6(X) is set
K6(K6(X)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
dom (F . 0) is Element of K6(X)
lim F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is Relation-like ext-real-valued set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V41(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
Integral (M,(lim F)) is ext-real Element of ExtREAL
E is Element of S
(F . 0) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((F . 0) | E)) is ext-real Element of ExtREAL
|.(F . 0).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(F . 0).| is Element of K6(X)
f is Element of X
(F . 0) . f is ext-real Element of ExtREAL
|.(F . 0).| . f is ext-real Element of ExtREAL
|.((F . 0) . f).| is ext-real Element of ExtREAL
Integral (M,(F . 0)) is ext-real Element of ExtREAL
integral+ (M,(F . 0)) is ext-real Element of ExtREAL
integral+ (M,|.(F . 0).|) is ext-real Element of ExtREAL
max+ (F . 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
max- (F . 0) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (max- (F . 0)) is Element of K6(X)
f is set
(max- (F . 0)) . f is ext-real Element of ExtREAL
f is Element of X
(F . 0) . f is ext-real Element of ExtREAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . N is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(F . N).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(F . N).| . f is ext-real Element of ExtREAL
(F . N) . f is ext-real Element of ExtREAL
|.((F . N) . f).| is ext-real Element of ExtREAL
dom (F . N) is Element of K6(X)
dom |.(F . N).| is Element of K6(X)
f is Element of X
F # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . N is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . N) . f is ext-real Element of ExtREAL
F . N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . N1) . f is ext-real Element of ExtREAL
(F # f) . N is ext-real Element of ExtREAL
(F # f) . N1 is ext-real Element of ExtREAL
dom (max+ (F . 0)) is Element of K6(X)
(max+ (F . 0)) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
f is set
(max+ (F . 0)) . f is ext-real Element of ExtREAL
(max+ (F . 0)) + (max- (F . 0)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((max+ (F . 0)) + (max- (F . 0))) is Element of K6(X)
(dom (max+ (F . 0))) /\ (dom (max- (F . 0))) is Element of K6(X)
(max- (F . 0)) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max+ (F . 0)) + (max- (F . 0)))) is ext-real Element of ExtREAL
integral+ (M,(max+ (F . 0))) is ext-real Element of ExtREAL
integral+ (M,(max- (F . 0))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (F . 0)))) + (integral+ (M,(max- (F . 0)))) is ext-real Element of ExtREAL
f is Element of S
(max+ (F . 0)) | f is Relation-like X -defined f -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max+ (F . 0)) | f)) is ext-real Element of ExtREAL
(max- (F . 0)) | f is Relation-like X -defined f -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max- (F . 0)) | f)) is ext-real Element of ExtREAL
(integral+ (M,((max+ (F . 0)) | f))) + (integral+ (M,((max- (F . 0)) | f))) is ext-real Element of ExtREAL
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_inf F)) is ext-real Element of ExtREAL
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_sup F)) is ext-real Element of ExtREAL
f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf f is ext-real Element of ExtREAL
inferior_realsequence f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence f) is ext-real Element of ExtREAL
rng (inferior_realsequence f) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence f)) is ext-real Element of ExtREAL
lim_sup f is ext-real Element of ExtREAL
superior_realsequence f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence f) is ext-real Element of ExtREAL
rng (superior_realsequence f) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence f)) is ext-real Element of ExtREAL
N is Element of X
F # N is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim f is ext-real Element of ExtREAL
X is set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K6(X) is set
K6(K6(X)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
dom (F . 0) is Element of K6(X)
lim F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is Relation-like ext-real-valued set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V41(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
Integral (M,(lim F)) is ext-real Element of ExtREAL
E is Element of S
M . E is ext-real Element of ExtREAL
f is V11() real ext-real set
max (f,1) is V11() real ext-real set
N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom N1 is Element of K6(X)
|.N1.| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.N1.| is Element of K6(X)
R_EAL (max (f,1)) is ext-real Element of ExtREAL
(R_EAL (max (f,1))) * +infty is ext-real Element of ExtREAL
h is set
N1 . h is ext-real Element of ExtREAL
Integral (M,N1) is ext-real Element of ExtREAL
integral' (M,N1) is ext-real Element of ExtREAL
M . (dom N1) is ext-real Element of ExtREAL
(R_EAL (max (f,1))) * (M . (dom N1)) is ext-real Element of ExtREAL
h is Element of X
N1 . h is ext-real Element of ExtREAL
|.N1.| . h is ext-real Element of ExtREAL
|.(N1 . h).| is ext-real Element of ExtREAL
integral+ (M,N1) is ext-real Element of ExtREAL
integral+ (M,|.N1.|) is ext-real Element of ExtREAL
max+ N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (max+ N1) is Element of K6(X)
(max+ N1) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
max- N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (max- N1) is Element of K6(X)
h is set
(max- N1) . h is ext-real Element of ExtREAL
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
AFN is set
(F . h) . AFN is ext-real Element of ExtREAL
|.((F . h) . AFN).| is ext-real Element of ExtREAL
h is Element of X
N1 . h is ext-real Element of ExtREAL
AFN is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . AFN is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(F . AFN).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(F . AFN).| . h is ext-real Element of ExtREAL
dom (F . AFN) is Element of K6(X)
dom |.(F . AFN).| is Element of K6(X)
(F . AFN) . h is ext-real Element of ExtREAL
|.((F . AFN) . h).| is ext-real Element of ExtREAL
h is set
(max+ N1) . h is ext-real Element of ExtREAL
(max+ N1) + (max- N1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((max+ N1) + (max- N1)) is Element of K6(X)
(dom (max+ N1)) /\ (dom (max- N1)) is Element of K6(X)
(max- N1) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max+ N1) + (max- N1))) is ext-real Element of ExtREAL
integral+ (M,(max+ N1)) is ext-real Element of ExtREAL
integral+ (M,(max- N1)) is ext-real Element of ExtREAL
(integral+ (M,(max+ N1))) + (integral+ (M,(max- N1))) is ext-real Element of ExtREAL
h is Element of S
(max+ N1) | h is Relation-like X -defined h -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max+ N1) | h)) is ext-real Element of ExtREAL
(max- N1) | h is Relation-like X -defined h -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max- N1) | h)) is ext-real Element of ExtREAL
(integral+ (M,((max+ N1) | h))) + (integral+ (M,((max- N1) | h))) is ext-real Element of ExtREAL
dom (lim F) is Element of K6(X)
lim_inf F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
h is Element of X
(lim F) . h is ext-real Element of ExtREAL
(lim_inf F) . h is ext-real Element of ExtREAL
F # h is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
dom (lim_inf F) is Element of K6(X)
Integral (M,(lim_inf F)) is ext-real Element of ExtREAL
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_sup F)) is ext-real Element of ExtREAL
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . h) is Element of K6(X)
|.(F . h).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(lim_inf F).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
AFN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf AFN is ext-real Element of ExtREAL
inferior_realsequence AFN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence AFN) is ext-real Element of ExtREAL
rng (inferior_realsequence AFN) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence AFN)) is ext-real Element of ExtREAL
lim_sup AFN is ext-real Element of ExtREAL
superior_realsequence AFN is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence AFN) is ext-real Element of ExtREAL
rng (superior_realsequence AFN) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence AFN)) is ext-real Element of ExtREAL
J is Element of X
F # J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim AFN is ext-real Element of ExtREAL
X is set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . 0) is Element of K6(X)
K6(X) is set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
M is Element of X
F # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim (F # M) is ext-real Element of ExtREAL
S . M is ext-real Element of ExtREAL
f is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N1 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
F . h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . h) . M is ext-real Element of ExtREAL
((F . h) . M) - (S . M) is ext-real Element of ExtREAL
K152((S . M)) is ext-real set
K151(((F . h) . M),K152((S . M))) is ext-real set
|.(((F . h) . M) - (S . M)).| is ext-real Element of ExtREAL
(F # M) . h is ext-real Element of ExtREAL
E is V11() real ext-real set
R_EAL E is ext-real Element of ExtREAL
((F # M) . h) - (R_EAL E) is ext-real Element of ExtREAL
K152((R_EAL E)) is ext-real set
K151(((F # M) . h),K152((R_EAL E))) is ext-real set
|.(((F # M) . h) - (R_EAL 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
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . N1) . M is ext-real Element of ExtREAL
((F . N1) . M) - (S . M) is ext-real Element of ExtREAL
K152((S . M)) is ext-real set
K151(((F . N1) . M),K152((S . M))) is ext-real set
|.(((F . N1) . M) - (S . M)).| is ext-real Element of ExtREAL
- (((F . N1) . M) - (S . M)) is ext-real Element of ExtREAL
|.(- (((F . N1) . M) - (S . M))).| is ext-real Element of ExtREAL
(F # M) . N1 is ext-real Element of ExtREAL
R_EAL E is ext-real Element of ExtREAL
((F # M) . N1) - (S . M) is ext-real Element of ExtREAL
K151(((F # M) . N1),K152((S . M))) is ext-real set
- (((F # M) . N1) - (S . M)) is ext-real Element of ExtREAL
(S . M) - ((F # M) . N1) is ext-real Element of ExtREAL
K152(((F # M) . N1)) is ext-real set
K151((S . M),K152(((F # M) . N1))) is ext-real set
E is V11() real ext-real set
- E is V11() real ext-real set
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V66() V67() V68() V69() V70() V71() V72() Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . N1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . N1) . M is ext-real Element of ExtREAL
((F . N1) . M) - (S . M) is ext-real Element of ExtREAL
K152((S . M)) is ext-real set
K151(((F . N1) . M),K152((S . M))) is ext-real set
|.(((F . N1) . M) - (S . M)).| is ext-real Element of ExtREAL
(F # M) . N1 is ext-real Element of ExtREAL
R_EAL (- E) is ext-real Element of ExtREAL
((F # M) . N1) - (S . M) is ext-real Element of ExtREAL
K151(((F # M) . N1),K152((S . M))) is ext-real set
X is non empty set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K6(X) is set
K6(K6(X)) is set
K7(X,ExtREAL) is Relation-like ext-real-valued set
K6(K7(X,ExtREAL)) is set
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . 0) is Element of K6(X)
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is Relation-like ext-real-valued set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V41(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
M . E is ext-real Element of ExtREAL
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,f) is ext-real Element of ExtREAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
1 / 2 is V11() real ext-real non negative Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
1. is ext-real Element of ExtREAL
h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom h is Element of K6(X)
max- h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
AFN is set
h . AFN is ext-real Element of ExtREAL
Integral (M,h) is ext-real Element of ExtREAL
integral' (M,h) is ext-real Element of ExtREAL
F . N is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(F . N).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . N) is Element of K6(X)
dom |.(F . N).| is Element of K6(X)
J is set
|.(F . N).| . J is ext-real Element of ExtREAL
(F . N) . J is ext-real Element of ExtREAL
|.((F . N) . J).| is ext-real Element of ExtREAL
|.(F . N).| + h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (|.(F . N).| + h) is Element of K6(X)
(dom |.(F . N).|) /\ (dom h) is Element of K6(X)
J is set
(F . N) . J is ext-real Element of ExtREAL
f . J is ext-real Element of ExtREAL
((F . N) . J) - (f . J) is ext-real Element of ExtREAL
K152((f . J)) is ext-real set
K151(((F . N) . J),K152((f . J))) is ext-real set
|.(((F . N) . J) - (f . J)).| is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
J is set
F . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . I) . J is ext-real Element of ExtREAL
f . J is ext-real Element of ExtREAL
((F . I) . J) - (f . J) is ext-real Element of ExtREAL
K152((f . J)) is ext-real set
K151(((F . I) . J),K152((f . J))) is ext-real set
|.(((F . I) . J) - (f . J)).| is ext-real Element of ExtREAL
(F . N) . J is ext-real Element of ExtREAL
((F . N) . J) - (f . J) is ext-real Element of ExtREAL
K151(((F . N) . J),K152((f . J))) is ext-real set
|.(((F . N) . J) - (f . J)).| is ext-real Element of ExtREAL
- 1. is ext-real Element of ExtREAL
|.((F . I) . J).| is ext-real Element of ExtREAL
|.((F . N) . J).| is ext-real Element of ExtREAL
|.((F . N) . J).| + 1. is ext-real Element of ExtREAL
E /\ E is M9(X,S)
|.(F . N).| . J is ext-real Element of ExtREAL
h . J is ext-real Element of ExtREAL
(|.(F . N).| . J) + (h . J) is ext-real Element of ExtREAL
(|.(F . N).| + h) . J is ext-real Element of ExtREAL
(|.(F . N).| . J) + 1. is ext-real Element of ExtREAL
dom (F . I) is Element of K6(X)
|.(F . I).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.(F . I).| is Element of K6(X)
(f . J) - ((F . N) . J) is ext-real Element of ExtREAL
K152(((F . N) . J)) is ext-real set
K151((f . J),K152(((F . N) . J))) is ext-real set
|.((f . J) - ((F . N) . J)).| is ext-real Element of ExtREAL
|.((F . I) . J).| - |.((F . N) . J).| is ext-real Element of ExtREAL
K152(|.((F . N) . J).|) is ext-real set
K151(|.((F . I) . J).|,K152(|.((F . N) . J).|)) is ext-real set
((F . I) . J) - ((F . N) . J) is ext-real Element of ExtREAL
K151(((F . I) . J),K152(((F . N) . J))) is ext-real set
|.(((F . I) . J) - ((F . N) . J)).| is ext-real Element of ExtREAL
n is V11() real ext-real Element of REAL
(1 / 2) + (1 / 2) is V11() real ext-real non negative Element of REAL
I is V11() real ext-real Element of REAL
I + n is V11() real ext-real Element of REAL
|.(((F . I) . J) - (f . J)).| + |.((f . J) - ((F . N) . J)).| is ext-real Element of ExtREAL
- (f . J) is ext-real Element of ExtREAL
(- (f . J)) + (f . J) is ext-real Element of ExtREAL
((F . I) . J) + ((- (f . J)) + (f . J)) is ext-real Element of ExtREAL
(((F . I) . J) + ((- (f . J)) + (f . J))) - ((F . N) . J) is ext-real Element of ExtREAL
K151((((F . I) . J) + ((- (f . J)) + (f . J))),K152(((F . N) . J))) is ext-real set
((F . I) . J) + (- (f . J)) is ext-real Element of ExtREAL
(((F . I) . J) + (- (f . J))) + (f . J) is ext-real Element of ExtREAL
((((F . I) . J) + (- (f . J))) + (f . J)) - ((F . N) . J) is ext-real Element of ExtREAL
K151(((((F . I) . J) + (- (f . J))) + (f . J)),K152(((F . N) . J))) is ext-real set
(((F . I) . J) - (f . J)) + ((f . J) - ((F . N) . J)) is ext-real Element of ExtREAL
|.(F . I).| . J is ext-real Element of ExtREAL
N1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F ^\ N1 is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued PFuncs (X,ExtREAL) -valued Function-like total V41( NAT , PFuncs (X,ExtREAL)) V41( NAT , PFuncs (X,ExtREAL)) with_the_same_dom subsequence of F
J is Element of X
(|.(F . N).| + h) . J is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(F ^\ N1) . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.((F ^\ N1) . I).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.((F ^\ N1) . I).| . J is ext-real Element of ExtREAL
I + N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . (I + N) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
max+ h is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (max- h) is Element of K6(X)
J is set
(max- h) . J is ext-real Element of ExtREAL
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (F . J) is Element of K6(X)
I is Element of S
(F ^\ N1) . 0 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
0 + N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . (0 + N) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((F ^\ N1) . 0) is Element of K6(X)
J is Element of X
dom f is Element of K6(X)
lim F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (lim F) is Element of K6(X)
F # J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim (F # J) is ext-real Element of ExtREAL
f . J is ext-real Element of ExtREAL
(lim F) . J is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
(R_EAL 1) * +infty is ext-real Element of ExtREAL
J is Element of X
|.h.| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom |.h.| is Element of K6(X)
h . J is ext-real Element of ExtREAL
|.(h . J).| is ext-real Element of ExtREAL
|.h.| . J is ext-real Element of ExtREAL
integral+ (M,h) is ext-real Element of ExtREAL
M . (dom h) is ext-real Element of ExtREAL
(R_EAL 1) * (M . (dom h)) is ext-real Element of ExtREAL
integral+ (M,|.h.|) is ext-real Element of ExtREAL
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(F ^\ N1) . J is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
J + N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
F . (J + N) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
J is Element of X
(F ^\ N1) # J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
F # J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim (F # J) is ext-real Element of ExtREAL
lim ((F ^\ N1) # J) is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
((F ^\ N1) # J) . I is ext-real Element of ExtREAL
(F ^\ N1) . I is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
((F ^\ N1) . I) . J is ext-real Element of ExtREAL
I + N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . (I + N) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
(F . (I + N)) . J is ext-real Element of ExtREAL
(F # J) . (I + N) is ext-real Element of ExtREAL
(F # J) ^\ N1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of F # J
((F # J) ^\ N1) . I is ext-real Element of ExtREAL
lim ((F # J) ^\ N1) is ext-real Element of ExtREAL
J is Element of X
(F ^\ N1) # J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim (F ^\ N1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (lim (F ^\ N1)) is Element of K6(X)
J is Element of X
F # J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim (F # J) is ext-real Element of ExtREAL
(F ^\ N1) # J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim ((F ^\ N1) # J) is ext-real Element of ExtREAL
(lim (F ^\ N1)) . J is ext-real Element of ExtREAL
(lim F) . J is ext-real Element of ExtREAL
(max- h) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom (max+ h) is Element of K6(X)
(max+ h) | E is Relation-like X -defined E -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
J is set
(max+ h) . J is ext-real Element of ExtREAL
(max+ h) + (max- h) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((max+ h) + (max- h)) is Element of K6(X)
(dom (max+ h)) /\ (dom (max- h)) is Element of K6(X)
integral+ (M,((max+ h) + (max- h))) is ext-real Element of ExtREAL
integral+ (M,(max+ h)) is ext-real Element of ExtREAL
integral+ (M,(max- h)) is ext-real Element of ExtREAL
(integral+ (M,(max+ h))) + (integral+ (M,(max- h))) is ext-real Element of ExtREAL
J is Element of S
(max+ h) | J is Relation-like X -defined J -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max+ h) | J)) is ext-real Element of ExtREAL
(max- h) | J is Relation-like X -defined J -defined X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,((max- h) | J)) is ext-real Element of ExtREAL
(integral+ (M,((max+ h) | J))) + (integral+ (M,((max- h) | J))) is ext-real Element of ExtREAL
lim_inf (F ^\ N1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
|.(lim_inf (F ^\ N1)).| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_inf (F ^\ N1))) is ext-real Element of ExtREAL
lim_sup (F ^\ N1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(lim_sup (F ^\ N1))) is ext-real Element of ExtREAL
Integral (M,(lim (F ^\ N1))) is ext-real Element of ExtREAL
J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim_inf J is ext-real Element of ExtREAL
inferior_realsequence J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence J) is ext-real Element of ExtREAL
rng (inferior_realsequence J) is non empty V50() V67() Element of K6(ExtREAL)
sup (rng (inferior_realsequence J)) is ext-real Element of ExtREAL
lim_sup J is ext-real Element of ExtREAL
superior_realsequence J is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence J) is ext-real Element of ExtREAL
rng (superior_realsequence J) is non empty V50() V67() Element of K6(ExtREAL)
inf (rng (superior_realsequence J)) is ext-real Element of ExtREAL
lim J is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
dom (lim_inf (F ^\ N1)) is Element of K6(X)
n is Element of X
(F ^\ N1) # n is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(lim (F ^\ N1)) . n is ext-real Element of ExtREAL
(lim_inf (F ^\ N1)) . n is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
I . n is ext-real Element of ExtREAL
F . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(F . n)) is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
(F ^\ N1) . n is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
n + N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V66() V67() V68() V69() V70() V71() V75() V76() Element of NAT
F . (n + N) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K6(K7(X,ExtREAL))
I ^\ N1 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued subsequence of I
(I ^\ N1) . n is ext-real Element of ExtREAL
I . (n + N) is ext-real Element of ExtREAL
J . n is ext-real Element of ExtREAL
Integral (M,((F ^\ N1) . n)) is ext-real Element of ExtREAL
n is Element of X
(F ^\ N1) # n is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim I is ext-real Element of ExtREAL
n is Element of X
(F ^\ N1) # n is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
Integral (M,(lim F)) is ext-real Element of ExtREAL
n is Element of X
(F ^\ N1) # n is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V41( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))