REAL is non empty V12() complex-membered ext-real-membered real-membered V51() non finite V66() V67() V69() set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() non finite cardinal limit_cardinal V64() V66() Element of K19(REAL)
K19(REAL) is V12() non finite set
COMPLEX is non empty V12() complex-membered V51() non finite set
omega is non empty V12() epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() non finite cardinal limit_cardinal V64() V66() set
K19(omega) is V12() non finite set
K19(NAT) is V12() non finite set
RAT is non empty V12() complex-membered ext-real-membered real-membered rational-membered V51() non finite set
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() finite finite-yielding V57() cardinal {} -element V66() V67() V68() V69() Function-yielding V71() set
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() finite finite-yielding V57() cardinal {} -element V66() V67() V68() V69() Function-yielding V71() set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() finite finite-yielding V57() cardinal {} -element V66() V67() V68() V69() Function-yielding V71() set
INT is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered V51() non finite set
1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite cardinal V64() V65() V66() V67() V68() Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() finite finite-yielding V57() cardinal {} -element V66() V67() V68() V69() Function-yielding V71() Element of NAT
|.0.| is real complex ext-real Element of REAL
f is Relation-like Function-like FinSequence-like set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
i is Relation-like Function-like set
dom i is set
len f is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite cardinal V66() V67() V68() Element of NAT
Seg (len f) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite cardinal V66() V67() V68() Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
f is Relation-like Function-like FinSequence-like set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
i is Relation-like Function-like FinSequence-like set
dom i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
(dom f) /\ (dom i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
n is Relation-like Function-like set
dom n is set
y is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
Seg y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite cardinal V66() V67() V68() Element of NAT : ( 1 <= b1 & b1 <= y ) } is set
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
Seg m is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite cardinal V66() V67() V68() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
<*> COMPLEX is Relation-like NAT -defined COMPLEX -valued Function-like complex-valued FinSequence-like FinSequence of COMPLEX
f is real rational complex ext-real set
|.f.| is real complex ext-real Element of REAL
- f is real rational complex ext-real set
f is Relation-like Function-like complex-valued set
i is Relation-like Function-like complex-valued set
dom f is set
dom i is set
(dom f) /\ (dom i) is set
y is Relation-like Function-like set
dom y is set
y is Relation-like Function-like set
dom y is set
m is Relation-like Function-like set
dom m is set
m is set
y . m is set
f . m is complex set
i . m is complex set
(f . m) + (i . m) is set
m . m is set
y is Relation-like Function-like set
dom y is set
m is Relation-like Function-like complex-valued set
dom m is set
m is Relation-like Function-like complex-valued set
dom m is set
(dom m) /\ (dom m) is set
(dom m) /\ (dom m) is set
i2 is set
y . i2 is set
m . i2 is complex set
m . i2 is complex set
(m . i2) + (m . i2) is set
f is Relation-like Function-like complex-valued set
i is Relation-like Function-like complex-valued set
(f,i) is Relation-like Function-like set
n is set
dom (f,i) is set
(f,i) . n is set
f . n is complex set
i . n is complex set
(f . n) + (i . n) is set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-valued set
n is set
dom (f,i) is set
(f,i) . n is complex set
f . n is real complex ext-real set
i . n is real complex ext-real set
(f . n) + (i . n) is real complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
i is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real rational complex ext-real set
i . y is real rational complex ext-real set
(f . y) + (i . y) is real rational complex ext-real set
f is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
i is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real integer rational complex ext-real set
i . y is real integer rational complex ext-real set
(f . y) + (i . y) is real integer rational complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
i is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
(f,i) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set
f . n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f . n) + (i . n) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is set
i is complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is complex-membered set
K20(f,n) is Relation-like complex-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (y,m) is set
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (y,m) is complex-membered set
f is set
i is complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered set
K20(f,n) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
(f,i,n,y,m) is Relation-like f -defined COMPLEX -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered Element of K19(COMPLEX)
K19(COMPLEX) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered rational-membered set
K20(f,n) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
(f,i,n,y,m) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered Element of K19(REAL)
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
(f,i,n,y,m) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered rational-membered Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,n))
(y,m) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
(f,i,n,y,m) is Relation-like f -defined RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,INT))
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is non empty complex-membered set
K20(f,n) is Relation-like complex-valued set
K19(K20(f,n)) is set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
f is set
i is non empty complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered set
K20(f,n) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered rational-membered set
K20(f,n) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,n)) is set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
f is set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is non empty complex-membered set
K20(f,n) is Relation-like complex-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined COMPLEX -valued Function-like total V29(f, COMPLEX ) complex-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
m is Element of f
(f,i,n,y,m) . m is complex set
y . m is complex set
m . m is complex set
(y . m) + (m . m) is set
dom y is Element of K19(f)
f is Relation-like Function-like complex-valued FinSequence-like set
i is Relation-like Function-like complex-valued FinSequence-like set
(f,i) is Relation-like Function-like complex-valued set
dom (f,i) is set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
dom i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
(dom f) /\ (dom i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
i is complex set
f is Relation-like Function-like complex-valued set
dom f is set
n is Relation-like Function-like set
dom n is set
n is Relation-like Function-like set
dom n is set
y is Relation-like Function-like set
dom y is set
m is set
n . m is set
f . m is complex set
i + (f . m) is set
y . m is set
f is Relation-like Function-like complex-valued set
i is complex set
(f,i) is Relation-like Function-like set
n is set
dom (f,i) is set
(f,i) . n is set
f . n is complex set
i + (f . n) is set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is real complex ext-real set
(f,i) is Relation-like Function-like complex-valued set
n is set
dom (f,i) is set
(f,i) . n is complex set
f . n is real complex ext-real set
i + (f . n) is real complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
i is real rational complex ext-real set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real rational complex ext-real set
i + (f . y) is real rational complex ext-real set
f is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
i is real integer rational complex ext-real set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real integer rational complex ext-real set
i + (f . y) is real integer rational complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,i) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set
f . n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i + (f . n) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is set
i is complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued Element of K19(K20(f,i))
y is complex set
(n,y) is Relation-like Function-like complex-valued set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (n,y) is set
dom n is Element of K19(f)
K19(f) is set
rng (n,y) is complex-membered set
f is set
i is complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered Element of K19(COMPLEX)
K19(COMPLEX) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real rational complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
(f,i,n,y) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered Element of K19(REAL)
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real integer rational complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
(f,i,n,y) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered rational-membered Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
y is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(n,y) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
(f,i,n,y) is Relation-like f -defined RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,INT))
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued Element of K19(K20(f,i))
y is complex set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
f is set
i is non empty complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real complex ext-real set
(f,i,n,y) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real rational complex ext-real set
(f,i,n,y) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real integer rational complex ext-real set
(f,i,n,y) is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
y is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,i,n,y) is Relation-like f -defined NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
f is non empty set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like non empty total V29(f,i) complex-valued Element of K19(K20(f,i))
y is complex set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like non empty total V29(f, COMPLEX ) complex-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like V12() complex-valued non finite set
K19(K20(f,COMPLEX)) is V12() non finite set
dom (f,i,n,y) is non empty Element of K19(f)
K19(f) is set
m is Element of f
(f,i,n,y) . m is complex Element of COMPLEX
n . m is complex Element of i
y + (n . m) is set
f is Relation-like Function-like complex-valued FinSequence-like set
i is complex set
(f,i) is Relation-like Function-like complex-valued set
dom (f,i) is set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
f is Relation-like Function-like complex-valued set
i is complex set
- i is complex set
(f,(- i)) is Relation-like Function-like complex-valued set
f is Relation-like Function-like complex-valued set
dom f is set
i is complex set
(f,i) is Relation-like Function-like set
- i is complex set
(f,(- i)) is Relation-like Function-like complex-valued set
dom (f,i) is set
n is set
(f,i) . n is set
f . n is complex set
(f . n) - i is set
(f . n) + (- i) is set
f is Relation-like Function-like complex-valued set
i is complex set
(f,i) is Relation-like Function-like set
- i is complex set
(f,(- i)) is Relation-like Function-like complex-valued set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is real complex ext-real set
(f,i) is Relation-like Function-like complex-valued set
- i is real complex ext-real set
(f,(- i)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
i is real rational complex ext-real set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
- i is real rational complex ext-real set
(f,(- i)) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
f is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
i is real integer rational complex ext-real set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
- i is real integer rational complex ext-real set
(f,(- i)) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
f is set
i is complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued Element of K19(K20(f,i))
y is complex set
(n,y) is Relation-like Function-like complex-valued set
- y is complex set
(n,(- y)) is Relation-like Function-like complex-valued set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (n,y) is set
dom n is Element of K19(f)
K19(f) is set
rng (n,y) is complex-membered set
f is set
i is complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
- y is real complex ext-real set
(n,(- y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered Element of K19(COMPLEX)
K19(COMPLEX) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real rational complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
- y is real rational complex ext-real set
(n,(- y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
(f,i,n,y) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered Element of K19(REAL)
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real integer rational complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
- y is real integer rational complex ext-real set
(n,(- y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
(f,i,n,y) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered rational-membered Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued Element of K19(K20(f,i))
y is complex set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
- y is complex set
(n,(- y)) is Relation-like Function-like complex-valued set
m is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
f is set
i is non empty complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real complex ext-real set
(f,i,n,y) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
- y is real complex ext-real set
(n,(- y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
m is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real rational complex ext-real set
(f,i,n,y) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
- y is real rational complex ext-real set
(n,(- y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
m is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real integer rational complex ext-real set
(f,i,n,y) is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
- y is real integer rational complex ext-real set
(n,(- y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
m is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
f is non empty set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like non empty total V29(f,i) complex-valued Element of K19(K20(f,i))
y is complex set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like non empty total V29(f, COMPLEX ) complex-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like V12() complex-valued non finite set
K19(K20(f,COMPLEX)) is V12() non finite set
- y is complex set
(n,(- y)) is Relation-like Function-like complex-valued set
dom (f,i,n,y) is non empty Element of K19(f)
K19(f) is set
m is Element of f
(f,i,n,y) . m is complex Element of COMPLEX
n . m is complex Element of i
(n . m) - y is set
(n . m) + (- y) is set
f is Relation-like Function-like complex-valued FinSequence-like set
i is complex set
(f,i) is Relation-like Function-like complex-valued set
- i is complex set
(f,(- i)) is Relation-like Function-like complex-valued FinSequence-like set
f is Relation-like Function-like complex-valued set
i is Relation-like Function-like complex-valued set
dom f is set
dom i is set
(dom f) /\ (dom i) is set
y is Relation-like Function-like set
dom y is set
y is Relation-like Function-like set
dom y is set
m is Relation-like Function-like set
dom m is set
m is set
y . m is set
f . m is complex set
i . m is complex set
(f . m) * (i . m) is set
m . m is set
y is Relation-like Function-like set
dom y is set
m is Relation-like Function-like complex-valued set
dom m is set
m is Relation-like Function-like complex-valued set
dom m is set
(dom m) /\ (dom m) is set
(dom m) /\ (dom m) is set
i2 is set
y . i2 is set
m . i2 is complex set
m . i2 is complex set
(m . i2) * (m . i2) is set
f is Relation-like Function-like complex-valued set
i is Relation-like Function-like complex-valued set
(f,i) is Relation-like Function-like set
n is set
(f,i) . n is set
f . n is complex set
i . n is complex set
(f . n) * (i . n) is set
dom (f,i) is set
dom f is set
dom i is set
(dom f) /\ (dom i) is set
f is Relation-like Function-like complex-valued set
i is Relation-like Function-like complex-valued set
(f,i) is Relation-like Function-like set
n is set
dom (f,i) is set
(f,i) . n is set
f . n is complex set
i . n is complex set
(f . n) * (i . n) is set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-valued set
n is set
dom (f,i) is set
(f,i) . n is complex set
f . n is real complex ext-real set
i . n is real complex ext-real set
(f . n) * (i . n) is real complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
i is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real rational complex ext-real set
i . y is real rational complex ext-real set
(f . y) * (i . y) is real rational complex ext-real set
f is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
i is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real integer rational complex ext-real set
i . y is real integer rational complex ext-real set
(f . y) * (i . y) is real integer rational complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
i is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
(f,i) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set
f . n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f . n) * (i . n) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is set
i is complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is complex-membered set
K20(f,n) is Relation-like complex-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (y,m) is set
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (y,m) is complex-membered set
f is set
i is complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered set
K20(f,n) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
(f,i,n,y,m) is Relation-like f -defined COMPLEX -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered Element of K19(COMPLEX)
K19(COMPLEX) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered rational-membered set
K20(f,n) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
(f,i,n,y,m) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered Element of K19(REAL)
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(y,m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
(f,i,n,y,m) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered rational-membered Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
n is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,n)) is set
y is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,n))
(y,m) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
(f,i,n,y,m) is Relation-like f -defined RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,INT))
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
dom m is Element of K19(f)
(dom y) /\ (dom m) is Element of K19(f)
rng (f,i,n,y,m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is non empty complex-membered set
K20(f,n) is Relation-like complex-valued set
K19(K20(f,n)) is set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
f is set
i is non empty complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered set
K20(f,n) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered rational-membered set
K20(f,n) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,n)) is set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
n is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() set
K20(f,n) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,n)) is set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
y is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
m is Relation-like f -defined n -valued Function-like total V29(f,n) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,n))
(f,i,n,y,m) is Relation-like f -defined NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
dom y is Element of K19(f)
K19(f) is set
dom m is Element of K19(f)
dom (f,i,n,y,m) is Element of K19(f)
f /\ f is set
m is Relation-like f -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
f is Relation-like Function-like complex-valued FinSequence-like set
i is Relation-like Function-like complex-valued FinSequence-like set
(f,i) is Relation-like Function-like complex-valued set
dom (f,i) is set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
dom i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
(dom f) /\ (dom i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
i is complex set
f is Relation-like Function-like complex-valued set
dom f is set
n is Relation-like Function-like set
dom n is set
n is Relation-like Function-like set
dom n is set
y is Relation-like Function-like set
dom y is set
m is set
n . m is set
f . m is complex set
i * (f . m) is set
y . m is set
f is Relation-like Function-like complex-valued set
i is complex set
(f,i) is Relation-like Function-like set
n is set
(f,i) . n is set
f . n is complex set
i * (f . n) is set
dom f is set
dom (f,i) is set
i * 0 is set
f is Relation-like Function-like complex-valued set
i is complex set
(f,i) is Relation-like Function-like set
n is set
dom (f,i) is set
(f,i) . n is set
f . n is complex set
i * (f . n) is set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is real complex ext-real set
(f,i) is Relation-like Function-like complex-valued set
n is set
dom (f,i) is set
(f,i) . n is complex set
f . n is real complex ext-real set
i * (f . n) is real complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
i is real rational complex ext-real set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real rational complex ext-real set
i * (f . y) is real rational complex ext-real set
f is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
i is real integer rational complex ext-real set
(f,i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is set
rng (f,i) is complex-membered ext-real-membered real-membered set
dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set
f . y is real integer rational complex ext-real set
i * (f . y) is real integer rational complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,i) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set
f . n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i * (f . n) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is set
i is complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued Element of K19(K20(f,i))
y is complex set
(n,y) is Relation-like Function-like complex-valued set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (n,y) is set
dom n is Element of K19(f)
K19(f) is set
rng (n,y) is complex-membered set
f is set
i is complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered Element of K19(COMPLEX)
K19(COMPLEX) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real rational complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
(f,i,n,y) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered Element of K19(REAL)
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real integer rational complex ext-real set
(n,y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
(f,i,n,y) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered rational-membered Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
n is Relation-like f -defined i -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
y is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(n,y) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
(f,i,n,y) is Relation-like f -defined RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,INT))
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n,y) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(RAT)
K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set
K20(f,i) is Relation-like complex-valued set
K19(K20(f,i)) is set
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued Element of K19(K20(f,i))
y is complex set
(f,i,n,y) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
f is set
i is non empty complex-membered ext-real-membered real-membered set
K20(f,i) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real complex ext-real set
(f,i,n,y) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered set
K20(f,i) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,RAT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real rational complex ext-real set
(f,i,n,y) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,i)) is set
K20(f,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(f,INT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued Element of K19(K20(f,i))
y is real integer rational complex ext-real set
(f,i,n,y) is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
f is set
i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() set
K20(f,i) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,i)) is set
K20(f,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(f,NAT)) is set
n is Relation-like f -defined i -valued Function-like total V29(f,i) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,i))
y is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,i,n,y) is Relation-like f -defined NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
m is Relation-like f -defined NAT -valued Function-like complex-valued ext-real-valued