:: MESFUN7C semantic presentation

REAL is non empty V33() V38() V39() V40() V44() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V38() V39() V40() V41() V42() V43() V44() Element of K6(REAL)
K6(REAL) is non empty set
ExtREAL is non empty V39() set
K7(NAT,ExtREAL) is non empty Relation-like V46() set
K6(K7(NAT,ExtREAL)) is non empty set
K6(ExtREAL) is non empty set
K630() is V184() L11()
the U1 of K630() is set
COMPLEX is non empty V33() V38() V44() set
RAT is non empty V33() V38() V39() V40() V41() V44() set
INT is non empty V33() V38() V39() V40() V41() V42() V44() set
omega is non empty epsilon-transitive epsilon-connected ordinal V38() V39() V40() V41() V42() V43() V44() set
K6(omega) is non empty set
K6(NAT) is non empty set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative Relation-like non-empty empty-yielding RAT -valued V38() V39() V40() V41() V42() V43() V44() V45() V46() V47() V48() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative Relation-like non-empty empty-yielding RAT -valued V38() V39() V40() V41() V42() V43() V44() V45() V46() V47() V48() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
{{},1} is set
K7(NAT,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(NAT,REAL)) is non empty set
K6(K6(REAL)) is non empty set
K7(COMPLEX,COMPLEX) is non empty Relation-like V45() set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty Relation-like V45() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K7(REAL,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(REAL,REAL)) is non empty set
K7(K7(REAL,REAL),REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
K7(RAT,RAT) is non empty Relation-like RAT -valued V45() V46() V47() set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is non empty Relation-like RAT -valued V45() V46() V47() set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is non empty Relation-like RAT -valued INT -valued V45() V46() V47() set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is non empty Relation-like RAT -valued INT -valued V45() V46() V47() set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is non empty Relation-like RAT -valued INT -valued V45() V46() V47() V48() set
K7(K7(NAT,NAT),NAT) is non empty Relation-like RAT -valued INT -valued V45() V46() V47() V48() set
K6(K7(K7(NAT,NAT),NAT)) is non empty set
K7(NAT,COMPLEX) is non empty Relation-like V45() set
K6(K7(NAT,COMPLEX)) is non empty set
K6(RAT) is non empty set
K596( the U1 of K630()) is M21( the U1 of K630())
K596(COMPLEX) is M21( COMPLEX )
K7(COMPLEX,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(COMPLEX,REAL)) is non empty set
0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
+infty is non empty non real ext-real positive non negative Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
<i> is complex Element of COMPLEX
K64(0) is complex real ext-real Element of REAL
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
dom S is non empty V38() V39() V40() V41() V42() V43() Element of K6(NAT)
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
S . f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
f is Element of X
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
F is set
rng ((X,S) # f) is non empty V39() V81() Element of K6(ExtREAL)
c is set
((X,S) # f) . c is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(X,S) . n is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
((X,S) . n) . f is ext-real Element of ExtREAL
S . n is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
R_EAL (S . n) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(R_EAL (S . n)) . f is ext-real Element of ExtREAL
(S . n) . f is complex real ext-real Element of REAL
F is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
n is set
c is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
c . n is complex real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(X,S) . x is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
((X,S) . x) . f is ext-real Element of ExtREAL
S . x is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (S . x) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(R_EAL (S . x)) . f is ext-real Element of ExtREAL
(S # f) . n is complex real ext-real Element of REAL
X is non empty set
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
S is non empty Relation-like X -defined REAL -valued Function-like total V30(X, REAL ) V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL S is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
inf (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
inf (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (X,S) is Element of K6(X)
K6(X) is non empty set
f is Element of X
(X,S) . f is ext-real Element of ExtREAL
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
rng (R_EAL (S # f)) is non empty V39() V81() Element of K6(ExtREAL)
inf (rng (R_EAL (S # f))) is ext-real Element of ExtREAL
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inf ((X,S) # f) is ext-real Element of ExtREAL
rng ((X,S) # f) is non empty V39() V81() Element of K6(ExtREAL)
inf (rng ((X,S) # f)) is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
sup (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
sup (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (X,S) is Element of K6(X)
K6(X) is non empty set
f is Element of X
(X,S) . f is ext-real Element of ExtREAL
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
rng (R_EAL (S # f)) is non empty V39() V81() Element of K6(ExtREAL)
sup (rng (R_EAL (S # f))) is ext-real Element of ExtREAL
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
sup ((X,S) # f) is ext-real Element of ExtREAL
rng ((X,S) # f) is non empty V39() V81() Element of K6(ExtREAL)
sup (rng ((X,S) # f)) is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
inferior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
inferior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (S . 0) is Element of K6(X)
K6(X) is non empty set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,S) . f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
dom ((X,S) . f) is Element of K6(X)
(X,S) . 0 is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom ((X,S) . 0) is Element of K6(X)
R_EAL (S . 0) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (R_EAL (S . 0)) is Element of K6(X)
c is Element of X
((X,S) . f) . c is ext-real Element of ExtREAL
(X,S) # c is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inferior_realsequence ((X,S) # c) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
(inferior_realsequence ((X,S) # c)) . f is ext-real Element of ExtREAL
((X,S) # c) ^\ f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inf (((X,S) # c) ^\ f) is ext-real Element of ExtREAL
rng (((X,S) # c) ^\ f) is non empty V39() V81() Element of K6(ExtREAL)
inf (rng (((X,S) # c) ^\ f)) is ext-real Element of ExtREAL
S # c is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # c) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inferior_realsequence (R_EAL (S # c)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
(inferior_realsequence (R_EAL (S # c))) . f is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
superior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
superior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (S . 0) is Element of K6(X)
K6(X) is non empty set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,S) . f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
dom ((X,S) . f) is Element of K6(X)
c is Element of X
((X,S) . f) . c is ext-real Element of ExtREAL
(X,S) # c is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
superior_realsequence ((X,S) # c) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
(superior_realsequence ((X,S) # c)) . f is ext-real Element of ExtREAL
S # c is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # c) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
superior_realsequence (R_EAL (S # c)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
(superior_realsequence (R_EAL (S # c))) . f is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (S . 0) is Element of K6(X)
K6(X) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
inferior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
f is Element of X
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inferior_realsequence (R_EAL (S # f)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(X,S) . c is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
dom ((X,S) . c) is Element of K6(X)
((X,S) # f) . c is ext-real Element of ExtREAL
((X,S) . c) . f is ext-real Element of ExtREAL
(inferior_realsequence (R_EAL (S # f))) . c is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,S) . f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
dom ((X,S) . f) is Element of K6(X)
K6(X) is non empty set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,S) . F is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom ((X,S) . F) is Element of K6(X)
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
f is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
F is Element of f
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
S . c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
(X,S) . c is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
R_EAL (S . c) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
PFuncs (X,ExtREAL) is non empty functional set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,S) ^\ f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
S ^\ f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(S ^\ f)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
inferior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,S) . f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
S ^\ f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(S ^\ f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,(S ^\ f)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
inf (X,(S ^\ f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(inferior_realsequence (X,S)) . f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,S) ^\ f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
inf ((X,S) ^\ f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
superior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,S) . f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
S ^\ f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(S ^\ f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,(S ^\ f)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
sup (X,(S ^\ f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(superior_realsequence (X,S)) . f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,S) ^\ f is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
sup ((X,S) ^\ f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (S . 0) is Element of K6(X)
K6(X) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
superior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
f is Element of X
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
superior_realsequence (R_EAL (S # f)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(X,S) . c is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
dom ((X,S) . c) is Element of K6(X)
((X,S) # f) . c is ext-real Element of ExtREAL
((X,S) . c) . f is ext-real Element of ExtREAL
(superior_realsequence (R_EAL (S # f))) . c is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim_inf (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim_inf (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (X,S) is Element of K6(X)
K6(X) is non empty set
f is Element of X
(X,S) . f is ext-real Element of ExtREAL
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
lim_inf (R_EAL (S # f)) is ext-real Element of ExtREAL
inferior_realsequence (R_EAL (S # f)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence (R_EAL (S # f))) is ext-real Element of ExtREAL
rng (inferior_realsequence (R_EAL (S # f))) is non empty V39() V81() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (R_EAL (S # f)))) is ext-real Element of ExtREAL
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
lim_inf ((X,S) # f) is ext-real Element of ExtREAL
inferior_realsequence ((X,S) # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence ((X,S) # f)) is ext-real Element of ExtREAL
rng (inferior_realsequence ((X,S) # f)) is non empty V39() V81() Element of K6(ExtREAL)
sup (rng (inferior_realsequence ((X,S) # f))) is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim_sup (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim_sup (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (X,S) is Element of K6(X)
K6(X) is non empty set
f is Element of X
(X,S) . f is ext-real Element of ExtREAL
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
lim_sup (R_EAL (S # f)) is ext-real Element of ExtREAL
superior_realsequence (R_EAL (S # f)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence (R_EAL (S # f))) is ext-real Element of ExtREAL
rng (superior_realsequence (R_EAL (S # f))) is non empty V39() V81() Element of K6(ExtREAL)
inf (rng (superior_realsequence (R_EAL (S # f)))) is ext-real Element of ExtREAL
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
lim_sup ((X,S) # f) is ext-real Element of ExtREAL
superior_realsequence ((X,S) # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence ((X,S) # f)) is ext-real Element of ExtREAL
rng (superior_realsequence ((X,S) # f)) is non empty V39() V81() Element of K6(ExtREAL)
inf (rng (superior_realsequence ((X,S) # f))) is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (X,S) is Element of K6(X)
K6(X) is non empty set
f is Element of X
(X,S) . f is ext-real Element of ExtREAL
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
lim (R_EAL (S # f)) is ext-real Element of ExtREAL
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
lim ((X,S) # f) is ext-real Element of ExtREAL
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (X,S) is Element of K6(X)
K6(X) is non empty set
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
lim_sup (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
lim_inf (X,S) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
f is Element of X
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(X,S) . f is ext-real Element of ExtREAL
(X,S) . f is ext-real Element of ExtREAL
(X,S) . f is ext-real Element of ExtREAL
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
lim (R_EAL (S # f)) is ext-real Element of ExtREAL
lim_sup (R_EAL (S # f)) is ext-real Element of ExtREAL
superior_realsequence (R_EAL (S # f)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence (R_EAL (S # f))) is ext-real Element of ExtREAL
rng (superior_realsequence (R_EAL (S # f))) is non empty V39() V81() Element of K6(ExtREAL)
inf (rng (superior_realsequence (R_EAL (S # f)))) is ext-real Element of ExtREAL
lim_inf (R_EAL (S # f)) is ext-real Element of ExtREAL
inferior_realsequence (R_EAL (S # f)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence (R_EAL (S # f))) is ext-real Element of ExtREAL
rng (inferior_realsequence (R_EAL (S # f))) is non empty V39() V81() Element of K6(ExtREAL)
sup (rng (inferior_realsequence (R_EAL (S # f)))) is ext-real Element of ExtREAL
S . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (S . 0) is Element of K6(X)
dom (X,S) is Element of K6(X)
dom (X,S) is Element of K6(X)
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
bool X is non empty Element of K6(K6(X))
K7(NAT,(bool X)) is non empty Relation-like set
K6(K7(NAT,(bool X))) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
f . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (f . 0) is Element of K6(X)
(X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
sup (X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
F is non empty Relation-like NAT -defined bool X -valued S -valued Function-like total V30( NAT , bool X) Element of K6(K7(NAT,(bool X)))
rng F is non empty Element of K6(S)
K6(S) is non empty set
union (rng F) is set
c is complex real ext-real set
great_dom ((X,f),c) is Element of K6(X)
(dom (f . 0)) /\ (great_dom ((X,f),c)) is Element of K6(X)
x is set
y is Element of X
(X,f) . y is ext-real Element of ExtREAL
f # y is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (f # y) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
rng (R_EAL (f # y)) is non empty V39() V81() Element of K6(ExtREAL)
FG is ext-real set
FG is set
(R_EAL (f # y)) . FG is ext-real Element of ExtREAL
sup (rng (R_EAL (f # y))) is ext-real Element of ExtREAL
dom (X,f) is Element of K6(X)
FG is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(f # y) . FG is complex real ext-real Element of REAL
FG is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(f # y) . FG is complex real ext-real Element of REAL
f . FG is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (f . FG) is Element of K6(X)
(f . FG) . y is complex real ext-real Element of REAL
great_dom ((f . FG),c) is set
F . FG is Element of bool X
(dom (f . 0)) /\ (great_dom ((f . FG),c)) is Element of K6(X)
x is set
rng F is non empty Element of K6((bool X))
K6((bool X)) is non empty set
y is set
dom F is non empty V38() V39() V40() V41() V42() V43() Element of K6(NAT)
FG is set
F . FG is set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
F . k is Element of bool X
f . k is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
great_dom ((f . k),c) is set
(dom (f . 0)) /\ (great_dom ((f . k),c)) is Element of K6(X)
FG is Element of X
(f . k) . FG is complex real ext-real Element of REAL
f # FG is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(X,f) # FG is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
((X,f) # FG) . k is ext-real Element of ExtREAL
rng ((X,f) # FG) is non empty V39() V81() Element of K6(ExtREAL)
sup (rng ((X,f) # FG)) is ext-real Element of ExtREAL
dom (X,f) is Element of K6(X)
(X,f) . FG is ext-real Element of ExtREAL
sup ((X,f) # FG) is ext-real Element of ExtREAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
bool X is non empty Element of K6(K6(X))
K7(NAT,(bool X)) is non empty Relation-like set
K6(K7(NAT,(bool X))) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
f . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (f . 0) is Element of K6(X)
(X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
inf (X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
F is non empty Relation-like NAT -defined bool X -valued S -valued Function-like total V30( NAT , bool X) Element of K6(K7(NAT,(bool X)))
rng F is non empty Element of K6(S)
K6(S) is non empty set
meet (rng F) is set
c is complex real ext-real set
great_eq_dom ((X,f),c) is Element of K6(X)
(dom (f . 0)) /\ (great_eq_dom ((X,f),c)) is Element of K6(X)
x is set
rng F is non empty Element of K6((bool X))
K6((bool X)) is non empty set
meet (rng F) is Element of K6(X)
F . 0 is Element of bool X
great_eq_dom ((f . 0),c) is set
(dom (f . 0)) /\ (great_eq_dom ((f . 0),c)) is Element of K6(X)
dom (X,f) is Element of K6(X)
FG is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
F . FG is Element of bool X
y is Element of X
f . FG is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
great_eq_dom ((f . FG),c) is set
(dom (f . 0)) /\ (great_eq_dom ((f . FG),c)) is Element of K6(X)
(f . FG) . y is complex real ext-real Element of REAL
f # y is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (f # y) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
(R_EAL (f # y)) . FG is ext-real Element of ExtREAL
rng (R_EAL (f # y)) is non empty V39() V81() Element of K6(ExtREAL)
FG is ext-real set
FG is set
(R_EAL (f # y)) . FG is ext-real Element of ExtREAL
inf (rng (R_EAL (f # y))) is ext-real Element of ExtREAL
(X,f) . x is ext-real Element of ExtREAL
x is set
y is Element of X
(X,f) . y is ext-real Element of ExtREAL
FG is set
FG is set
F . FG is set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
f . k is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (f . k) is Element of K6(X)
f # y is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
R_EAL (f # y) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
rng (R_EAL (f # y)) is non empty V39() V81() Element of K6(ExtREAL)
inf (rng (R_EAL (f # y))) is ext-real Element of ExtREAL
(f . k) . y is complex real ext-real Element of REAL
(R_EAL (f # y)) . k is ext-real Element of ExtREAL
great_eq_dom ((f . k),c) is set
F . k is Element of bool X
(dom (f . 0)) /\ (great_eq_dom ((f . k),c)) is Element of K6(X)
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
f . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (f . 0) is Element of K6(X)
(X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim_sup (X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
F is Element of S
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,f) . c is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
f . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (f . 0) is Element of K6(X)
(X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim_inf (X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
F is Element of S
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,f) . c is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (S . 0) is Element of K6(X)
K6(X) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
superior_realsequence (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
f is Element of X
S # f is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(X,S) # f is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
R_EAL (S # f) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
superior_realsequence (R_EAL (S # f)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V30( NAT , ExtREAL ) V46() Element of K6(K7(NAT,ExtREAL))
superior_realsequence (S # f) is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
f . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (f . 0) is Element of K6(X)
(X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
(X,f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V30( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is non empty set
lim (X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
F is Element of S
dom (X,f) is Element of K6(X)
(X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
lim_sup (X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
c is Element of X
f # c is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(X,f) . c is ext-real Element of ExtREAL
(X,f) . c is ext-real Element of ExtREAL
dom (X,f) is Element of K6(X)
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
K7(X,ExtREAL) is non empty Relation-like V46() set
K6(K7(X,ExtREAL)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
f . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
K7(X,REAL) is non empty Relation-like V45() V46() V47() set
K6(K7(X,REAL)) is non empty set
dom (f . 0) is Element of K6(X)
F is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom F is Element of K6(X)
c is Element of S
(X,f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of