:: 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 K6(K7(X,ExtREAL))
(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))
dom (X,f) is Element of K6(X)
n is Element of X
f # n is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
lim (f # n) is complex real ext-real Element of REAL
R_EAL (f # n) 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 (f # n)) is ext-real Element of ExtREAL
F . n is ext-real Element of ExtREAL
(X,f) . n is ext-real Element of ExtREAL
n is Element of X
f # n 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
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
f is Element of X
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 COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
(S . F) . f is complex set
F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . c is complex set
S . c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
(S . c) . f is complex set
F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
c is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
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
F . n is complex Element of COMPLEX
S . n is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
(S . n) . f is complex set
c . n is complex Element of COMPLEX
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
S . 0 is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (S . 0) is Element of K6(X)
K6(X) is non empty set
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom f is Element of K6(X)
F is Element of X
f /. F is complex Element of COMPLEX
(X,S,F) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
lim (X,S,F) is complex Element of COMPLEX
f . F is complex set
F is set
c is set
F is Element of X
f . F is complex set
(X,S,F) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
lim (X,S,F) is complex Element of COMPLEX
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom f is Element of K6(X)
F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom F is Element of K6(X)
c is Element of X
f . c is complex set
(X,S,c) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
lim (X,S,c) is complex Element of COMPLEX
F . c is complex set
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) 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,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
PFuncs (X,REAL) is non empty functional M19(X, REAL )
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 COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . f) is Element of K6(X)
K6(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
F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom F is Element of K6(X)
dom F is set
c is Element of X
F /. c is complex real ext-real Element of REAL
(X,S,c) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (X,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))
(Re (X,S,c)) . f is complex real ext-real Element of REAL
F . c is complex real ext-real Element of REAL
c is set
n is set
c is Element of X
F . c is complex real ext-real set
(X,S,c) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (X,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))
(Re (X,S,c)) . f is complex real ext-real Element of REAL
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
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))))
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))))
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . 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
dom (F . c) is Element of K6(X)
K6(X) is non empty set
S . c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . c) is Element of K6(X)
n is Element of X
(F . c) . n is complex real ext-real Element of REAL
(X,S,n) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (X,S,n) is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(Re (X,S,n)) . c is complex real ext-real Element of REAL
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))))
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))))
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
f . 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
dom (f . c) is Element of K6(X)
K6(X) is non empty set
S . c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . c) is Element of K6(X)
F . c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (F . c) is Element of K6(X)
n is Element of X
(f . c) . n is complex real ext-real Element of REAL
(X,S,n) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (X,S,n) is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(Re (X,S,n)) . c is complex real ext-real Element of REAL
(F . c) . n is complex real ext-real Element of REAL
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,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,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
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,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
dom ((X,S) . f) is Element of K6(X)
K6(X) is non empty set
S . f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . f) is Element of K6(X)
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
S . F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (S . F) is Element of K6(X)
(X,S) . F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,S) . F) is Element of K6(X)
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) 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,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
PFuncs (X,REAL) is non empty functional M19(X, REAL )
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 COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . f) is Element of K6(X)
K6(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
F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom F is Element of K6(X)
dom F is set
c is Element of X
F /. c is complex real ext-real Element of REAL
(X,S,c) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Im (X,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))
(Im (X,S,c)) . f is complex real ext-real Element of REAL
F . c is complex real ext-real Element of REAL
c is set
n is set
c is Element of X
F . c is complex real ext-real set
(X,S,c) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Im (X,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))
(Im (X,S,c)) . f is complex real ext-real Element of REAL
K7(NAT,(PFuncs (X,REAL))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,REAL)))) is non empty set
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))))
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))))
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . 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
dom (F . c) is Element of K6(X)
K6(X) is non empty set
S . c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . c) is Element of K6(X)
n is Element of X
(F . c) . n is complex real ext-real Element of REAL
(X,S,n) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Im (X,S,n) is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(Im (X,S,n)) . c is complex real ext-real Element of REAL
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))))
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))))
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
f . 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
dom (f . c) is Element of K6(X)
K6(X) is non empty set
S . c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . c) is Element of K6(X)
F . c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (F . c) is Element of K6(X)
n is Element of X
(f . c) . n is complex real ext-real Element of REAL
(X,S,n) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Im (X,S,n) is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(Im (X,S,n)) . c is complex real ext-real Element of REAL
(F . c) . n is complex real ext-real Element of REAL
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,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,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
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,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
dom ((X,S) . f) is Element of K6(X)
K6(X) is non empty set
S . f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (S . f) is Element of K6(X)
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
S . F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (S . F) is Element of K6(X)
(X,S) . F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,S) . F) is Element of K6(X)
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
S . 0 is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) 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,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
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
(X,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))))
f is Element of X
(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 COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (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 REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
Im (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))
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 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 ((X,S) . n) is Element of K6(X)
S . n is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (S . n) is Element of K6(X)
(X,S) . n is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,S) . n) is Element of K6(X)
((X,S) # f) . n is complex real ext-real Element of REAL
((X,S) . n) . f is complex real ext-real Element of REAL
((X,S) # f) . n is complex real ext-real Element of REAL
((X,S) . n) . f is complex real ext-real Element of REAL
(Re (X,S,f)) . n is complex real ext-real Element of REAL
(Im (X,S,f)) . n is complex real ext-real Element of REAL
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,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,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
(X,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))))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(X,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
S . f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
Re (S . f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(X,S) . f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Im (S . f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,S) . f) is Element of K6(X)
K6(X) is non empty set
dom (S . f) is Element of K6(X)
dom (Re (S . f)) is Element of K6(X)
F is Element of X
(Re (S . f)) . F is complex real ext-real Element of REAL
(S . f) . F is complex set
Re ((S . f) . F) is complex real ext-real Element of REAL
(X,S,F) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
(X,S,F) . f is complex set
Re ((X,S,F) . f) is complex real ext-real Element of REAL
((X,S) . f) . F is complex real ext-real Element of REAL
Re (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))
(Re (X,S,F)) . f is complex real ext-real Element of REAL
dom ((X,S) . f) is Element of K6(X)
dom (Im (S . f)) is Element of K6(X)
F is Element of X
(Im (S . f)) . F is complex real ext-real Element of REAL
(S . f) . F is complex set
Im ((S . f) . F) is complex real ext-real Element of REAL
(X,S,F) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
(X,S,F) . f is complex set
Im ((X,S,F) . f) is complex real ext-real Element of REAL
((X,S) . f) . F is complex real ext-real Element of REAL
Im (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))
(Im (X,S,F)) . f is complex real ext-real Element of REAL
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
S . 0 is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) 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,REAL) -valued Function-like total V30( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
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
(X,(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,(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
lim (X,(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 COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Re (X,S) 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) 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,(X,S)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,(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))))
lim (X,(X,S)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
Im (X,S) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (X,(X,S)) is Element of K6(X)
(X,S) . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,S) . 0) is Element of K6(X)
dom (Re (X,S)) is Element of K6(X)
dom (X,S) is Element of K6(X)
f is Element of X
(X,S,f) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (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 REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(X,(X,S)) . f is ext-real Element of ExtREAL
R_EAL ((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 (R_EAL ((X,S) # f)) is ext-real Element of ExtREAL
lim ((X,S) # f) is complex real ext-real Element of REAL
lim (Re (X,S,f)) is complex real ext-real Element of REAL
lim (X,S,f) is complex Element of COMPLEX
Re (lim (X,S,f)) is complex real ext-real Element of REAL
(Re (X,S)) . f is complex real ext-real Element of REAL
(X,S) . f is complex set
Re ((X,S) . f) is complex real ext-real Element of REAL
dom (X,(X,S)) is Element of K6(X)
(X,S) . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,S) . 0) is Element of K6(X)
dom (Im (X,S)) is Element of K6(X)
f is Element of X
(X,S,f) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Im (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 REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
(X,(X,S)) . f is ext-real Element of ExtREAL
R_EAL ((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 (R_EAL ((X,S) # f)) is ext-real Element of ExtREAL
lim ((X,S) # f) is complex real ext-real Element of REAL
lim (Im (X,S,f)) is complex real ext-real Element of REAL
lim (X,S,f) is complex Element of COMPLEX
Im (lim (X,S,f)) is complex real ext-real Element of REAL
(Im (X,S)) . f is complex real ext-real Element of REAL
(X,S) . f is complex set
Im ((X,S) . f) is complex real ext-real Element of REAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) 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,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
f . 0 is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
dom (f . 0) is Element of K6(X)
(X,f) is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
F is Element of S
(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))))
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
(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,(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,(X,f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
Im (X,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
R_EAL (Im (X,f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
c is Element of X
(X,f,c) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Im (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 non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
f . c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Im (f . c) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(X,f) . c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(X,f) . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,f) . 0) is Element of K6(X)
c is Element of X
(X,f,c) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (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) 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,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))
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
f . c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Re (f . c) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(X,f) . c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(X,(X,f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,(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))))
lim (X,(X,f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
Re (X,f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (Re (X,f)) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(X,f) . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,f) . 0) 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,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is non empty Relation-like set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) 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,COMPLEX) -valued Function-like total V30( NAT , PFuncs (X,COMPLEX)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
f . 0 is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (f . 0) is Element of K6(X)
F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom F is Element of K6(X)
c is Element of S
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
f . n is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Im (f . 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
(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))))
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
(X,f) . n is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Im F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (Im F) is Element of K6(X)
n is Element of X
(X,f,n) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Im (X,f,n) 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) # n is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
F . n is complex set
lim (X,f,n) is complex Element of COMPLEX
Im (F . n) is complex real ext-real Element of REAL
lim (Im (X,f,n)) is complex real ext-real Element of REAL
lim ((X,f) # n) is complex real ext-real Element of REAL
(Im F) . n is complex real ext-real Element of REAL
(X,f) . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,f) . 0) is Element of K6(X)
R_EAL (Im 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
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
f . n is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Re (f . n) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(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))))
(X,f) . n is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Re F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (Re F) is Element of K6(X)
n is Element of X
(X,f,n) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V30( NAT , COMPLEX ) V45() Element of K6(K7(NAT,COMPLEX))
Re (X,f,n) 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) # n is non empty Relation-like NAT -defined REAL -valued Function-like total V30( NAT , REAL ) V45() V46() V47() Element of K6(K7(NAT,REAL))
F . n is complex set
lim (X,f,n) is complex Element of COMPLEX
Re (F . n) is complex real ext-real Element of REAL
lim (Re (X,f,n)) is complex real ext-real Element of REAL
lim ((X,f) # n) is complex real ext-real Element of REAL
(Re F) . n is complex real ext-real Element of REAL
(X,f) . 0 is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((X,f) . 0) is Element of K6(X)
R_EAL (Re F) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
X is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is set
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
f | S is Relation-like X -defined S -defined X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
F is complex real ext-real Element of REAL
F (#) f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
(F (#) f) | S is Relation-like X -defined S -defined X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
F (#) (f | S) is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom ((F (#) f) | S) is Element of K6(X)
K6(X) is non empty set
dom (F (#) f) is Element of K6(X)
(dom (F (#) f)) /\ S is Element of K6(X)
dom f is Element of K6(X)
(dom f) /\ S is Element of K6(X)
dom (f | S) is Element of K6(X)
dom (F (#) (f | S)) is Element of K6(X)
c is Element of X
((F (#) f) | S) . c is complex set
(F (#) f) . c is complex set
f . c is complex set
F * (f . c) is complex set
(f | S) . c is complex set
F * ((f | S) . c) is complex set
(F (#) (f | S)) . c is complex set
X is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.S.| 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
f is set
dom |.S.| is Element of K6(X)
K6(X) is non empty set
|.S.| . f is complex real ext-real Element of REAL
S . f is complex set
|.(S . f).| is complex real ext-real Element of REAL
Re (S . f) is complex real ext-real Element of REAL
K62((Re (S . f))) is complex real ext-real Element of REAL
Im (S . f) is complex real ext-real Element of REAL
K62((Im (S . f))) is complex real ext-real Element of REAL
K62((Re (S . f))) + K62((Im (S . f))) is complex real ext-real Element of REAL
K64((K62((Re (S . f))) + K62((Im (S . f))))) is complex real ext-real Element of REAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom f is Element of K6(X)
|.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
F is complex real ext-real set
|.f.| to_power F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
c is Element of S
dom |.f.| is Element of K6(X)
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 Relation-like X -defined REAL -valued Function-like 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
f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL f is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(R_EAL S) (#) (R_EAL f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
S (#) f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (S (#) f) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom ((R_EAL S) (#) (R_EAL f)) is Element of K6(X)
K6(X) is non empty set
dom (R_EAL S) is Element of K6(X)
dom (R_EAL f) is Element of K6(X)
(dom (R_EAL S)) /\ (dom (R_EAL f)) is Element of K6(X)
F is Element of X
dom (S (#) f) is Element of K6(X)
(S (#) f) . F is complex real ext-real Element of REAL
S . F is complex real ext-real Element of REAL
f . F is complex real ext-real Element of REAL
(S . F) * (f . F) is complex real ext-real Element of REAL
((R_EAL S) (#) (R_EAL f)) . F is ext-real Element of ExtREAL
(R_EAL S) . F is ext-real Element of ExtREAL
(R_EAL f) . F is ext-real Element of ExtREAL
((R_EAL S) . F) * ((R_EAL f) . F) is ext-real Element of ExtREAL
(R_EAL (S (#) f)) . F is ext-real Element of ExtREAL
dom (R_EAL (S (#) f)) is Element of K6(X)
X is non empty set
K6(X) is non empty set
K6(K6(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 compl-closed sigma-multiplicative Element of K6(K6(X))
f is Element of S
F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom F is Element of K6(X)
c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom c is Element of K6(X)
(dom F) /\ (dom c) is Element of K6(X)
F (#) c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL 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
R_EAL c is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
(R_EAL F) (#) (R_EAL c) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
R_EAL (F (#) c) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
X is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Re S 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
Im S is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
S (#) f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Re (S (#) f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Re f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(Re S) (#) (Re f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Im f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(Im S) (#) (Im f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
((Re S) (#) (Re f)) - ((Im S) (#) (Im f)) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Im (S (#) f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(Im S) (#) (Re f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(Re S) (#) (Im f) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
((Im S) (#) (Re f)) + ((Re S) (#) (Im f)) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((Re S) (#) (Re f)) is Element of K6(X)
K6(X) is non empty set
dom (Re S) is Element of K6(X)
dom (Re f) is Element of K6(X)
(dom (Re S)) /\ (dom (Re f)) is Element of K6(X)
dom ((Im S) (#) (Im f)) is Element of K6(X)
dom (Im S) is Element of K6(X)
dom (Im f) is Element of K6(X)
(dom (Im S)) /\ (dom (Im f)) is Element of K6(X)
dom S is Element of K6(X)
dom f is Element of K6(X)
dom (Re (S (#) f)) is Element of K6(X)
dom (S (#) f) is Element of K6(X)
(dom S) /\ (dom f) is Element of K6(X)
dom (((Re S) (#) (Re f)) - ((Im S) (#) (Im f))) is Element of K6(X)
(dom ((Re S) (#) (Re f))) /\ (dom ((Im S) (#) (Im f))) is Element of K6(X)
F is set
(Re (S (#) f)) . F is complex real ext-real Element of REAL
(S (#) f) . F is complex set
Re ((S (#) f) . F) is complex real ext-real Element of REAL
S . F is complex set
f . F is complex set
(S . F) * (f . F) is complex set
Re ((S . F) * (f . F)) is complex real ext-real Element of REAL
Re (S . F) is complex real ext-real Element of REAL
Re (f . F) is complex real ext-real Element of REAL
(Re (S . F)) * (Re (f . F)) is complex real ext-real Element of REAL
Im (S . F) is complex real ext-real Element of REAL
Im (f . F) is complex real ext-real Element of REAL
(Im (S . F)) * (Im (f . F)) is complex real ext-real Element of REAL
((Re (S . F)) * (Re (f . F))) - ((Im (S . F)) * (Im (f . F))) is complex real ext-real Element of REAL
(Re f) . F is complex real ext-real Element of REAL
(Im f) . F is complex real ext-real Element of REAL
(Re S) . F is complex real ext-real Element of REAL
(Im S) . F is complex real ext-real Element of REAL
((Re S) (#) (Re f)) . F is complex real ext-real Element of REAL
((Im S) . F) * ((Im f) . F) is complex real ext-real Element of REAL
(((Re S) (#) (Re f)) . F) - (((Im S) . F) * ((Im f) . F)) is complex real ext-real Element of REAL
((Im S) (#) (Im f)) . F is complex real ext-real Element of REAL
(((Re S) (#) (Re f)) . F) - (((Im S) (#) (Im f)) . F) is complex real ext-real Element of REAL
(((Re S) (#) (Re f)) - ((Im S) (#) (Im f))) . F is complex real ext-real Element of REAL
dom ((Im S) (#) (Re f)) is Element of K6(X)
(dom (Im S)) /\ (dom (Re f)) is Element of K6(X)
dom ((Re S) (#) (Im f)) is Element of K6(X)
(dom (Re S)) /\ (dom (Im f)) is Element of K6(X)
dom (Im (S (#) f)) is Element of K6(X)
dom (((Im S) (#) (Re f)) + ((Re S) (#) (Im f))) is Element of K6(X)
(dom ((Im S) (#) (Re f))) /\ (dom ((Re S) (#) (Im f))) is Element of K6(X)
F is set
(Im (S (#) f)) . F is complex real ext-real Element of REAL
(S (#) f) . F is complex set
Im ((S (#) f) . F) is complex real ext-real Element of REAL
S . F is complex set
f . F is complex set
(S . F) * (f . F) is complex set
Im ((S . F) * (f . F)) is complex real ext-real Element of REAL
Im (S . F) is complex real ext-real Element of REAL
Re (f . F) is complex real ext-real Element of REAL
(Im (S . F)) * (Re (f . F)) is complex real ext-real Element of REAL
Re (S . F) is complex real ext-real Element of REAL
Im (f . F) is complex real ext-real Element of REAL
(Re (S . F)) * (Im (f . F)) is complex real ext-real Element of REAL
((Im (S . F)) * (Re (f . F))) + ((Re (S . F)) * (Im (f . F))) is complex real ext-real Element of REAL
(Re f) . F is complex real ext-real Element of REAL
(Im f) . F is complex real ext-real Element of REAL
(Re S) . F is complex real ext-real Element of REAL
(Im S) . F is complex real ext-real Element of REAL
((Im S) (#) (Re f)) . F is complex real ext-real Element of REAL
((Re S) . F) * ((Im f) . F) is complex real ext-real Element of REAL
(((Im S) (#) (Re f)) . F) + (((Re S) . F) * ((Im f) . F)) is complex real ext-real Element of REAL
((Re S) (#) (Im f)) . F is complex real ext-real Element of REAL
(((Im S) (#) (Re f)) . F) + (((Re S) (#) (Im f)) . F) is complex real ext-real Element of REAL
(((Im S) (#) (Re f)) + ((Re S) (#) (Im f))) . F is complex real ext-real Element of REAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom f is Element of K6(X)
F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom F is Element of K6(X)
(dom f) /\ (dom F) is Element of K6(X)
f (#) F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
c is Element of S
Im 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
dom (Im F) is Element of K6(X)
Im f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (Im f) is Element of K6(X)
(Im f) (#) (Im F) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((Im f) (#) (Im F)) is Element of K6(X)
Re f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (Re f) is Element of K6(X)
Re F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (Re F) is Element of K6(X)
(Im f) (#) (Re F) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(Re f) (#) (Im F) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
((Im f) (#) (Re F)) + ((Re f) (#) (Im F)) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Im (f (#) F) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(Re f) (#) (Re F) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
((Re f) (#) (Re F)) - ((Im f) (#) (Im F)) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Re (f (#) F) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is non empty set
K6(K6(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 compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is non empty Relation-like V46() set
K6(K7(S,ExtREAL)) is non empty set
f is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) V46() V54() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom F is Element of K6(X)
c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom c is Element of K6(X)
Integral (f,c) is ext-real Element of ExtREAL
Integral (f,F) is ext-real Element of ExtREAL
R_EAL 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
integral+ (f,(R_EAL c)) is ext-real Element of ExtREAL
R_EAL F is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
integral+ (f,(R_EAL F)) is ext-real Element of ExtREAL
n is Element of S
n is Element of S
n is Element of S
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is non empty Relation-like V46() set
K6(K7(S,ExtREAL)) is non empty set
f is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) V46() V54() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom F is Element of K6(X)
|.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
Re F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (Re 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 (R_EAL (Re F)) is Element of K6(X)
c is Element of S
Im F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (Im F) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (R_EAL (Im F)) is Element of K6(X)
n is Element of S
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is non empty Relation-like V46() set
K6(K7(S,ExtREAL)) is non empty set
K7(NAT,S) is non empty Relation-like set
K6(K7(NAT,S)) is non empty set
f is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) V46() V54() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom F is Element of K6(X)
|.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
Coim (|.F.|,0) is set
(dom F) \ (Coim (|.F.|,0)) is Element of K6(X)
c is Element of S
dom |.F.| is Element of K6(X)
n is set
|.F.| . n is complex real ext-real Element of REAL
c \ (Coim (|.F.|,0)) is Element of K6(X)
x is complex real ext-real Element of REAL
F . n is complex set
|.(F . n).| is complex real ext-real Element of REAL
Re (F . n) is complex real ext-real Element of REAL
K62((Re (F . n))) is complex real ext-real Element of REAL
Im (F . n) is complex real ext-real Element of REAL
K62((Im (F . n))) is complex real ext-real Element of REAL
K62((Re (F . n))) + K62((Im (F . n))) is complex real ext-real Element of REAL
K64((K62((Re (F . n))) + K62((Im (F . n))))) is complex real ext-real Element of REAL
great_dom (|.F.|,0) is set
c /\ (great_dom (|.F.|,0)) is Element of K6(X)
n is set
|.F.| . n is complex real ext-real Element of REAL
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
n + 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 / (n + 1) is non empty complex real ext-real positive non negative Element of REAL
great_eq_dom (|.F.|,(1 / (n + 1))) is set
c /\ (great_eq_dom (|.F.|,(1 / (n + 1)))) is Element of K6(X)
n is non empty Relation-like NAT -defined S -valued Function-like total V30( NAT ,S) Element of K6(K7(NAT,S))
Integral (f,|.F.|) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
n . x is set
f . (n . x) is ext-real Element of ExtREAL
x + 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 / (x + 1) is non empty complex real ext-real positive non negative Element of REAL
R_EAL (1 / (x + 1)) is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
n . y is Element of S
y + 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 / (y + 1) is non empty complex real ext-real positive non negative Element of REAL
great_eq_dom (|.F.|,(1 / (y + 1))) is set
c /\ (great_eq_dom (|.F.|,(1 / (y + 1)))) is Element of K6(X)
FG is Element of S
|.F.| | FG is Relation-like X -defined FG -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
x is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom x is Element of K6(X)
dom (|.F.| | FG) is Element of K6(X)
great_eq_dom (|.F.|,(1 / (x + 1))) is set
y is Element of X
x . y is complex real ext-real Element of REAL
(|.F.| | FG) . y is complex real ext-real Element of REAL
|.F.| . y is complex real ext-real Element of REAL
(dom |.F.|) /\ FG is Element of K6(X)
c /\ FG is M11(X,S)
y is set
x . y is complex real ext-real Element of REAL
|.F.| | c is Relation-like X -defined c -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Integral (f,(|.F.| | FG)) is ext-real Element of ExtREAL
Integral (f,x) is ext-real Element of ExtREAL
f . FG is ext-real Element of ExtREAL
(R_EAL (1 / (x + 1))) * (f . FG) is ext-real Element of ExtREAL
((R_EAL (1 / (x + 1))) * (f . FG)) / (R_EAL (1 / (x + 1))) is ext-real Element of ExtREAL
+infty / (R_EAL (1 / (x + 1))) is ext-real Element of ExtREAL
rng n is non empty Element of K6(K6(X))
union (rng n) is Element of K6(X)
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
n . x is set
x + 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 / (x + 1) is non empty complex real ext-real positive non negative Element of REAL
great_eq_dom (|.F.|,(1 / (x + 1))) is set
c /\ (great_eq_dom (|.F.|,(1 / (x + 1)))) is Element of K6(X)
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
n . x is set
x + 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 / (x + 1) is non empty complex real ext-real positive non negative Element of REAL
0 + (1 / (x + 1)) is non empty complex real ext-real positive non negative Element of REAL
great_eq_dom (|.F.|,(0 + (1 / (x + 1)))) is set
c /\ (great_eq_dom (|.F.|,(0 + (1 / (x + 1))))) is Element of K6(X)
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
n . x is set
x + 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 / (x + 1) is non empty complex real ext-real positive non negative Element of REAL
R_EAL (1 / (x + 1)) is ext-real Element of ExtREAL
great_eq_dom (|.F.|,(R_EAL (1 / (x + 1)))) is set
(dom F) /\ (great_eq_dom (|.F.|,(R_EAL (1 / (x + 1))))) is Element of K6(X)
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
n . y is set
FG is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
n . FG is set
f . (n . FG) is ext-real Element of ExtREAL
X is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.S.| 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
f is set
|.S.| | f is Relation-like X -defined f -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
S | f is Relation-like X -defined f -defined X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.(S | f).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (|.S.| | f) is Element of K6(X)
K6(X) is non empty set
dom |.S.| is Element of K6(X)
(dom |.S.|) /\ f is Element of K6(X)
dom S is Element of K6(X)
(dom S) /\ f is Element of K6(X)
dom (S | f) is Element of K6(X)
dom |.(S | f).| is Element of K6(X)
F is Element of X
|.(S | f).| . F is complex real ext-real Element of REAL
(S | f) . F is complex set
|.((S | f) . F).| is complex real ext-real Element of REAL
Re ((S | f) . F) is complex real ext-real Element of REAL
K62((Re ((S | f) . F))) is complex real ext-real Element of REAL
Im ((S | f) . F) is complex real ext-real Element of REAL
K62((Im ((S | f) . F))) is complex real ext-real Element of REAL
K62((Re ((S | f) . F))) + K62((Im ((S | f) . F))) is complex real ext-real Element of REAL
K64((K62((Re ((S | f) . F))) + K62((Im ((S | f) . F))))) is complex real ext-real Element of REAL
S . F is complex set
|.(S . F).| is complex real ext-real Element of REAL
Re (S . F) is complex real ext-real Element of REAL
K62((Re (S . F))) is complex real ext-real Element of REAL
Im (S . F) is complex real ext-real Element of REAL
K62((Im (S . F))) is complex real ext-real Element of REAL
K62((Re (S . F))) + K62((Im (S . F))) is complex real ext-real Element of REAL
K64((K62((Re (S . F))) + K62((Im (S . F))))) is complex real ext-real Element of REAL
(|.S.| | f) . F is complex real ext-real Element of REAL
|.S.| . F is complex real ext-real Element of REAL
X is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.S.| 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 is Element of K6(X)
K6(X) is non empty set
dom |.S.| is Element of K6(X)
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.f.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
|.S.| + |.f.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (|.S.| + |.f.|) is Element of K6(X)
dom f is Element of K6(X)
(dom S) /\ (dom f) is Element of K6(X)
S + f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.(S + f).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom |.(S + f).| is Element of K6(X)
dom |.f.| is Element of K6(X)
(dom |.S.|) /\ (dom |.f.|) is Element of K6(X)
(dom S) /\ (dom |.f.|) is Element of K6(X)
dom (S + f) is Element of K6(X)
X is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.S.| 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
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
S + f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.(S + f).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom |.(S + f).| is Element of K6(X)
K6(X) is non empty set
|.S.| | (dom |.(S + f).|) is Relation-like X -defined dom |.(S + f).| -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
|.f.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
|.f.| | (dom |.(S + f).|) is Relation-like X -defined dom |.(S + f).| -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(|.S.| | (dom |.(S + f).|)) + (|.f.| | (dom |.(S + f).|)) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
|.S.| + |.f.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
(|.S.| + |.f.|) | (dom |.(S + f).|) is Relation-like X -defined dom |.(S + f).| -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom |.f.| is Element of K6(X)
dom f is Element of K6(X)
f | (dom |.(S + f).|) is Relation-like X -defined dom |.(S + f).| -defined X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (f | (dom |.(S + f).|)) is Element of K6(X)
(dom f) /\ (dom |.(S + f).|) is Element of K6(X)
|.(f | (dom |.(S + f).|)).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom |.(f | (dom |.(S + f).|)).| is Element of K6(X)
dom |.S.| is Element of K6(X)
dom S is Element of K6(X)
(dom |.(S + f).|) /\ (dom |.(S + f).|) is Element of K6(X)
(dom S) /\ (dom f) is Element of K6(X)
dom (|.S.| + |.f.|) is Element of K6(X)
dom ((|.S.| + |.f.|) | (dom |.(S + f).|)) is Element of K6(X)
S | (dom |.(S + f).|) is Relation-like X -defined dom |.(S + f).| -defined X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (S | (dom |.(S + f).|)) is Element of K6(X)
(dom S) /\ (dom |.(S + f).|) is Element of K6(X)
|.(S | (dom |.(S + f).|)).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom ((|.S.| | (dom |.(S + f).|)) + (|.f.| | (dom |.(S + f).|))) is Element of K6(X)
(dom (S | (dom |.(S + f).|))) /\ (dom (f | (dom |.(S + f).|))) is Element of K6(X)
dom |.(S | (dom |.(S + f).|)).| is Element of K6(X)
F is Element of X
((|.S.| + |.f.|) | (dom |.(S + f).|)) . F is complex real ext-real Element of REAL
(|.S.| + |.f.|) . F is complex real ext-real Element of REAL
|.S.| . F is complex real ext-real Element of REAL
|.f.| . F is complex real ext-real Element of REAL
(|.S.| . F) + (|.f.| . F) is complex real ext-real Element of REAL
S . F is complex set
|.(S . F).| is complex real ext-real Element of REAL
Re (S . F) is complex real ext-real Element of REAL
K62((Re (S . F))) is complex real ext-real Element of REAL
Im (S . F) is complex real ext-real Element of REAL
K62((Im (S . F))) is complex real ext-real Element of REAL
K62((Re (S . F))) + K62((Im (S . F))) is complex real ext-real Element of REAL
K64((K62((Re (S . F))) + K62((Im (S . F))))) is complex real ext-real Element of REAL
|.(S . F).| + (|.f.| . F) is complex real ext-real Element of REAL
((|.S.| | (dom |.(S + f).|)) + (|.f.| | (dom |.(S + f).|))) . F is complex real ext-real Element of REAL
(|.S.| | (dom |.(S + f).|)) . F is complex real ext-real Element of REAL
(|.f.| | (dom |.(S + f).|)) . F is complex real ext-real Element of REAL
((|.S.| | (dom |.(S + f).|)) . F) + ((|.f.| | (dom |.(S + f).|)) . F) is complex real ext-real Element of REAL
(S | (dom |.(S + f).|)) . F is complex set
|.((S | (dom |.(S + f).|)) . F).| is complex real ext-real Element of REAL
Re ((S | (dom |.(S + f).|)) . F) is complex real ext-real Element of REAL
K62((Re ((S | (dom |.(S + f).|)) . F))) is complex real ext-real Element of REAL
Im ((S | (dom |.(S + f).|)) . F) is complex real ext-real Element of REAL
K62((Im ((S | (dom |.(S + f).|)) . F))) is complex real ext-real Element of REAL
K62((Re ((S | (dom |.(S + f).|)) . F))) + K62((Im ((S | (dom |.(S + f).|)) . F))) is complex real ext-real Element of REAL
K64((K62((Re ((S | (dom |.(S + f).|)) . F))) + K62((Im ((S | (dom |.(S + f).|)) . F))))) is complex real ext-real Element of REAL
|.(f | (dom |.(S + f).|)).| . F is complex real ext-real Element of REAL
|.((S | (dom |.(S + f).|)) . F).| + (|.(f | (dom |.(S + f).|)).| . F) is complex real ext-real Element of REAL
(f | (dom |.(S + f).|)) . F is complex set
|.((f | (dom |.(S + f).|)) . F).| is complex real ext-real Element of REAL
Re ((f | (dom |.(S + f).|)) . F) is complex real ext-real Element of REAL
K62((Re ((f | (dom |.(S + f).|)) . F))) is complex real ext-real Element of REAL
Im ((f | (dom |.(S + f).|)) . F) is complex real ext-real Element of REAL
K62((Im ((f | (dom |.(S + f).|)) . F))) is complex real ext-real Element of REAL
K62((Re ((f | (dom |.(S + f).|)) . F))) + K62((Im ((f | (dom |.(S + f).|)) . F))) is complex real ext-real Element of REAL
K64((K62((Re ((f | (dom |.(S + f).|)) . F))) + K62((Im ((f | (dom |.(S + f).|)) . F))))) is complex real ext-real Element of REAL
|.((S | (dom |.(S + f).|)) . F).| + |.((f | (dom |.(S + f).|)) . F).| is complex real ext-real Element of REAL
|.(S . F).| + |.((f | (dom |.(S + f).|)) . F).| is complex real ext-real Element of REAL
f . F is complex set
|.(f . F).| is complex real ext-real Element of REAL
Re (f . F) is complex real ext-real Element of REAL
K62((Re (f . F))) is complex real ext-real Element of REAL
Im (f . F) is complex real ext-real Element of REAL
K62((Im (f . F))) is complex real ext-real Element of REAL
K62((Re (f . F))) + K62((Im (f . F))) is complex real ext-real Element of REAL
K64((K62((Re (f . F))) + K62((Im (f . F))))) is complex real ext-real Element of REAL
|.(S . F).| + |.(f . F).| is complex real ext-real Element of REAL
X is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.S.| 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
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
S + f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.(S + f).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom |.(S + f).| is Element of K6(X)
K6(X) is non empty set
|.f.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
|.S.| + |.f.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
F is set
|.(S + f).| . F is complex real ext-real Element of REAL
(|.S.| + |.f.|) . F is complex real ext-real Element of REAL
S . F is complex set
f . F is complex set
(S . F) + (f . F) is complex set
|.((S . F) + (f . F)).| is complex real ext-real Element of REAL
Re ((S . F) + (f . F)) is complex real ext-real Element of REAL
K62((Re ((S . F) + (f . F)))) is complex real ext-real Element of REAL
Im ((S . F) + (f . F)) is complex real ext-real Element of REAL
K62((Im ((S . F) + (f . F)))) is complex real ext-real Element of REAL
K62((Re ((S . F) + (f . F)))) + K62((Im ((S . F) + (f . F)))) is complex real ext-real Element of REAL
K64((K62((Re ((S . F) + (f . F)))) + K62((Im ((S . F) + (f . F)))))) is complex real ext-real Element of REAL
|.(S . F).| is complex real ext-real Element of REAL
Re (S . F) is complex real ext-real Element of REAL
K62((Re (S . F))) is complex real ext-real Element of REAL
Im (S . F) is complex real ext-real Element of REAL
K62((Im (S . F))) is complex real ext-real Element of REAL
K62((Re (S . F))) + K62((Im (S . F))) is complex real ext-real Element of REAL
K64((K62((Re (S . F))) + K62((Im (S . F))))) is complex real ext-real Element of REAL
|.(f . F).| is complex real ext-real Element of REAL
Re (f . F) is complex real ext-real Element of REAL
K62((Re (f . F))) is complex real ext-real Element of REAL
Im (f . F) is complex real ext-real Element of REAL
K62((Im (f . F))) is complex real ext-real Element of REAL
K62((Re (f . F))) + K62((Im (f . F))) is complex real ext-real Element of REAL
K64((K62((Re (f . F))) + K62((Im (f . F))))) is complex real ext-real Element of REAL
|.(S . F).| + |.(f . F).| is complex real ext-real Element of REAL
dom (S + f) is Element of K6(X)
(S + f) . F is complex set
|.((S + f) . F).| is complex real ext-real Element of REAL
Re ((S + f) . F) is complex real ext-real Element of REAL
K62((Re ((S + f) . F))) is complex real ext-real Element of REAL
Im ((S + f) . F) is complex real ext-real Element of REAL
K62((Im ((S + f) . F))) is complex real ext-real Element of REAL
K62((Re ((S + f) . F))) + K62((Im ((S + f) . F))) is complex real ext-real Element of REAL
K64((K62((Re ((S + f) . F))) + K62((Im ((S + f) . F))))) is complex real ext-real Element of REAL
dom |.f.| is Element of K6(X)
|.f.| . F is complex real ext-real Element of REAL
dom f is Element of K6(X)
dom |.S.| is Element of K6(X)
dom S is Element of K6(X)
(dom S) /\ (dom f) is Element of K6(X)
dom (|.S.| + |.f.|) is Element of K6(X)
|.S.| . F 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 Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom S is Element of K6(X)
K6(X) is non empty set
f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
f - S is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
F is set
dom (f - S) is Element of K6(X)
dom f is Element of K6(X)
(dom f) /\ (dom S) is Element of K6(X)
f . F is complex real ext-real Element of REAL
S . F is complex real ext-real Element of REAL
(f . F) - (S . F) is complex real ext-real Element of REAL
(f - S) . F is complex real ext-real Element of REAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is non empty Relation-like V46() set
K6(K7(S,ExtREAL)) is non empty set
f is non empty Relation-like S -defined ExtREAL -valued Function-like total V30(S, ExtREAL ) V46() V54() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
F is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
|.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
c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
F + c is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom (F + c) is Element of K6(X)
|.(F + c).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
|.c.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
|.F.| + |.c.| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Im c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (Im 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 (R_EAL (Im c)) is Element of K6(X)
n is Element of S
Im F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (Im F) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (R_EAL (Im F)) is Element of K6(X)
x is Element of S
Re c is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (Re c) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (R_EAL (Re c)) is Element of K6(X)
y is Element of S
dom c is Element of K6(X)
dom |.(F + c).| is Element of K6(X)
k is set
|.(F + c).| . k is complex real ext-real Element of REAL
(|.F.| + |.c.|) . k is complex real ext-real Element of REAL
(|.F.| + |.c.|) - |.(F + c).| is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Re F is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
R_EAL (Re F) is Relation-like X -defined ExtREAL -valued Function-like V46() Element of K6(K7(X,ExtREAL))
dom (R_EAL (Re F)) is Element of K6(X)
k is Element of S
dom F is Element of K6(X)
k /\ y is M11(X,S)
x is Element of S
(dom F) /\ (dom c) is Element of K6(X)
dom |.F.| is Element of K6(X)
dom |.c.| is Element of K6(X)
dom (|.F.| + |.c.|) is Element of K6(X)
(dom |.F.|) /\ (dom |.c.|) is Element of K6(X)
(dom |.(F + c).|) /\ (dom (|.F.| + |.c.|)) is Element of K6(X)
(dom (|.F.| + |.c.|)) /\ (dom |.(F + c).|) is Element of K6(X)
y is Element of S
|.(F + c).| | y is Relation-like X -defined y -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Integral (f,(|.(F + c).| | y)) is ext-real Element of ExtREAL
(|.F.| + |.c.|) | y is Relation-like X -defined y -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Integral (f,((|.F.| + |.c.|) | y)) is ext-real Element of ExtREAL
|.c.| | y is Relation-like X -defined y -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom (|.c.| | y) is Element of K6(X)
|.F.| | y is Relation-like X -defined y -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Integral (f,(|.F.| | y)) is ext-real Element of ExtREAL
Integral (f,(|.c.| | y)) is ext-real Element of ExtREAL
(Integral (f,(|.F.| | y))) + (Integral (f,(|.c.| | y))) is ext-real Element of ExtREAL
dom (|.F.| | y) is Element of K6(X)
(dom (|.F.| | y)) /\ (dom (|.c.| | y)) is Element of K6(X)
(|.F.| | y) + (|.c.| | y) is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Integral (f,((|.F.| | y) + (|.c.| | y))) is ext-real Element of ExtREAL
i is Element of S
(|.F.| | y) | i is Relation-like X -defined i -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Integral (f,((|.F.| | y) | i)) is ext-real Element of ExtREAL
(|.c.| | y) | i is Relation-like X -defined i -defined X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
Integral (f,((|.c.| | y) | i)) is ext-real Element of ExtREAL
(Integral (f,((|.F.| | y) | i))) + (Integral (f,((|.c.| | y) | i))) is ext-real Element of ExtREAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
X is non empty set
K6(X) is non empty set
K6(K6(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 compl-closed sigma-multiplicative Element of K6(K6(X))
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Re 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
Im f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
dom f is Element of K6(X)
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
rng F is Element of K6(S)
K6(S) is non empty set
union (rng F) is set
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
dom (Im f) is Element of K6(X)
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . c is set
n is Element of X
x is Element of X
(Im f) . n is complex real ext-real Element of REAL
(Im f) . x is complex real ext-real Element of REAL
f . n is complex set
Im (f . n) is complex real ext-real Element of REAL
f . x is complex set
Im (f . x) is complex real ext-real Element of REAL
dom (Re f) is Element of K6(X)
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . c is set
n is Element of X
x is Element of X
(Re f) . n is complex real ext-real Element of REAL
(Re f) . x is complex real ext-real Element of REAL
f . n is complex set
Re (f . n) is complex real ext-real Element of REAL
f . x is complex set
Re (f . x) is complex real ext-real Element of REAL
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
rng F is Element of K6(S)
union (rng F) is set
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
len 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
n is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
rng n is Element of K6(S)
union (rng n) is set
dom n is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
len 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
(len F) * (len 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
y is Relation-like Function-like FinSequence-like set
len y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
dom y is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
Seg ((len F) * (len n)) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT : ( 1 <= b₁ & b₁ <= (len F) * (len n) ) } is set
FG is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
FG -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(FG -' 1) mod (len 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
((FG -' 1) mod (len n)) + 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
(FG -' 1) div (len 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
((FG -' 1) div (len n)) + 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
((len F) * (len n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(((len F) * (len n)) -' 1) div (len 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
((len F) * (len n)) div (len 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
(((len F) * (len n)) div (len n)) - 1 is complex real ext-real Element of REAL
F . (((FG -' 1) div (len n)) + 1) is set
n . (((FG -' 1) mod (len n)) + 1) is set
(F . (((FG -' 1) div (len n)) + 1)) /\ (n . (((FG -' 1) mod (len n)) + 1)) is set
y . FG is set
FG is Relation-like NAT -defined S -valued Function-like FinSequence-like FinSequence of S
dom FG is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
FG is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
FG . FG is set
FG . k is set
k -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(k -' 1) mod (len 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
((k -' 1) mod (len n)) + 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
(k -' 1) div (len 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
((k -' 1) div (len n)) + 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
(k -' 1) + 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
(((k -' 1) div (len n)) + 1) - 1 is complex real ext-real Element of REAL
((((k -' 1) div (len n)) + 1) - 1) * (len n) is complex real ext-real Element of REAL
(((k -' 1) mod (len n)) + 1) - 1 is complex real ext-real Element of REAL
(((((k -' 1) div (len n)) + 1) - 1) * (len n)) + ((((k -' 1) mod (len n)) + 1) - 1) is complex real ext-real Element of REAL
((((((k -' 1) div (len n)) + 1) - 1) * (len n)) + ((((k -' 1) mod (len n)) + 1) - 1)) + 1 is complex real ext-real Element of REAL
FG -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(FG -' 1) mod (len 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
((FG -' 1) mod (len n)) + 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
(FG -' 1) div (len 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
((FG -' 1) div (len n)) + 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
F . (((FG -' 1) div (len n)) + 1) is set
n . (((FG -' 1) mod (len n)) + 1) is set
(F . (((FG -' 1) div (len n)) + 1)) /\ (n . (((FG -' 1) mod (len n)) + 1)) is set
(FG . FG) /\ (FG . k) is set
F . (((k -' 1) div (len n)) + 1) is set
n . (((k -' 1) mod (len n)) + 1) is set
(F . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
((F . (((FG -' 1) div (len n)) + 1)) /\ (n . (((FG -' 1) mod (len n)) + 1))) /\ ((F . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(n . (((FG -' 1) mod (len n)) + 1)) /\ ((F . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(F . (((FG -' 1) div (len n)) + 1)) /\ ((n . (((FG -' 1) mod (len n)) + 1)) /\ ((F . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)))) is set
(n . (((FG -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
(F . (((k -' 1) div (len n)) + 1)) /\ ((n . (((FG -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(F . (((FG -' 1) div (len n)) + 1)) /\ ((F . (((k -' 1) div (len n)) + 1)) /\ ((n . (((FG -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)))) is set
(F . (((FG -' 1) div (len n)) + 1)) /\ (F . (((k -' 1) div (len n)) + 1)) is set
((F . (((FG -' 1) div (len n)) + 1)) /\ (F . (((k -' 1) div (len n)) + 1))) /\ ((n . (((FG -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
Seg (len F) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
k - 1 is complex real ext-real Element of REAL
(k - 1) + 1 is complex real ext-real Element of REAL
(((((k -' 1) div (len n)) + 1) - 1) * (len n)) + (((k -' 1) mod (len n)) + 1) is complex real ext-real Element of REAL
Seg (len n) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
(FG -' 1) + 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
(((FG -' 1) div (len n)) + 1) - 1 is complex real ext-real Element of REAL
((((FG -' 1) div (len n)) + 1) - 1) * (len n) is complex real ext-real Element of REAL
(((FG -' 1) mod (len n)) + 1) - 1 is complex real ext-real Element of REAL
(((((FG -' 1) div (len n)) + 1) - 1) * (len n)) + ((((FG -' 1) mod (len n)) + 1) - 1) is complex real ext-real Element of REAL
((((((FG -' 1) div (len n)) + 1) - 1) * (len n)) + ((((FG -' 1) mod (len n)) + 1) - 1)) + 1 is complex real ext-real Element of REAL
FG - 1 is complex real ext-real Element of REAL
(FG - 1) + 1 is complex real ext-real Element of REAL
(((((FG -' 1) div (len n)) + 1) - 1) * (len n)) + (((FG -' 1) mod (len n)) + 1) is complex real ext-real Element of REAL
{} /\ ((n . (((FG -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
((F . (((FG -' 1) div (len n)) + 1)) /\ (F . (((k -' 1) div (len n)) + 1))) /\ {} is set
FG is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
rng FG is Element of K6(S)
union (rng FG) is set
k is set
x is set
y is set
i is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
n . i is set
j is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . j is set
i9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
1 + i9 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
j - 1 is complex real ext-real Element of REAL
(j - 1) * (len n) is complex real ext-real Element of REAL
((j - 1) * (len n)) + i is complex real ext-real Element of REAL
(len F) - 1 is complex real ext-real Element of REAL
((len F) - 1) * (len n) is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(((len F) - 1) * (len n)) + i is complex real ext-real Element of REAL
(((len F) - 1) * (len n)) + (len n) is complex real ext-real Element of REAL
j9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
1 + j9 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
k -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
k - 1 is complex real ext-real Element of REAL
i9 * (len 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
(i9 * (len n)) + j9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(k -' 1) div (len 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
((k -' 1) div (len n)) + 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
(k -' 1) mod (len 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
((k -' 1) mod (len n)) + 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
dom FG is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
FG . k is set
(F . j) /\ (n . i) is set
k is set
x is set
dom FG is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
FG . y is set
y -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(y -' 1) mod (len 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
((y -' 1) mod (len n)) + 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
(y -' 1) div (len 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
((y -' 1) div (len n)) + 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
F . (((y -' 1) div (len n)) + 1) is set
n . (((y -' 1) mod (len n)) + 1) is set
(F . (((y -' 1) div (len n)) + 1)) /\ (n . (((y -' 1) mod (len n)) + 1)) is set
dom FG is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
FG . k is set
x is Element of X
y is Element of X
f . x is complex set
f . y is complex set
k -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT
(k -' 1) div (len 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
((k -' 1) div (len n)) + 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
(k -' 1) mod (len 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
((k -' 1) mod (len n)) + 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
(Im f) . x is complex real ext-real Element of REAL
Im (f . x) is complex real ext-real Element of REAL
(Im f) . y is complex real ext-real Element of REAL
Im (f . y) is complex real ext-real Element of REAL
(Re f) . x is complex real ext-real Element of REAL
Re (f . x) is complex real ext-real Element of REAL
(Re f) . y is complex real ext-real Element of REAL
Re (f . y) is complex real ext-real Element of REAL
F . (((k -' 1) div (len n)) + 1) is set
n . (((k -' 1) mod (len n)) + 1) is set
(F . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom f is Element of K6(X)
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
rng F is Element of K6(S)
K6(S) is non empty set
union (rng F) is set
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
len 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
Seg (len F) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
c is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . c is set
n is complex Element of COMPLEX
x is set
f . x is complex set
n is set
f . n is complex set
rng f is V38() Element of K6(COMPLEX)
K6(COMPLEX) is non empty set
x is complex Element of COMPLEX
bool X is non empty Element of K6(K6(X))
y is set
f . y is complex set
c is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom c is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . n is set
c . n is complex set
x is set
f . x is complex set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
x is set
F . n is set
f . x is complex set
c . n is complex set
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom f is Element of K6(X)
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
rng F is Element of K6(S)
K6(S) is non empty set
union (rng F) is set
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
c is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom c is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
n is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
x is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
c is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . n is set
x is Element of X
y is Element of X
f . x is complex set
f . y is complex set
c . n is complex set
rng F is Element of K6(S)
union (rng F) is set
X is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
Re X is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
X *' is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
X + (X *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
2 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
K445(1,2) is non empty complex real ext-real positive non negative V61() Element of RAT
K445(1,2) * (X + (X *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom (Re X) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(Re X) . S is complex real ext-real Element of REAL
X . S is complex set
Re (X . S) is complex real ext-real Element of REAL
1 / 2 is non empty complex real ext-real positive non negative Element of REAL
(1 / 2) * (X *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
((1 / 2) * (X *')) . S is complex set
(X *') . S is complex set
(1 / 2) * ((X *') . S) is complex set
(1 / 2) * X is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
len ((1 / 2) * 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
len 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
len ((1 / 2) * (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
len (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
(1 / 2) * (X + (X *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
((1 / 2) * X) + ((1 / 2) * (X *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
((1 / 2) * X) . S is complex set
(((1 / 2) * X) . S) + (((1 / 2) * (X *')) . S) is complex set
len (Re 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) *' is complex Element of COMPLEX
Im (X . S) is complex real ext-real Element of REAL
(Im (X . S)) * <i> is complex set
(Re (X . S)) - ((Im (X . S)) * <i>) is complex set
(1 / 2) * ((X . S) *') is complex set
(1 / 2) * (X . S) is complex set
((1 / 2) * (X . S)) + ((1 / 2) * ((X . S) *')) is complex set
(Re (X . S)) + ((Im (X . S)) * <i>) is complex set
X is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
Im X is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
X *' is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
X - (X *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
2 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
K445(1,2) is non empty complex real ext-real positive non negative V61() Element of RAT
K432(K445(1,2),<i>) is complex Element of COMPLEX
K428(K432(K445(1,2),<i>)) is complex Element of COMPLEX
K428(K432(K445(1,2),<i>)) * (X - (X *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom (Im X) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(Im X) . S is complex real ext-real Element of REAL
X . S is complex set
Im (X . S) is complex real ext-real Element of REAL
len (Im 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
len 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
1 / 2 is non empty complex real ext-real positive non negative Element of REAL
(1 / 2) * <i> is complex set
- ((1 / 2) * <i>) is complex set
(- ((1 / 2) * <i>)) * (X *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
((- ((1 / 2) * <i>)) * (X *')) . S is complex set
(X *') . S is complex set
(- ((1 / 2) * <i>)) * ((X *') . S) is complex set
(X . S) *' is complex Element of COMPLEX
Re (X . S) is complex real ext-real Element of REAL
(Im (X . S)) * <i> is complex set
(Re (X . S)) - ((Im (X . S)) * <i>) is complex set
(- ((1 / 2) * <i>)) * ((X . S) *') is complex set
(- ((1 / 2) * <i>)) * X is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
len ((- ((1 / 2) * <i>)) * 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
len ((- ((1 / 2) * <i>)) * (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
len (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
(- ((1 / 2) * <i>)) * (X - (X *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
((- ((1 / 2) * <i>)) * X) - ((- ((1 / 2) * <i>)) * (X *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
((- ((1 / 2) * <i>)) * X) . S is complex set
(((- ((1 / 2) * <i>)) * X) . S) - (((- ((1 / 2) * <i>)) * (X *')) . S) is complex set
(- ((1 / 2) * <i>)) * (X . S) is complex set
((- ((1 / 2) * <i>)) * (X . S)) - ((- ((1 / 2) * <i>)) * ((X . S) *')) is complex set
(X . S) - ((X . S) *') is complex set
(Re (X . S)) + ((Im (X . S)) * <i>) is complex set
((Re (X . S)) + ((Im (X . S)) * <i>)) - ((Re (X . S)) - ((Im (X . S)) * <i>)) is complex set
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
Re 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
Im f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
c is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
Re c is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
c *' is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
c + (c *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
2 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
K445(1,2) is non empty complex real ext-real positive non negative V61() Element of RAT
K445(1,2) * (c + (c *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
Im c is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
c - (c *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
K432(K445(1,2),<i>) is complex Element of COMPLEX
K428(K432(K445(1,2),<i>)) is complex Element of COMPLEX
K428(K432(K445(1,2),<i>)) * (c - (c *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
len (Im 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
len 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
dom (Im c) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
Seg (len c) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT : ( 1 <= b₁ & b₁ <= len c ) } is set
dom c is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
dom (Im f) is Element of K6(X)
dom f is Element of K6(X)
rng F is Element of K6(S)
K6(S) is non empty set
union (rng F) is set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . n is set
(Im c) . n is complex real ext-real Element of REAL
x is set
(Im f) . x is complex real ext-real Element of REAL
f . x is complex set
Im (f . x) is complex real ext-real Element of REAL
c . n is complex set
Im (c . n) is complex real ext-real Element of REAL
len (Re 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
dom (Re c) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
dom (Re f) is Element of K6(X)
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . n is set
(Re c) . n is complex real ext-real Element of REAL
x is set
(Re f) . x is complex real ext-real Element of REAL
f . x is complex set
Re (f . x) is complex real ext-real Element of REAL
c . n is complex set
Re (c . n) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . n is set
c . n is complex set
x is set
f . x is complex set
(Im f) . x is complex real ext-real Element of REAL
Im (f . x) is complex real ext-real Element of REAL
(Re f) . x is complex real ext-real Element of REAL
Re (f . x) is complex real ext-real Element of REAL
(Im c) . n is complex real ext-real Element of REAL
Im (c . n) is complex real ext-real Element of REAL
(Re c) . n is complex real ext-real Element of REAL
Re (c . n) is complex real ext-real Element of REAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,COMPLEX) is non empty Relation-like V45() set
K6(K7(X,COMPLEX)) is non empty set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
f is Relation-like X -defined COMPLEX -valued Function-like V45() Element of K6(K7(X,COMPLEX))
dom f is Element of K6(X)
Re 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
Im f is Relation-like X -defined REAL -valued Function-like V45() V46() V47() Element of K6(K7(X,REAL))
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
c is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
Im c is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
c *' is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
c - (c *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
2 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
K445(1,2) is non empty complex real ext-real positive non negative V61() Element of RAT
K432(K445(1,2),<i>) is complex Element of COMPLEX
K428(K432(K445(1,2),<i>)) is complex Element of COMPLEX
K428(K432(K445(1,2),<i>)) * (c - (c *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
x is set
F . n is set
(Im f) . x is complex real ext-real Element of REAL
(Im c) . n is complex real ext-real Element of REAL
Re c is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
c + (c *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
K445(1,2) * (c + (c *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
x is set
F . n is set
(Re f) . x is complex real ext-real Element of REAL
(Re c) . n is complex real ext-real Element of REAL
rng F is Element of K6(S)
K6(S) is non empty set
union (rng F) is set
dom c is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
F is Relation-like NAT -defined S -valued Function-like FinSequence-like V92() FinSequence of S
rng F is Element of K6(S)
union (rng F) is set
dom F is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
c is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom c is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
Re c is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
c *' is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
c + (c *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
K445(1,2) * (c + (c *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
Im c is Relation-like NAT -defined REAL -valued Function-like V45() V46() V47() FinSequence-like FinSequence of REAL
c - (c *') is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
K428(K432(K445(1,2),<i>)) * (c - (c *')) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSequence of COMPLEX
dom (Im f) is Element of K6(X)
len (Im 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
len 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
dom (Im c) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
Seg (len c) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V38() V39() V40() V41() V42() V43() V60() V61() Element of NAT : ( 1 <= b₁ & b₁ <= len c ) } is set
len (Re 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
dom (Re c) is V38() V39() V40() V41() V42() V43() Element of K6(NAT)
dom (Re f) is Element of K6(X)
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
F . n is set
c . n is complex set
x is set
f . x is complex set
(Im f) . x is complex real ext-real Element of REAL
Im (f . x) is complex real ext-real Element of REAL
(Re f) . x is complex real ext-real Element of REAL
Re (f . x) is complex real ext-real Element of REAL
(Im c) . n is complex real ext-real Element of REAL
Im (c . n) is complex real ext-real Element of REAL
(Re c) . n is complex real ext-real Element of REAL
Re (c . n) is complex real ext-real Element of REAL