:: 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