:: MESFUN9C semantic presentation

REAL is non empty V29() V40() V41() V42() V46() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V40() V41() V42() V43() V44() V45() V46() Element of K6(REAL)
K6(REAL) is set
ExtREAL is non empty V41() set
K7(NAT,ExtREAL) is V58() set
K6(K7(NAT,ExtREAL)) is set
K6(ExtREAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V40() V41() V42() V43() V44() V45() V46() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is V57() V58() V59() set
K6(K7(NAT,REAL)) is set
COMPLEX is non empty V29() V40() V46() set
RAT is non empty V29() V40() V41() V42() V43() V46() set
INT is non empty V29() V40() V41() V42() V43() V44() V46() set
K7(NAT,COMPLEX) is V57() set
K6(K7(NAT,COMPLEX)) is set
K6(K6(REAL)) is set
K6(RAT) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V40() V41() V42() V43() V44() V45() V46() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
{{},1} is non empty V40() V41() V42() V43() V44() V45() set
K129() is non empty non real ext-real positive non negative Element of ExtREAL
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V40() V41() V42() V43() V44() V45() V46() V72() V74() Element of NAT
K130() is non empty non real ext-real non positive negative Element of ExtREAL
<i> is complex Element of COMPLEX
X is set
S is set
PFuncs (X,S) is non empty functional set
K7(NAT,(PFuncs (X,S))) is set
K6(K7(NAT,(PFuncs (X,S)))) is set
M is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V51( NAT , PFuncs (X,S)) Element of K6(K7(NAT,(PFuncs (X,S))))
E is set
K7(X,S) is set
K6(K7(X,S)) is set
F is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V51( NAT , PFuncs (X,S)) Element of K6(K7(NAT,(PFuncs (X,S))))
F is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V51( NAT , PFuncs (X,S)) Element of K6(K7(NAT,(PFuncs (X,S))))
f is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V51( NAT , PFuncs (X,S)) Element of K6(K7(NAT,(PFuncs (X,S))))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
F . I is set
f . I is set
F . I is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
K7(X,S) is set
K6(K7(X,S)) is set
M . I is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
(M . I) | E is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
f . I is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is Element of X
S # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
E is set
(X,REAL,S,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,S,E) # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
R_EAL (X,REAL,S,E) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
(R_EAL (X,REAL,S,E)) # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
R_EAL (S # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(R_EAL S) # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL (X,REAL,S,E)) . f is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
(R_EAL S) . f is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
((R_EAL S) . f) | E is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
X is set
S is set
PFuncs (X,S) is non empty functional set
K7(NAT,(PFuncs (X,S))) is set
K6(K7(NAT,(PFuncs (X,S)))) is set
M is set
E is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V51( NAT , PFuncs (X,S)) Element of K6(K7(NAT,(PFuncs (X,S))))
(X,S,E,M) is non empty Relation-like NAT -defined PFuncs (X,S) -valued Function-like total V51( NAT , PFuncs (X,S)) Element of K6(K7(NAT,(PFuncs (X,S))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S,E,M) . F is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
K7(X,S) is set
K6(K7(X,S)) is set
dom ((X,S,E,M) . F) is Element of K6(X)
K6(X) is set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S,E,M) . f is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
dom ((X,S,E,M) . f) is Element of K6(X)
E . f is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
(E . f) | M is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
dom (E . f) is Element of K6(X)
(dom (E . f)) /\ M is Element of K6(X)
E . F is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
(E . F) | M is Relation-like X -defined S -valued Function-like Element of K6(K7(X,S))
dom (E . F) is Element of K6(X)
(dom (E . F)) /\ M is Element of K6(X)
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (S . 0) is Element of K6(X)
K6(X) is set
lim S is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL S) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
M is set
(lim S) | M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(X,REAL,S,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
lim (X,REAL,S,M) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (X,REAL,S,M) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (X,REAL,S,M)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
F is Element of X
(R_EAL S) # F is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
S # F is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL (X,REAL,S,M)) . F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(R_EAL S) . F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
((R_EAL S) . F) | M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
E . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (E . 0) is Element of K6(X)
(X,REAL,E,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,REAL,E,M) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL E is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
R_EAL (X,REAL,E,M) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL E) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
(R_EAL (X,REAL,E,M)) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
((R_EAL E) . I) | M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
E . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (E . I) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL ((X,REAL,E,M) . F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
X is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
R_EAL X is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Partial_Sums (R_EAL X) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Partial_Sums X is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
R_EAL (Partial_Sums X) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Partial_Sums (R_EAL X)) . S is ext-real Element of ExtREAL
(R_EAL (Partial_Sums X)) . S is ext-real Element of ExtREAL
S + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Partial_Sums (R_EAL X)) . (S + 1) is ext-real Element of ExtREAL
(R_EAL (Partial_Sums X)) . (S + 1) is ext-real Element of ExtREAL
(Partial_Sums X) . S is complex real ext-real Element of REAL
R_EAL ((Partial_Sums X) . S) is ext-real Element of ExtREAL
X . (S + 1) is complex real ext-real Element of REAL
R_EAL (X . (S + 1)) is ext-real Element of ExtREAL
(R_EAL ((Partial_Sums X) . S)) + (R_EAL (X . (S + 1))) is ext-real Element of ExtREAL
((Partial_Sums X) . S) + (X . (S + 1)) is complex real ext-real Element of REAL
R_EAL (((Partial_Sums X) . S) + (X . (S + 1))) is ext-real Element of ExtREAL
(Partial_Sums (R_EAL X)) . 0 is ext-real Element of ExtREAL
X . 0 is complex real ext-real Element of REAL
R_EAL (X . 0) is ext-real Element of ExtREAL
(R_EAL (Partial_Sums X)) . 0 is ext-real Element of ExtREAL
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,E,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
f is Element of X
(X,REAL,E,M) # f is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
E # f is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(E # f) . I is complex real ext-real Element of REAL
((X,REAL,E,M) # f) . I is complex real ext-real Element of REAL
E . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(E . I) . f is complex real ext-real Element of REAL
(E . I) | M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((E . I) | M) . f is complex real ext-real Element of REAL
(X,REAL,E,M) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((X,REAL,E,M) . I) . f is complex real ext-real Element of REAL
Partial_Sums (E # f) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums ((X,REAL,E,M) # f) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
S . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
S . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E is set
F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F + (S . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
I + (S . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M is Relation-like Function-like set
dom M is set
M . 0 is set
E is set
rng M is set
F is set
M . F is set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . I is set
I + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . (I + 1) is set
A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S . (I + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
A + (S . (I + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . f is set
E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
E . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
E . (F + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S . (F + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(E . F) + (S . (F + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
E . (F + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S . (F + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(E . F) + (S . (F + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
E . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
M . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . (F + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . (F + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S . (F + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(M . F) + (S . (F + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
PFuncs (X,ExtREAL) is non empty functional set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
K7(NAT,(PFuncs (X,ExtREAL))) is set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
Partial_Sums (R_EAL S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
R_EAL (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Partial_Sums (R_EAL S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
(R_EAL (X,S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
M + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Partial_Sums (R_EAL S)) . (M + 1) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(R_EAL (X,S)) . (M + 1) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(X,S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
R_EAL ((X,S) . M) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
S . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (S . (M + 1)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(R_EAL ((X,S) . M)) + (R_EAL (S . (M + 1))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
((X,S) . M) + (S . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (((X,S) . M) + (S . (M + 1))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(Partial_Sums (R_EAL S)) . 0 is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
(R_EAL S) . 0 is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(X,S) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
R_EAL ((X,S) . 0) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(R_EAL (X,S)) . 0 is Relation-like X -defined ExtREAL -valued Function-like V58() 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((X,S) . M) is Element of K6(X)
K6(X) is set
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((X,S) . E) is Element of K6(X)
S . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom (S . E) is Element of K6(X)
F is set
R_EAL (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
(R_EAL (X,S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
Partial_Sums (R_EAL S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(Partial_Sums (R_EAL S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(Partial_Sums (R_EAL S)) . E is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(R_EAL (X,S)) . E is Relation-like X -defined ExtREAL -valued Function-like V58() 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F is set
(R_EAL S) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
dom ((R_EAL S) . M) is Element of K6(X)
K6(X) is set
(R_EAL S) . E is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom ((R_EAL S) . E) is Element of K6(X)
(dom ((R_EAL S) . M)) /\ (dom ((R_EAL S) . E)) is Element of K6(X)
S . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
R_EAL (S . M) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
((R_EAL S) . M) . F is ext-real Element of ExtREAL
+infty is non empty non real ext-real positive non negative set
((R_EAL S) . E) . F is ext-real Element of ExtREAL
-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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((X,S) . M) is Element of K6(X)
K6(X) is set
{ (dom (S . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= M } is set
meet { (dom (S . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= M } is set
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
Partial_Sums (R_EAL S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(Partial_Sums (R_EAL S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
dom ((Partial_Sums (R_EAL S)) . M) is Element of K6(X)
{ (dom ((R_EAL S) . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= M } is set
meet { (dom ((R_EAL S) . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= M } is set
R_EAL (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(R_EAL (X,S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (S . 0) is Element of K6(X)
K6(X) is set
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((X,S) . M) is Element of K6(X)
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
Partial_Sums (R_EAL S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(Partial_Sums (R_EAL S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
dom ((Partial_Sums (R_EAL S)) . M) is Element of K6(X)
(R_EAL S) . 0 is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom ((R_EAL S) . 0) is Element of K6(X)
R_EAL (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(R_EAL (X,S)) . M is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom ((R_EAL (X,S)) . M) is Element of K6(X)
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (S . 0) is Element of K6(X)
K6(X) is set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
E is Element of X
S # E is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums (S # E) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Partial_Sums (S # E)) . M is complex real ext-real Element of REAL
(X,S) # E is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((X,S) # E) . M is complex real ext-real Element of REAL
F is set
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
(R_EAL S) # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Partial_Sums ((R_EAL S) # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
(Partial_Sums ((R_EAL S) # E)) . M is ext-real Element of ExtREAL
Partial_Sums (R_EAL S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(Partial_Sums (R_EAL S)) # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
((Partial_Sums (R_EAL S)) # E) . M is ext-real Element of ExtREAL
R_EAL (S # E) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Partial_Sums (R_EAL (S # E)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
(Partial_Sums (R_EAL (S # E))) . M is ext-real Element of ExtREAL
R_EAL (Partial_Sums (S # E)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
(R_EAL (Partial_Sums (S # E))) . M is ext-real Element of ExtREAL
R_EAL ((Partial_Sums (S # E)) . M) is ext-real Element of ExtREAL
R_EAL (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(R_EAL (X,S)) # E is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
((R_EAL (X,S)) # E) . M 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (S . 0) is Element of K6(X)
K6(X) is set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is Element of X
S # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums (S # M) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,S) # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
E is set
R_EAL (S # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
R_EAL S is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
(R_EAL S) # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Partial_Sums (R_EAL S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
R_EAL (X,S) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(Partial_Sums (R_EAL S)) # M is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
R_EAL (Partial_Sums (S # M)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Partial_Sums (R_EAL (S # M)) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Partial_Sums ((R_EAL S) # M) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
S . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom (S . 0) is Element of K6(X)
K6(X) is set
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom M is Element of K6(X)
E is Element of X
M . E is complex real ext-real Element of REAL
S # E is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Sum (S # E) is complex real ext-real Element of REAL
Partial_Sums (S # E) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim (Partial_Sums (S # E)) is complex real ext-real Element of REAL
(X,S) # E is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim ((X,S) # E) is complex real ext-real Element of REAL
dom (Partial_Sums (S # E)) is V40() V41() V42() V43() V44() V45() Element of K6(NAT)
dom ((X,S) # E) is V40() V41() V42() V43() V44() V45() Element of K6(NAT)
F is set
(Partial_Sums (S # E)) . F is complex real ext-real Element of REAL
((X,S) # E) . F is complex real ext-real Element of REAL
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,M) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
R_EAL M is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL M) . F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
M . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (M . F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Partial_Sums (R_EAL M) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(Partial_Sums (R_EAL M)) . E is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (X,M) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(R_EAL (X,M)) . E is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL ((X,M) . E) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,E) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,E) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
I + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(X,E) . (I + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . (I + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((X,E) . I) + (E . (I + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,E) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((X,S) . M) is Element of K6(X)
K6(X) is set
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,S) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((X,S) . E) is Element of K6(X)
S . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom (S . 0) is Element of K6(X)
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
E . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (E . 0) is Element of K6(X)
(X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
lim (X,E) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (X,E) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL (X,E)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
F is Element of X
E # F is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums (E # F) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,E) # F is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,E) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((X,E) . 0) is Element of K6(X)
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,E) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
R_EAL E is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL E) . f is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
E . f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (E . f) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Partial_Sums (R_EAL E) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(Partial_Sums (R_EAL E)) . F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (X,E) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
(R_EAL (X,E)) . F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL ((X,E) . F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
X is non empty set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Im S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M is set
(Re S) | M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S | M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re (S | M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im S) | M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (S | M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re S) | M) is Element of K6(X)
K6(X) is set
dom (Re S) is Element of K6(X)
(dom (Re S)) /\ M is Element of K6(X)
dom S is Element of K6(X)
(dom S) /\ M is Element of K6(X)
dom (S | M) is Element of K6(X)
dom (Re (S | M)) is Element of K6(X)
E is set
(Re (S | M)) . E is complex real ext-real Element of REAL
(S | M) . E is complex set
Re ((S | M) . E) is complex real ext-real Element of REAL
S . E is complex set
Re (S . E) is complex real ext-real Element of REAL
(Re S) . E is complex real ext-real Element of REAL
((Re S) | M) . E is complex real ext-real Element of REAL
dom ((Im S) | M) is Element of K6(X)
dom (Im S) is Element of K6(X)
(dom (Im S)) /\ M is Element of K6(X)
dom (Im (S | M)) is Element of K6(X)
E is set
(Im (S | M)) . E is complex real ext-real Element of REAL
(S | M) . E is complex set
Im ((S | M) . E) is complex real ext-real Element of REAL
S . E is complex set
Im (S . E) is complex real ext-real Element of REAL
(Im S) . E is complex real ext-real Element of REAL
((Im S) | M) . E 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 set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is set
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re (X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Re M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
Im (X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
Im M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re (X,COMPLEX,M,S)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(Re M) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Re M) . F) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im (X,COMPLEX,M,S)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im M) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Im M) . F) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
(M . F) | S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re ((M . F) | S) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (M . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re (M . F)) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im ((M . F) | S) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (M . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im (M . F)) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,COMPLEX,M,S) . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re ((X,COMPLEX,M,S) . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im ((X,COMPLEX,M,S) . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
PFuncs (X,REAL) is non empty functional set
S is set
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re (X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Re M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Re M),S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re (X,COMPLEX,M,S)) . E is set
(X,REAL,(Re M),S) . E is set
(Re (X,COMPLEX,M,S)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(Re M) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Re M) . E) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
PFuncs (X,REAL) is non empty functional set
S is set
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Im (X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Im M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Im M),S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Im (X,COMPLEX,M,S)) . E is set
(X,REAL,(Im M),S) . E is set
(Im (X,COMPLEX,M,S)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(Im M) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Im M) . E) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is Element of X
M is set
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
E . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (E . 0) is Element of K6(X)
K6(X) is set
E # S is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(X,COMPLEX,E,M) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,COMPLEX,E,M) # S is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
PFuncs (X,REAL) is non empty functional set
Re (X,COMPLEX,E,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Re E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Re E),M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re E) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re (X,COMPLEX,E,M)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re E) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Re E) . 0) is Element of K6(X)
((Re E) . 0) | M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom (((Re E) . 0) | M) is Element of K6(X)
(Re (X,COMPLEX,E,M)) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re (X,COMPLEX,E,M)) . 0) is Element of K6(X)
(X,COMPLEX,E,M) . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,COMPLEX,E,M) . 0) is Element of K6(X)
Re ((X,COMPLEX,E,M) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (X,COMPLEX,E,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,COMPLEX,E,M)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im ((X,COMPLEX,E,M) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Im E),M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im E) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re (E # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (E # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() 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 set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Re S) . M) is Element of K6(X)
K6(X) is set
S . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (S . M) is Element of K6(X)
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re S) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re S) . E) is Element of K6(X)
S . E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom (S . E) is Element of K6(X)
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Im S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Im S) . M) is Element of K6(X)
K6(X) is set
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im S) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Im S) . E) is Element of K6(X)
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im S) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Im S) . M) is Element of K6(X)
K6(X) is set
S . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (S . M) is Element of K6(X)
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im S) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Im S) . E) is Element of K6(X)
S . E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom (S . E) is Element of K6(X)
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is set
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
M . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (M . 0) is Element of K6(X)
K6(X) is set
lim M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(lim M) | S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
lim (X,COMPLEX,M,S) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
PFuncs (X,REAL) is non empty functional set
Re (X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Re M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Re M),S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(M . 0) | S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((M . 0) | S) is Element of K6(X)
(X,COMPLEX,M,S) . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,COMPLEX,M,S) . 0) is Element of K6(X)
F is Element of X
M # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(X,COMPLEX,M,S) # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
F is Element of X
(Re M) # F is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
M # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re (M # F) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re M) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Re M) . 0) is Element of K6(X)
lim (Re M) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (Re M) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL (Re M)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(lim (Re M)) | S is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
lim (Re (X,COMPLEX,M,S)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Re (X,COMPLEX,M,S)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Re (X,COMPLEX,M,S))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Re (lim M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re (lim M)) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (lim (X,COMPLEX,M,S)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re ((lim M) | S) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is Element of X
(Im M) # F is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
M # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Im (M # F) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (X,COMPLEX,M,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Im M),S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im M) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Im M) . 0) is Element of K6(X)
lim (Im M) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Im M) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Im M)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(lim (Im M)) | S is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
lim (Im (X,COMPLEX,M,S)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Im (X,COMPLEX,M,S)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Im (X,COMPLEX,M,S))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Im (lim M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im (lim M)) | S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (lim (X,COMPLEX,M,S)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im ((lim M) | S) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
<i> (#) (Im (lim (X,COMPLEX,M,S))) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(Re (lim (X,COMPLEX,M,S))) + (<i> (#) (Im (lim (X,COMPLEX,M,S)))) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
F . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (F . 0) is Element of K6(X)
(X,COMPLEX,F,M) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,COMPLEX,F,M) . E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
PFuncs (X,REAL) is non empty functional set
Re (X,COMPLEX,F,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Re F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Re F),M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
Im (X,COMPLEX,F,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
Im F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Im F),M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(Im F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re (F . I) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (F . I) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Im F) . 0) is Element of K6(X)
(Im (X,COMPLEX,F,M)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im ((X,COMPLEX,F,M) . E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re F) . 0) is Element of K6(X)
(Re (X,COMPLEX,F,M)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re ((X,COMPLEX,F,M) . E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
E . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (E . 0) is Element of K6(X)
(X,COMPLEX,E,M) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Im E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
f is Element of X
(Im E) # f is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
E # f is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Im (E # f) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
f is Element of X
(Re E) # f is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
E # f is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re (E # f) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
f is Element of X
(X,COMPLEX,E,M) . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(E . 0) | M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,COMPLEX,E,M) . 0) is Element of K6(X)
Im (X,COMPLEX,E,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Im E),M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,COMPLEX,E,M)) # f is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,COMPLEX,E,M) # f is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Im ((X,COMPLEX,E,M) # f) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re (X,COMPLEX,E,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,REAL,(Re E),M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,COMPLEX,E,M)) # f is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re ((X,COMPLEX,E,M) # f) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() 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 set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
S . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
S . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
M + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
S . (M + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E is set
F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
F + (S . (M + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
f is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
I + (S . (M + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
f is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
M is Relation-like Function-like set
dom M is set
M . 0 is set
E is set
rng M is set
F is set
M . F is set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . I is set
I + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . (I + 1) is set
A is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
S . (I + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
A + (S . (I + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . f is set
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
E . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
E . (F + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
S . (F + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(E . F) + (S . (F + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
E . (f + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E . f is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
S . (f + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(E . f) + (S . (f + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
E . (F + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
S . (F + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(E . F) + (S . (F + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
M . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
E . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
M . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
F + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . (F + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E . (F + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
S . (F + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(M . F) + (S . (F + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
PFuncs (X,REAL) is non empty functional set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(X,(Re S)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re (X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
Im S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Im S)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
Im (X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(X,(Re S)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(Re (X,S)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(X,(Re S)) . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re (X,S)) . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re S) . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Re (X,S)) . M) + ((Re S) . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S . (M + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Re (S . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Re (X,S)) . M) + (Re (S . (M + 1))) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,S) . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re ((X,S) . M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re ((X,S) . M)) + (Re (S . (M + 1))) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((X,S) . M) + (S . (M + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re (((X,S) . M) + (S . (M + 1))) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,S) . (M + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re ((X,S) . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(X,(Im S)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(Im (X,S)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
M + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(X,(Im S)) . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im (X,S)) . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im S) . (M + 1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Im (X,S)) . M) + ((Im S) . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S . (M + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Im (S . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Im (X,S)) . M) + (Im (S . (M + 1))) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,S) . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im ((X,S) . M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im ((X,S) . M)) + (Im (S . (M + 1))) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((X,S) . M) + (S . (M + 1)) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im (((X,S) . M) + (S . (M + 1))) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,S) . (M + 1) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im ((X,S) . (M + 1)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,(Im S)) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(Im S) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
S . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Im (S . 0) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,S) . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im ((X,S) . 0) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im (X,S)) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,(Re S)) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re S) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (S . 0) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re ((X,S) . 0) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re (X,S)) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
E is set
F is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,F) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,F) . S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom ((X,F) . S) is Element of K6(X)
K6(X) is set
(X,F) . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,F) . M) is Element of K6(X)
F . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom (F . M) is Element of K6(X)
Re (X,F) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(Re (X,F)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Re (X,F)) . S) is Element of K6(X)
Re F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re F)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re F)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((X,(Re F)) . S) is Element of K6(X)
(X,(Re F)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((X,(Re F)) . M) is Element of K6(X)
(Re (X,F)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re (X,F)) . M) is Element of K6(X)
(Re F) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re F) . M) is Element of K6(X)
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,M) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,M) . S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom ((X,M) . S) is Element of K6(X)
K6(X) is set
{ (dom (M . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= S } is set
meet { (dom (M . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= S } is set
E is set
Re M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
{ (dom ((Re M) . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= S } is set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re M) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Re M) . F) is Element of K6(X)
M . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom (M . F) is Element of K6(X)
E is set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
M . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom (M . F) is Element of K6(X)
(Re M) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re M) . F) is Element of K6(X)
(X,(Re M)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re M)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((X,(Re M)) . S) is Element of K6(X)
Re (X,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,M)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re (X,M)) . S) is Element of K6(X)
meet { (dom ((Re M) . b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT : b₁ <= S } is set
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,M) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,M) . S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom ((X,M) . S) is Element of K6(X)
K6(X) is set
M . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom (M . 0) is Element of K6(X)
Re M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(X,(Re M)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re M)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((X,(Re M)) . S) is Element of K6(X)
(Re M) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re M) . 0) is Element of K6(X)
Re (X,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,M)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re (X,M)) . S) is Element of K6(X)
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
M is Element of X
E is set
F is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
F . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (F . 0) is Element of K6(X)
K6(X) is set
F # M is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Partial_Sums (F # M) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(Partial_Sums (F # M)) . S is complex Element of COMPLEX
(X,F) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,F) # M is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
((X,F) # M) . S is complex Element of COMPLEX
Im F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(Im F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Im F) . 0) is Element of K6(X)
(X,F) . S is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,F) . S) is Element of K6(X)
Re ((X,F) . S) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom (Re ((X,F) . S)) is Element of K6(X)
Re F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im F) # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums ((Im F) # M) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Partial_Sums ((Im F) # M)) . S is complex real ext-real Element of REAL
(X,(Im F)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Im F)) # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((X,(Im F)) # M) . S is complex real ext-real Element of REAL
(Re F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re F) . 0) is Element of K6(X)
(Re F) # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums ((Re F) # M) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Partial_Sums ((Re F) # M)) . S is complex real ext-real Element of REAL
(X,(Re F)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re F)) # M is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((X,(Re F)) # M) . S is complex real ext-real Element of REAL
Re ((Partial_Sums (F # M)) . S) is complex real ext-real Element of REAL
Re (Partial_Sums (F # M)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re (Partial_Sums (F # M))) . S is complex real ext-real Element of REAL
Re (F # M) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums (Re (F # M)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Partial_Sums (Re (F # M))) . S is complex real ext-real Element of REAL
(X,(Re F)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((X,(Re F)) . S) . M is complex real ext-real Element of REAL
Re (X,F) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,F)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Re (X,F)) . S) . M is complex real ext-real Element of REAL
(Re ((X,F) . S)) . M is complex real ext-real Element of REAL
((X,F) . S) . M is complex set
Re (((X,F) . S) . M) is complex real ext-real Element of REAL
Re (((X,F) # M) . S) is complex real ext-real Element of REAL
Im ((X,F) . S) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom (Im ((X,F) . S)) is Element of K6(X)
Im ((Partial_Sums (F # M)) . S) is complex real ext-real Element of REAL
Im (Partial_Sums (F # M)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im (Partial_Sums (F # M))) . S is complex real ext-real Element of REAL
Im (F # M) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums (Im (F # M)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Partial_Sums (Im (F # M))) . S is complex real ext-real Element of REAL
(X,(Im F)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((X,(Im F)) . S) . M is complex real ext-real Element of REAL
Im (X,F) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,F)) . S is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Im (X,F)) . S) . M is complex real ext-real Element of REAL
(Im ((X,F) . S)) . M is complex real ext-real Element of REAL
Im (((X,F) . S) . M) is complex real ext-real Element of REAL
Im (((X,F) # M) . S) is complex real ext-real Element of REAL
(Im ((Partial_Sums (F # M)) . S)) * <i> is complex set
(Re ((Partial_Sums (F # M)) . S)) + ((Im ((Partial_Sums (F # M)) . S)) * <i>) is complex set
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,S) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re S is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(X,(Re S)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
Re (X,S) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
X is non empty set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is Element of X
M is set
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
E . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (E . 0) is Element of K6(X)
K6(X) is set
E # S is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Partial_Sums (E # S) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(X,E) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,E) # S is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(Re E) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Re E) . 0) is Element of K6(X)
Im E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im E) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Im E) . 0) is Element of K6(X)
(X,E) . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,E) . 0) is Element of K6(X)
Im (Partial_Sums (E # S)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (E # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums (Im (E # S)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im E) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums ((Im E) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,(Im E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Im E)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,E)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im ((X,E) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re (Partial_Sums (E # S)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re (E # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums (Re (E # S)) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re E) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Partial_Sums ((Re E) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,(Re E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re E)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,E)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re ((X,E) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() 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 set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is Element of X
M is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
M . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom (M . 0) is Element of K6(X)
K6(X) is set
M # S is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Sum (M # S) is complex Element of COMPLEX
(X,M) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,M) # S is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
lim ((X,M) # S) is complex Element of COMPLEX
E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom E is Element of K6(X)
E . S is complex set
Re E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (Re E) is Element of K6(X)
Re M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(Re M) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re M) . 0) is Element of K6(X)
Partial_Sums (M # S) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re ((X,M) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim (Re ((X,M) # S)) is complex real ext-real Element of REAL
Re (lim ((X,M) # S)) is complex real ext-real Element of REAL
Im ((X,M) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim (Im ((X,M) # S)) is complex real ext-real Element of REAL
Im (lim ((X,M) # S)) is complex real ext-real Element of REAL
Im E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom (Im E) is Element of K6(X)
Im M is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im M) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Im M) . 0) is Element of K6(X)
(Im E) . S is complex real ext-real Element of REAL
Im (E . S) is complex real ext-real Element of REAL
(X,M) . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,M) . 0) is Element of K6(X)
Re (X,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,M)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,(Re M)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re M)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim ((X,(Re M)) # S) is complex real ext-real Element of REAL
Im (X,M) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,M)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,(Im M)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Im M)) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim ((X,(Im M)) # S) is complex real ext-real Element of REAL
(Re E) . S is complex real ext-real Element of REAL
Re (E . S) is complex real ext-real Element of REAL
Re (M # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re M) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (M # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im M) # S is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Sum ((Re M) # S) is complex real ext-real Element of REAL
Partial_Sums ((Re M) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim (Partial_Sums ((Re M) # S)) is complex real ext-real Element of REAL
Sum ((Im M) # S) is complex real ext-real Element of REAL
Partial_Sums ((Im M) # S) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim (Partial_Sums ((Im M) # S)) is complex real ext-real Element of REAL
(Sum ((Im M) # S)) * <i> is complex set
(Sum ((Re M) # S)) + ((Sum ((Im M) # S)) * <i>) is complex set
Re (Sum (M # S)) is complex real ext-real Element of REAL
Im (Sum (M # S)) is complex real ext-real Element of REAL
(Im (E . S)) * <i> is complex set
(Re (E . S)) + ((Im (E . S)) * <i>) is complex set
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,E) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,E) . M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Im E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im E) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im (E . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,(Im E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Im E)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Im (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,E)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im ((X,E) . M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re E) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re (E . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,(Re E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re E)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,E)) . M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re ((X,E) . M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Re F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(Re F) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Im F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im F) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F . E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Re (F . E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (F . E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,F) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,F) . E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Im F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im F) . f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
(X,(Im F)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Im F)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Im (X,F) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,F)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im ((X,F) . E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re F) . f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,(Re F)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re F)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (X,F) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,F)) . E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re ((X,F) . E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Element of S
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
E . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (E . 0) is Element of K6(X)
(X,E) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
lim (X,E) is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(Im E) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Im E) . 0) is Element of K6(X)
(X,E) . 0 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom ((X,E) . 0) is Element of K6(X)
F is Element of X
(X,E) # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
E # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Partial_Sums (E # F) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(X,(Im E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,(Im E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,E) . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im ((X,E) . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F is Element of X
(Im E) # F is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
E # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Im (E # F) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Re E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
lim (X,(Im E)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (X,(Im E)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL (X,(Im E))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Im (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
lim (Im (X,E)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Im (X,E)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Im (X,E))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
F is Element of X
(Re E) # F is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
E # F is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re (E # F) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(X,(Re E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,(Re E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,E) . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re ((X,E) . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (lim (X,E)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (Im (lim (X,E))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(Re E) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re E) . 0) is Element of K6(X)
lim (X,(Re E)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (X,(Re E)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (X,(Re E))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Re (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
lim (Re (X,E)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Re (X,E)) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Re (X,E))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Re (lim (X,E)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (Re (lim (X,E))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
(X,E) is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( NAT , PFuncs (X,COMPLEX)) Element of K6(K7(NAT,(PFuncs (X,COMPLEX))))
Im E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im E) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Im (E . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re E is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re E) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
E . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
Re (E . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(X,E) . F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
(X,(Im E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Im E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Im (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im (X,E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im ((X,E) . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(X,(Re E)) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(X,(Re E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (X,E) is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re (X,E)) . F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re ((X,E) . F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E is Element of S
Im M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Re M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E is Element of S
M | E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
R_EAL (Im M) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
(Im M) | E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL ((Im M) | E) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Im (M | E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (Re M) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(Re M) | E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL ((Re M) | E) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Re (M | E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
dom M is Element of K6(X)
E is Relation-like NAT -defined S -valued Function-like V37() V134() M5(S)
rng E is Element of K6(S)
K6(S) is set
union (rng E) is set
dom E is V40() V41() V42() V43() V44() V45() Element of K6(NAT)
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
M + E is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Im E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im M) + (Im E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (M + E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re E is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re M) + (Re E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (M + E) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
E is complex set
E (#) M is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
Im E is complex real ext-real Element of REAL
(Im E) (#) (Re M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im M is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im E) (#) (Im M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
- 1 is non empty complex real ext-real non positive negative Element of REAL
(- 1) (#) ((Im E) (#) (Im M)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
- ((Im E) (#) (Im M)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) ((Im E) (#) (Im M)) is Relation-like Function-like set
R_EAL (- ((Im E) (#) (Im M))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
Re E is complex real ext-real Element of REAL
(Re E) (#) (Re M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL ((Re E) (#) (Re M)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(R_EAL ((Re E) (#) (Re M))) + (R_EAL (- ((Im E) (#) (Im M)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
((Re E) (#) (Re M)) - ((Im E) (#) (Im M)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
- ((Im E) (#) (Im M)) is Relation-like Function-like V57() set
((Re E) (#) (Re M)) + (- ((Im E) (#) (Im M))) is Relation-like Function-like set
R_EAL (((Re E) (#) (Re M)) - ((Im E) (#) (Im M))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Re (E (#) M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re E) (#) (Im M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Im E) (#) (Re M)) + ((Re E) (#) (Im M)) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (E (#) M) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,ExtREAL) is non empty functional set
K7(NAT,(PFuncs (X,ExtREAL))) is set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
F . 0 is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom (F . 0) is Element of K6(X)
lim F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
f is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
lim_sup F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom (lim_sup F) is Element of K6(X)
I is Element of X
f . I is ext-real Element of ExtREAL
- (f . I) is ext-real Element of ExtREAL
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(F # I) . A is ext-real Element of ExtREAL
F . A is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom (F . A) is Element of K6(X)
|.(F . A).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom |.(F . A).| is Element of K6(X)
|.(F . A).| . I is ext-real Element of ExtREAL
(F . A) . I is ext-real Element of ExtREAL
|.((F . A) . I).| is ext-real Element of ExtREAL
I is Element of X
f . I is ext-real Element of ExtREAL
- (f . I) is ext-real Element of ExtREAL
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
superior_realsequence (F # I) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(superior_realsequence (F # I)) . A is ext-real Element of ExtREAL
(F # I) . A is ext-real Element of ExtREAL
lim_sup (F # I) is ext-real Element of ExtREAL
inf (superior_realsequence (F # I)) is ext-real Element of ExtREAL
rng (superior_realsequence (F # I)) is non empty V41() V86() Element of K6(ExtREAL)
inf (rng (superior_realsequence (F # I))) is ext-real Element of ExtREAL
(lim_sup F) . I is ext-real Element of ExtREAL
A is ext-real set
rng (F # I) is non empty V41() V86() Element of K6(ExtREAL)
dom (F # I) is V40() V41() V42() V43() V44() V45() Element of K6(NAT)
I is set
(F # I) . I is ext-real Element of ExtREAL
sup (rng (F # I)) is ext-real set
(F # I) ^\ 0 is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
sup ((F # I) ^\ 0) is ext-real Element of ExtREAL
rng ((F # I) ^\ 0) is non empty V41() V86() Element of K6(ExtREAL)
sup (rng ((F # I) ^\ 0)) is ext-real Element of ExtREAL
(superior_realsequence (F # I)) . 0 is ext-real Element of ExtREAL
|.((lim_sup F) . I).| is ext-real Element of ExtREAL
I is Element of X
dom (lim F) is Element of K6(X)
F # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
(lim F) . I is ext-real Element of ExtREAL
(lim_sup F) . I is ext-real Element of ExtREAL
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 V57() V58() V59() Element of K6(K7(X,REAL))
dom (F . 0) is Element of K6(X)
lim F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom f is Element of K6(X)
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL F) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
F . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (F . I) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
I is Element of X
(R_EAL F) # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
F # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
R_EAL f is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
I is Element of X
(R_EAL f) . I is ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL F) . A is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
|.((R_EAL F) . A).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
|.((R_EAL F) . A).| . I is ext-real Element of ExtREAL
F . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.(F . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL |.(F . A).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (F . A) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
|.(R_EAL (F . A)).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 V57() V58() V59() Element of K6(K7(X,REAL))
dom (F . 0) is Element of K6(X)
lim F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim F)) is ext-real Element of ExtREAL
K439(X,(lim F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim F))) is ext-real Element of ExtREAL
K440(X,(lim F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim F))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim F)))) - (integral+ (M,K440(X,(lim F)))) is ext-real Element of ExtREAL
f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom f is Element of K6(X)
R_EAL f is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
I is Element of X
(R_EAL f) . I is ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL F) . A is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
|.((R_EAL F) . A).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
|.((R_EAL F) . A).| . I is ext-real Element of ExtREAL
F . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.(F . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL |.(F . A).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (F . A) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
|.(R_EAL (F . A)).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL F) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
F . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (F . I) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
I is set
|.(F . 0).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom |.(F . 0).| is Element of K6(X)
|.(F . 0).| . I is complex real ext-real Element of REAL
(F . 0) . I is complex real ext-real Element of REAL
|.((F . 0) . I).| is complex real ext-real Element of REAL
f . I is complex real ext-real Element of REAL
lim_inf (R_EAL F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim_inf (R_EAL F))) is ext-real Element of ExtREAL
K439(X,(lim_inf (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim_inf (R_EAL F)))) is ext-real Element of ExtREAL
K440(X,(lim_inf (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim_inf (R_EAL F)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim_inf (R_EAL F))))) - (integral+ (M,K440(X,(lim_inf (R_EAL F))))) is ext-real Element of ExtREAL
lim_sup (R_EAL F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim_sup (R_EAL F))) is ext-real Element of ExtREAL
K439(X,(lim_sup (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim_sup (R_EAL F)))) is ext-real Element of ExtREAL
K440(X,(lim_sup (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim_sup (R_EAL F)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim_sup (R_EAL F))))) - (integral+ (M,K440(X,(lim_sup (R_EAL F))))) is ext-real Element of ExtREAL
Integral (M,(lim (R_EAL F))) is ext-real Element of ExtREAL
K439(X,(lim (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim (R_EAL F)))) is ext-real Element of ExtREAL
K440(X,(lim (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim (R_EAL F)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim (R_EAL F))))) - (integral+ (M,K440(X,(lim (R_EAL F))))) is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
lim_inf I is ext-real Element of ExtREAL
inferior_realsequence I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
sup (inferior_realsequence I) is ext-real Element of ExtREAL
rng (inferior_realsequence I) is non empty V41() V86() Element of K6(ExtREAL)
sup (rng (inferior_realsequence I)) is ext-real Element of ExtREAL
lim_sup I is ext-real Element of ExtREAL
superior_realsequence I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
inf (superior_realsequence I) is ext-real Element of ExtREAL
rng (superior_realsequence I) is non empty V41() V86() Element of K6(ExtREAL)
inf (rng (superior_realsequence I)) is ext-real Element of ExtREAL
lim I is ext-real Element of ExtREAL
+infty is non empty non real ext-real positive non negative set
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
K439(X,(R_EAL f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL f))) is ext-real Element of ExtREAL
K440(X,(R_EAL f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL f)))) - (integral+ (M,K440(X,(R_EAL f)))) is ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I . A is ext-real Element of ExtREAL
|.(I . A).| is ext-real Element of ExtREAL
(R_EAL F) . A is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom ((R_EAL F) . A) is Element of K6(X)
|.((R_EAL F) . A).| is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,((R_EAL F) . A)) is ext-real Element of ExtREAL
K439(X,((R_EAL F) . A)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,((R_EAL F) . A))) is ext-real Element of ExtREAL
K440(X,((R_EAL F) . A)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,((R_EAL F) . A))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,((R_EAL F) . A)))) - (integral+ (M,K440(X,((R_EAL F) . A)))) is ext-real Element of ExtREAL
|.(Integral (M,((R_EAL F) . A))).| is ext-real Element of ExtREAL
Integral (M,|.((R_EAL F) . A).|) is ext-real Element of ExtREAL
K439(X,|.((R_EAL F) . A).|) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,|.((R_EAL F) . A).|)) is ext-real Element of ExtREAL
K440(X,|.((R_EAL F) . A).|) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,|.((R_EAL F) . A).|)) is ext-real Element of ExtREAL
(integral+ (M,K439(X,|.((R_EAL F) . A).|))) - (integral+ (M,K440(X,|.((R_EAL F) . A).|))) is ext-real Element of ExtREAL
I is Element of X
((R_EAL F) . A) . I is ext-real Element of ExtREAL
|.(((R_EAL F) . A) . I).| is ext-real Element of ExtREAL
(R_EAL f) . I is ext-real Element of ExtREAL
|.((R_EAL F) . A).| . I is ext-real Element of ExtREAL
dom |.((R_EAL F) . A).| is Element of K6(X)
dom I is V40() V41() V42() V43() V44() V45() Element of K6(NAT)
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
I . A is ext-real Element of ExtREAL
|.(I . A).| is ext-real Element of ExtREAL
I is Element of X
F # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(R_EAL F) # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
-infty is non empty non real ext-real non positive negative set
I is Element of X
(R_EAL F) # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
I is Element of X
(R_EAL F) # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
A is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim A is complex real ext-real Element of REAL
I is Element of X
F # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
A . I is complex real ext-real Element of REAL
F . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(F . I)) is ext-real Element of ExtREAL
R_EAL (F . I) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (F . I))) is ext-real Element of ExtREAL
K439(X,(R_EAL (F . I))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (F . I)))) is ext-real Element of ExtREAL
K440(X,(R_EAL (F . I))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (F . I)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (F . I))))) - (integral+ (M,K440(X,(R_EAL (F . I))))) is ext-real Element of ExtREAL
I is Element of X
F # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
X is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
+infty is non empty non real ext-real positive non negative set
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
M . E is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom (F . 0) is Element of K6(X)
lim F is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim F)) is ext-real Element of ExtREAL
K439(X,(lim F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim F))) is ext-real Element of ExtREAL
K440(X,(lim F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim F))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim F)))) - (integral+ (M,K440(X,(lim F)))) is ext-real Element of ExtREAL
f is complex real ext-real set
I is Element of X
(R_EAL F) # I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
F # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(R_EAL F) . 0 is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom ((R_EAL F) . 0) is Element of K6(X)
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL F) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
A is set
((R_EAL F) . I) . A is ext-real Element of ExtREAL
|.(((R_EAL F) . I) . A).| is ext-real Element of ExtREAL
F . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(F . I) . A is complex real ext-real Element of REAL
|.((F . I) . A).| is complex real ext-real Element of REAL
R_EAL ((F . I) . A) is ext-real Element of ExtREAL
|.(R_EAL ((F . I) . A)).| is ext-real Element of ExtREAL
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL F) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
F . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (F . I) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim (R_EAL F))) is ext-real Element of ExtREAL
K439(X,(lim (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim (R_EAL F)))) is ext-real Element of ExtREAL
K440(X,(lim (R_EAL F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim (R_EAL F)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim (R_EAL F))))) - (integral+ (M,K440(X,(lim (R_EAL F))))) is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
lim I is ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (F . A) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I . A is ext-real Element of ExtREAL
F . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(F . A)) is ext-real Element of ExtREAL
R_EAL (F . A) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (F . A))) is ext-real Element of ExtREAL
K439(X,(R_EAL (F . A))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (F . A)))) is ext-real Element of ExtREAL
K440(X,(R_EAL (F . A))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (F . A)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (F . A))))) - (integral+ (M,K440(X,(R_EAL (F . A))))) is ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
X is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,REAL) is non empty functional set
K7(NAT,(PFuncs (X,REAL))) is set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
M . E is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 V57() V58() V59() Element of K6(K7(X,REAL))
dom (F . 0) is Element of K6(X)
f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,f) is ext-real Element of ExtREAL
R_EAL f is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
K439(X,(R_EAL f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL f))) is ext-real Element of ExtREAL
K440(X,(R_EAL f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL f)))) - (integral+ (M,K440(X,(R_EAL f)))) is ext-real Element of ExtREAL
R_EAL F is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(R_EAL F) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
F . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (F . I) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
(R_EAL F) . 0 is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
dom ((R_EAL F) . 0) is Element of K6(X)
I is complex real ext-real set
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
B is set
F . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(F . I) . B is complex real ext-real Element of REAL
f . B is complex real ext-real Element of REAL
((F . I) . B) - (f . B) is complex real ext-real Element of REAL
|.(((F . I) . B) - (f . B)).| is complex real ext-real Element of REAL
R_EAL (((F . I) . B) - (f . B)) is ext-real Element of ExtREAL
|.(R_EAL (((F . I) . B) - (f . B))).| is ext-real Element of ExtREAL
(R_EAL F) . I is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
((R_EAL F) . I) . B is ext-real Element of ExtREAL
(R_EAL f) . B is ext-real Element of ExtREAL
(((R_EAL F) . I) . B) - ((R_EAL f) . B) is ext-real Element of ExtREAL
|.((((R_EAL F) . I) . B) - ((R_EAL f) . B)).| is ext-real Element of ExtREAL
dom (R_EAL f) is Element of K6(X)
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
lim I is ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I . A is ext-real Element of ExtREAL
F . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(F . A)) is ext-real Element of ExtREAL
R_EAL (F . A) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (F . A))) is ext-real Element of ExtREAL
K439(X,(R_EAL (F . A))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (F . A)))) is ext-real Element of ExtREAL
K440(X,(R_EAL (F . A))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (F . A)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (F . A))))) - (integral+ (M,K440(X,(R_EAL (F . A))))) is ext-real Element of ExtREAL
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom F is Element of K6(X)
f is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( 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 V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (f . 0) is Element of K6(X)
lim f is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
Im f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re f) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
I is Element of X
F . I is complex real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| . I is complex real ext-real Element of REAL
(Im f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . A).| . I is complex real ext-real Element of REAL
f # I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(f # I) . I is complex Element of COMPLEX
Re ((f # I) . I) is complex real ext-real Element of REAL
Re (f # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re (f # I)) . I is complex real ext-real Element of REAL
(Re (f # I)) . A is complex real ext-real Element of REAL
|.((Re (f # I)) . A).| is complex real ext-real Element of REAL
(f # I) . A is complex Element of COMPLEX
|.((f # I) . A).| is complex real ext-real Element of REAL
Im ((f # I) . I) is complex real ext-real Element of REAL
Im (f # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im (f # I)) . I is complex real ext-real Element of REAL
(Im (f # I)) . A is complex real ext-real Element of REAL
|.((Im (f # I)) . A).| is complex real ext-real Element of REAL
f . A is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
|.(f . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.(f . A).| . I is complex real ext-real Element of REAL
(f . A) . I is complex set
|.((f . A) . I).| is complex real ext-real Element of REAL
(Im f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Im f) # I) . I is complex real ext-real Element of REAL
|.(((Im f) # I) . I).| is complex real ext-real Element of REAL
(Im f) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Im f) . I) . I is complex real ext-real Element of REAL
|.(((Im f) . I) . I).| is complex real ext-real Element of REAL
(Re f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Re f) # I) . I is complex real ext-real Element of REAL
|.(((Re f) # I) . I).| is complex real ext-real Element of REAL
(Re f) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Re f) . I) . I is complex real ext-real Element of REAL
|.(((Re f) . I) . I).| is complex real ext-real Element of REAL
I is Element of X
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| . I is complex real ext-real Element of REAL
F . I is complex real ext-real Element of REAL
I is Element of X
B is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im f) . B is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . B).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . B).| . I is complex real ext-real Element of REAL
F . I is complex real ext-real Element of REAL
I is Element of X
(Re f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
f # I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re (f # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (f # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
I is Element of X
(Im f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im f) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Im f) . 0) is Element of K6(X)
lim (Im f) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (Im f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL (Im f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Im (lim f) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (Im (lim f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
I is Element of X
(Re f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re f) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re f) . 0) is Element of K6(X)
lim (Re f) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Re f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Re f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Re (lim f) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (Re (lim f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is set
K6(K6(X)) is set
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
F is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom F is Element of K6(X)
f is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( 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 V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (f . 0) is Element of K6(X)
lim f is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(lim f)) is complex set
Re f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
(Re f) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re f) . 0) is Element of K6(X)
Im f is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re f) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
I is Element of X
F . I is complex real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| . I is complex real ext-real Element of REAL
(Im f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . A).| . I is complex real ext-real Element of REAL
f # I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(f # I) . I is complex Element of COMPLEX
Re ((f # I) . I) is complex real ext-real Element of REAL
Re (f # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re (f # I)) . I is complex real ext-real Element of REAL
(Re (f # I)) . A is complex real ext-real Element of REAL
|.((Re (f # I)) . A).| is complex real ext-real Element of REAL
(f # I) . A is complex Element of COMPLEX
|.((f # I) . A).| is complex real ext-real Element of REAL
Im ((f # I) . I) is complex real ext-real Element of REAL
Im (f # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im (f # I)) . I is complex real ext-real Element of REAL
(Im (f # I)) . A is complex real ext-real Element of REAL
|.((Im (f # I)) . A).| is complex real ext-real Element of REAL
f . A is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
|.(f . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.(f . A).| . I is complex real ext-real Element of REAL
(f . A) . I is complex set
|.((f . A) . I).| is complex real ext-real Element of REAL
(Im f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Im f) # I) . I is complex real ext-real Element of REAL
|.(((Im f) # I) . I).| is complex real ext-real Element of REAL
(Re f) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Re f) # I) . A is complex real ext-real Element of REAL
|.(((Re f) # I) . A).| is complex real ext-real Element of REAL
((Re f) . A) . I is complex real ext-real Element of REAL
|.(((Re f) . A) . I).| is complex real ext-real Element of REAL
((Im f) . A) . I is complex real ext-real Element of REAL
|.(((Im f) . A) . I).| is complex real ext-real Element of REAL
I is Element of X
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re f) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . A).| . I is complex real ext-real Element of REAL
F . I is complex real ext-real Element of REAL
lim (Re f) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (Re f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL (Re f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim (Re f))) is ext-real Element of ExtREAL
K439(X,(lim (Re f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim (Re f)))) is ext-real Element of ExtREAL
K440(X,(lim (Re f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim (Re f)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim (Re f))))) - (integral+ (M,K440(X,(lim (Re f))))) is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim I is complex real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
f . A is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(f . A)) is complex set
A is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(Im f) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Im f) . 0) is Element of K6(X)
B is Element of X
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im f) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . n).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . n).| . B is complex real ext-real Element of REAL
F . B is complex real ext-real Element of REAL
lim (Im f) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Im f) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Im f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim (Im f))) is ext-real Element of ExtREAL
K439(X,(lim (Im f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim (Im f)))) is ext-real Element of ExtREAL
K440(X,(lim (Im f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim (Im f)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim (Im f))))) - (integral+ (M,K440(X,(lim (Im f))))) is ext-real Element of ExtREAL
B is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
lim B is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re f) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im f) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
n1 is Element of X
dom ((Re f) . n) is Element of K6(X)
|.((Re f) . n).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Re f) . n).| . n1 is complex real ext-real Element of REAL
F . n1 is complex real ext-real Element of REAL
((Re f) . n) . n1 is complex real ext-real Element of REAL
|.(((Re f) . n) . n1).| is complex real ext-real Element of REAL
n1 is Element of X
dom ((Im f) . n) is Element of K6(X)
|.((Im f) . n).| is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
|.((Im f) . n).| . n1 is complex real ext-real Element of REAL
F . n1 is complex real ext-real Element of REAL
((Im f) . n) . n1 is complex real ext-real Element of REAL
|.(((Im f) . n) . n1).| is complex real ext-real Element of REAL
n is set
I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re I) . n1 is complex real ext-real Element of REAL
I . n1 is complex Element of COMPLEX
Re (I . n1) is complex real ext-real Element of REAL
Im I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im I) . n1 is complex real ext-real Element of REAL
Im (I . n1) is complex real ext-real Element of REAL
(Im f) . n1 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
f . n1 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im (f . n1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re f) . n1 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (f . n1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Re (f . n1))) is ext-real Element of ExtREAL
R_EAL (Re (f . n1)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Re (f . n1)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re (f . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re (f . n1))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re (f . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re (f . n1))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re (f . n1)))))) - (integral+ (M,K440(X,(R_EAL (Re (f . n1)))))) is ext-real Element of ExtREAL
Integral (M,(Im (f . n1))) is ext-real Element of ExtREAL
R_EAL (Im (f . n1)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Im (f . n1)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im (f . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im (f . n1))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im (f . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im (f . n1))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im (f . n1)))))) - (integral+ (M,K440(X,(R_EAL (Im (f . n1)))))) is ext-real Element of ExtREAL
Integral (M,(f . n1)) is complex set
RF is complex real ext-real Element of REAL
IF is complex real ext-real Element of REAL
IF * <i> is complex set
RF + (IF * <i>) is complex set
I . n is complex set
Re (I . n) is complex real ext-real Element of REAL
Im (I . n) is complex real ext-real Element of REAL
(Re I) . n is complex real ext-real Element of REAL
I . n is complex real ext-real Element of REAL
(Im I) . n is complex real ext-real Element of REAL
B . n is complex real ext-real Element of REAL
n is set
(Re I) . n is complex real ext-real Element of REAL
I . n is complex real ext-real Element of REAL
lim I is complex Element of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I . n is complex Element of COMPLEX
f . n is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(f . n)) is complex set
n is set
(Im I) . n is complex real ext-real Element of REAL
B . n is complex real ext-real Element of REAL
Im (lim f) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Im (lim f))) is ext-real Element of ExtREAL
R_EAL (Im (lim f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Im (lim f)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im (lim f)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im (lim f))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im (lim f)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im (lim f))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im (lim f)))))) - (integral+ (M,K440(X,(R_EAL (Im (lim f)))))) is ext-real Element of ExtREAL
Re (lim f) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Re (lim f))) is ext-real Element of ExtREAL
R_EAL (Re (lim f)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Re (lim f)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re (lim f)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re (lim f))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re (lim f)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re (lim f))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re (lim f)))))) - (integral+ (M,K440(X,(R_EAL (Re (lim f)))))) is ext-real Element of ExtREAL
n is Element of X
f # n is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re (f # n) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im (f # n) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re f) # n is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im f) # n is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n is Element of X
(Re f) # n is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n1 is Element of X
(Im f) # n1 is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re I) . n is complex real ext-real Element of REAL
I . n is complex Element of COMPLEX
Re (I . n) is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Im I) . n1 is complex real ext-real Element of REAL
I . n1 is complex Element of COMPLEX
Im (I . n1) is complex real ext-real Element of REAL
lim (Re I) is complex real ext-real Element of REAL
lim (Im I) is complex real ext-real Element of REAL
(lim (Im I)) * <i> is complex set
(lim (Re I)) + ((lim (Im I)) * <i>) is complex set
n is Element of X
(Re f) # n is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n1 is Element of X
(Im f) # n1 is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n is Element of X
(Re f) # n is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n1 is Element of X
(Im f) # n1 is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
X is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
M . E is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( 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 V57() Element of K6(K7(X,COMPLEX))
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
dom (F . 0) is Element of K6(X)
lim F is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(lim F)) is complex set
f is complex real ext-real set
Re F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
I is Element of X
(Re F) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
F # I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re (F # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
Im F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Im F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Im F) . 0) is Element of K6(X)
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
A is Element of X
((Im F) . I) . A is complex real ext-real Element of REAL
|.(((Im F) . I) . A).| is complex real ext-real Element of REAL
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(F . I) . A is complex set
|.((F . I) . A).| is complex real ext-real Element of REAL
F # A is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(F # A) . I is complex Element of COMPLEX
|.((F # A) . I).| is complex real ext-real Element of REAL
Im ((F # A) . I) is complex real ext-real Element of REAL
Im (F # A) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im (F # A)) . I is complex real ext-real Element of REAL
(Im F) # A is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Im F) # A) . I is complex real ext-real Element of REAL
|.(((Im F) # A) . I).| is complex real ext-real Element of REAL
I is Element of X
(Im F) # I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
F # I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Im (F # I) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(F . I)) is complex set
I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
B is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im F) . B is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re F) . 0) is Element of K6(X)
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
B is Element of X
((Re F) . I) . B is complex real ext-real Element of REAL
|.(((Re F) . I) . B).| is complex real ext-real Element of REAL
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(F . I) . B is complex set
|.((F . I) . B).| is complex real ext-real Element of REAL
F # B is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(F # B) . I is complex Element of COMPLEX
|.((F # B) . I).| is complex real ext-real Element of REAL
Re ((F # B) . I) is complex real ext-real Element of REAL
Re (F # B) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re (F # B)) . I is complex real ext-real Element of REAL
(Re F) # B is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Re F) # B) . I is complex real ext-real Element of REAL
|.(((Re F) # B) . I).| is complex real ext-real Element of REAL
lim (Im F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
R_EAL (Im F) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,ExtREAL)))) is set
lim (R_EAL (Im F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim (Im F))) is ext-real Element of ExtREAL
K439(X,(lim (Im F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim (Im F)))) is ext-real Element of ExtREAL
K440(X,(lim (Im F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim (Im F)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim (Im F))))) - (integral+ (M,K440(X,(lim (Im F))))) is ext-real Element of ExtREAL
I is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
lim I is ext-real Element of ExtREAL
Im (lim F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (Im (lim F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
lim (Re F) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
R_EAL (Re F) is non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total V51( NAT , PFuncs (X,ExtREAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,ExtREAL))))
lim (R_EAL (Re F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(lim (Re F))) is ext-real Element of ExtREAL
K439(X,(lim (Re F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(lim (Re F)))) is ext-real Element of ExtREAL
K440(X,(lim (Re F))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(lim (Re F)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(lim (Re F))))) - (integral+ (M,K440(X,(lim (Re F))))) is ext-real Element of ExtREAL
B is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
lim B is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
F . n is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(Im F) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (F . n) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re F) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (F . n) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
A is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re A is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
R_EAL (Re A) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
Im A is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
R_EAL (Im A) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
n is set
(R_EAL (Re A)) . n is ext-real Element of ExtREAL
B . n is ext-real Element of ExtREAL
(R_EAL (Im A)) . n is ext-real Element of ExtREAL
I . n is ext-real Element of ExtREAL
A . n is complex set
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
F . n1 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(F . n1)) is complex set
Re (F . n1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Re (F . n1))) is ext-real Element of ExtREAL
R_EAL (Re (F . n1)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Re (F . n1)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re (F . n1))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re (F . n1))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re (F . n1)))))) - (integral+ (M,K440(X,(R_EAL (Re (F . n1)))))) is ext-real Element of ExtREAL
Im (F . n1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Im (F . n1))) is ext-real Element of ExtREAL
R_EAL (Im (F . n1)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Im (F . n1)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im (F . n1))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im (F . n1))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im (F . n1)))))) - (integral+ (M,K440(X,(R_EAL (Im (F . n1)))))) is ext-real Element of ExtREAL
RF is complex real ext-real Element of REAL
IF is complex real ext-real Element of REAL
IF * <i> is complex set
RF + (IF * <i>) is complex set
(Re A) . n1 is complex real ext-real Element of REAL
A . n1 is complex Element of COMPLEX
Re (A . n1) is complex real ext-real Element of REAL
(Re F) . n1 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Re A) . n is complex real ext-real Element of REAL
(Im A) . n1 is complex real ext-real Element of REAL
Im (A . n1) is complex real ext-real Element of REAL
(Im F) . n1 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im A) . n is complex real ext-real Element of REAL
n is set
(R_EAL (Im A)) . n is ext-real Element of ExtREAL
I . n is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative set
lim (Im A) is complex real ext-real Element of REAL
Re (lim F) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
R_EAL (Re (lim F)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
lim A is complex Element of COMPLEX
n is set
(R_EAL (Re A)) . n is ext-real Element of ExtREAL
B . n is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
A . n is complex Element of COMPLEX
F . n is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(F . n)) is complex set
(Re A) . n is complex real ext-real Element of REAL
Re (A . n) is complex real ext-real Element of REAL
(Im A) . n is complex real ext-real Element of REAL
Im (A . n) is complex real ext-real Element of REAL
(Re F) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (F . n) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Re (F . n))) is ext-real Element of ExtREAL
R_EAL (Re (F . n)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Re (F . n)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re (F . n))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re (F . n))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re (F . n)))))) - (integral+ (M,K440(X,(R_EAL (Re (F . n)))))) is ext-real Element of ExtREAL
(Im F) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (F . n) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Im (F . n))) is ext-real Element of ExtREAL
R_EAL (Im (F . n)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Im (F . n)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im (F . n))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im (F . n))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im (F . n)))))) - (integral+ (M,K440(X,(R_EAL (Im (F . n)))))) is ext-real Element of ExtREAL
(Im (A . n)) * <i> is complex set
(Re (A . n)) + ((Im (A . n)) * <i>) is complex set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re A) . n is complex real ext-real Element of REAL
A . n is complex Element of COMPLEX
Re (A . n) is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Im A) . n1 is complex real ext-real Element of REAL
A . n1 is complex Element of COMPLEX
Im (A . n1) is complex real ext-real Element of REAL
lim (Re A) is complex real ext-real Element of REAL
(lim (Im A)) * <i> is complex set
(lim (Re A)) + ((lim (Im A)) * <i>) is complex set
Integral (M,(Re (lim F))) is ext-real Element of ExtREAL
Integral (M,(R_EAL (Re (lim F)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re (lim F)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re (lim F))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re (lim F)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re (lim F))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re (lim F)))))) - (integral+ (M,K440(X,(R_EAL (Re (lim F)))))) is ext-real Element of ExtREAL
Integral (M,(Im (lim F))) is ext-real Element of ExtREAL
Integral (M,(R_EAL (Im (lim F)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im (lim F)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im (lim F))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im (lim F)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im (lim F))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im (lim F)))))) - (integral+ (M,K440(X,(R_EAL (Im (lim F)))))) is ext-real Element of ExtREAL
X is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
X is non empty set
K6(X) is set
K6(K6(X)) is set
PFuncs (X,COMPLEX) is non empty functional set
K7(NAT,(PFuncs (X,COMPLEX))) is set
K6(K7(NAT,(PFuncs (X,COMPLEX)))) is set
K7(X,COMPLEX) is V57() set
K6(K7(X,COMPLEX)) is set
S is non empty compl-closed sigma-multiplicative Element of K6(K6(X))
K7(S,ExtREAL) is V58() set
K6(K7(S,ExtREAL)) is set
M is non empty Relation-like S -defined ExtREAL -valued Function-like total V51(S, ExtREAL ) V58() V66() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
E is Element of S
M . E is ext-real Element of ExtREAL
F is non empty Relation-like NAT -defined PFuncs (X,COMPLEX) -valued Function-like total V51( 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 V57() Element of K6(K7(X,COMPLEX))
dom (F . 0) is Element of K6(X)
f is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,f) is complex set
Im F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( 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 set
K6(K7(NAT,(PFuncs (X,REAL)))) is set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Im (F . I) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom f is Element of K6(X)
(Im F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
K7(X,REAL) is V57() V58() V59() set
K6(K7(X,REAL)) is set
dom ((Im F) . 0) is Element of K6(X)
Im f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
I is complex real ext-real set
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Im F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
B is Element of X
((Im F) . I) . B is complex real ext-real Element of REAL
(Im f) . B is complex real ext-real Element of REAL
(((Im F) . I) . B) - ((Im f) . B) is complex real ext-real Element of REAL
|.((((Im F) . I) . B) - ((Im f) . B)).| is complex real ext-real Element of REAL
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(F . I) . B is complex set
f . B is complex set
((F . I) . B) - (f . B) is complex set
|.(((F . I) . B) - (f . B)).| is complex real ext-real Element of REAL
F # B is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(F # B) . I is complex Element of COMPLEX
((F # B) . I) - (f . B) is complex set
|.(((F # B) . I) - (f . B)).| is complex real ext-real Element of REAL
Im (((F # B) . I) - (f . B)) is complex real ext-real Element of REAL
Im ((F # B) . I) is complex real ext-real Element of REAL
Im (f . B) is complex real ext-real Element of REAL
(Im ((F # B) . I)) - (Im (f . B)) is complex real ext-real Element of REAL
|.((Im ((F # B) . I)) - (Im (f . B))).| is complex real ext-real Element of REAL
dom (Im f) is Element of K6(X)
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(F # B) . n is complex Element of COMPLEX
Im ((F # B) . n) is complex real ext-real Element of REAL
Im (F # B) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im (F # B)) . I is complex real ext-real Element of REAL
(Im F) # B is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Im F) # B) . n is complex real ext-real Element of REAL
dom (Im f) is Element of K6(X)
Re F is non empty Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like total V51( NAT , PFuncs (X,REAL)) with_the_same_dom Element of K6(K7(NAT,(PFuncs (X,REAL))))
(Re F) . 0 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
dom ((Re F) . 0) is Element of K6(X)
Re f is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
I is complex real ext-real set
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re F) . I is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
B is Element of X
((Re F) . I) . B is complex real ext-real Element of REAL
(Re f) . B is complex real ext-real Element of REAL
(((Re F) . I) . B) - ((Re f) . B) is complex real ext-real Element of REAL
|.((((Re F) . I) . B) - ((Re f) . B)).| is complex real ext-real Element of REAL
F # B is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
(F # B) . I is complex Element of COMPLEX
f . B is complex set
((F # B) . I) - (f . B) is complex set
Re (((F # B) . I) - (f . B)) is complex real ext-real Element of REAL
Re ((F # B) . I) is complex real ext-real Element of REAL
Re (f . B) is complex real ext-real Element of REAL
(Re ((F # B) . I)) - (Re (f . B)) is complex real ext-real Element of REAL
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
(F . I) . B is complex set
|.(((F # B) . I) - (f . B)).| is complex real ext-real Element of REAL
dom (Re f) is Element of K6(X)
|.((Re ((F # B) . I)) - (Re (f . B))).| is complex real ext-real Element of REAL
Re (F # B) is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re (F # B)) . n is complex real ext-real Element of REAL
(Re F) # B is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
((Re F) # B) . I is complex real ext-real Element of REAL
(Re F) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
((Re F) . n) . B is complex real ext-real Element of REAL
dom (Re f) is Element of K6(X)
I is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
F . I is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(F . I)) is complex set
I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
A is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
(Re F) . A is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F . A is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re (F . A) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Re f)) is ext-real Element of ExtREAL
R_EAL (Re f) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is V58() set
K6(K7(X,ExtREAL)) is set
Integral (M,(R_EAL (Re f))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re f)))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re f)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re f))))) - (integral+ (M,K440(X,(R_EAL (Re f))))) is ext-real Element of ExtREAL
A is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
lim A is ext-real Element of ExtREAL
Integral (M,(Im f)) is ext-real Element of ExtREAL
R_EAL (Im f) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Im f))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im f)))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im f))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im f)))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im f))))) - (integral+ (M,K440(X,(R_EAL (Im f))))) is ext-real Element of ExtREAL
B is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
lim B is ext-real Element of ExtREAL
n is set
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re F) . n1 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
F . n1 is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Re (F . n1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
(Im F) . n1 is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (F . n1) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Re (F . n1))) is ext-real Element of ExtREAL
R_EAL (Re (F . n1)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Re (F . n1)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re (F . n1))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re (F . n1))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re (F . n1)))))) - (integral+ (M,K440(X,(R_EAL (Re (F . n1)))))) is ext-real Element of ExtREAL
Integral (M,(Im (F . n1))) is ext-real Element of ExtREAL
R_EAL (Im (F . n1)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Im (F . n1)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im (F . n1))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im (F . n1)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im (F . n1))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im (F . n1)))))) - (integral+ (M,K440(X,(R_EAL (Im (F . n1)))))) is ext-real Element of ExtREAL
Integral (M,(F . n1)) is complex set
RF is complex real ext-real Element of REAL
IF is complex real ext-real Element of REAL
IF * <i> is complex set
RF + (IF * <i>) is complex set
I is non empty Relation-like NAT -defined COMPLEX -valued Function-like total V51( NAT , COMPLEX ) V57() Element of K6(K7(NAT,COMPLEX))
Re I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Re I) . n1 is complex real ext-real Element of REAL
I . n1 is complex Element of COMPLEX
Re (I . n1) is complex real ext-real Element of REAL
Im I is non empty Relation-like NAT -defined REAL -valued Function-like total V51( NAT , REAL ) V57() V58() V59() Element of K6(K7(NAT,REAL))
(Im I) . n1 is complex real ext-real Element of REAL
Im (I . n1) is complex real ext-real Element of REAL
I . n is complex set
Re (I . n) is complex real ext-real Element of REAL
Im (I . n) is complex real ext-real Element of REAL
R_EAL (Re I) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
(R_EAL (Re I)) . n is ext-real Element of ExtREAL
A . n is ext-real Element of ExtREAL
R_EAL (Im I) is non empty Relation-like NAT -defined ExtREAL -valued Function-like total V51( NAT , ExtREAL ) V58() Element of K6(K7(NAT,ExtREAL))
(R_EAL (Im I)) . n is ext-real Element of ExtREAL
B . n is ext-real Element of ExtREAL
n is set
(R_EAL (Im I)) . n is ext-real Element of ExtREAL
B . n is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative set
lim (Im I) is complex real ext-real Element of REAL
lim I is complex Element of COMPLEX
n is set
(R_EAL (Re I)) . n is ext-real Element of ExtREAL
A . n is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
I . n is complex Element of COMPLEX
F . n is Relation-like X -defined COMPLEX -valued Function-like V57() Element of K6(K7(X,COMPLEX))
Integral (M,(F . n)) is complex set
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re I) . n1 is complex real ext-real Element of REAL
I . n1 is complex Element of COMPLEX
Re (I . n1) is complex real ext-real Element of REAL
(Im I) . n1 is complex real ext-real Element of REAL
Im (I . n1) is complex real ext-real Element of REAL
(Re I) . n is complex real ext-real Element of REAL
(Im I) . n is complex real ext-real Element of REAL
((Im I) . n) * <i> is complex set
((Re I) . n) + (((Im I) . n) * <i>) is complex set
(Re F) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Re (F . n) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Re (F . n))) is ext-real Element of ExtREAL
R_EAL (Re (F . n)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Re (F . n)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Re (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Re (F . n))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Re (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Re (F . n))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Re (F . n)))))) - (integral+ (M,K440(X,(R_EAL (Re (F . n)))))) is ext-real Element of ExtREAL
(Im F) . n is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Im (F . n) is Relation-like X -defined REAL -valued Function-like V57() V58() V59() Element of K6(K7(X,REAL))
Integral (M,(Im (F . n))) is ext-real Element of ExtREAL
R_EAL (Im (F . n)) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
Integral (M,(R_EAL (Im (F . n)))) is ext-real Element of ExtREAL
K439(X,(R_EAL (Im (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K439(X,(R_EAL (Im (F . n))))) is ext-real Element of ExtREAL
K440(X,(R_EAL (Im (F . n)))) is Relation-like X -defined ExtREAL -valued Function-like V58() Element of K6(K7(X,ExtREAL))
integral+ (M,K440(X,(R_EAL (Im (F . n))))) is ext-real Element of ExtREAL
(integral+ (M,K439(X,(R_EAL (Im (F . n)))))) - (integral+ (M,K440(X,(R_EAL (Im (F . n)))))) is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Re I) . n is complex real ext-real Element of REAL
I . n is complex Element of COMPLEX
Re (I . n) is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V40() V41() V42() V43() V44() V45() V72() V74() Element of NAT
(Im I) . n1 is complex real ext-real Element of REAL
I . n1 is complex Element of COMPLEX
Im (I . n1) is complex real ext-real Element of REAL
lim (Re I) is complex real ext-real Element of REAL
(lim (Im I)) * <i> is complex set
(lim (Re I)) + ((lim (Im I)) * <i>) is complex set