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 real-valued natural-valued Element of K19(K20(f,NAT))
f is non empty set
K20(f,COMPLEX) is Relation-like V12() complex-valued non finite set
K19(K20(f,COMPLEX)) is V12() non finite 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))
m is Relation-like f -defined COMPLEX -valued Function-like non empty total V29(f, COMPLEX ) complex-valued Element of K19(K20(f,COMPLEX))
m is Element of f
m . m is complex set
(f,i,n,y) . m is complex set
m . m is complex Element of COMPLEX
n . m is complex Element of i
y * (n . m) is set
(f,i,n,y) . m is complex Element of COMPLEX
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
- 1 is real integer rational complex ext-real non positive set
(f,(- 1)) is Relation-like Function-like complex-valued set
i is Relation-like Function-like complex-valued set
n is Relation-like Function-like complex-valued set
(n,(- 1)) is Relation-like Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued set
dom (i,(- 1)) is set
dom i is set
dom n is set
y is set
n . y is complex set
(i,(- 1)) . y is complex set
(- 1) * (n . y) is set
m is complex set
(- 1) * m is set
i . y is complex set
(- 1) * (i . y) is set
f is Relation-like Function-like complex-valued set
(f) is Relation-like Function-like complex-valued set
(f,(- 1)) is Relation-like Function-like complex-valued set
dom (f) is set
dom f is set
i is set
(f) . i is complex set
f . i is complex set
- (f . i) is complex set
(- 1) * (f . i) is set
- 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() set
f is Relation-like Function-like complex-valued set
dom f is set
(f) is Relation-like Function-like complex-valued set
(f,(- 1)) is Relation-like Function-like complex-valued set
i is Relation-like Function-like set
dom i is set
dom (f) is set
n is set
i . n is set
(f) . n is complex set
f . n is complex set
- (f . n) is complex set
f is Relation-like Function-like complex-valued set
(f) is Relation-like Function-like complex-valued set
(f,(- 1)) is Relation-like Function-like complex-valued set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f) is Relation-like Function-like complex-valued set
(f,(- 1)) 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
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,(- 1)) 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
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,(- 1)) 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))
(n) is Relation-like Function-like complex-valued set
(n,(- 1)) 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) is set
dom n is Element of K19(f)
K19(f) is set
rng (n) 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,(- 1)) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,(- 1)) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,(- 1)) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(f,i,n) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
(n,(- 1)) is Relation-like Function-like complex-valued set
y 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))
(f,i,n) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
(n,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
y 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))
(f,i,n) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
(n,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
y 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))
(f,i,n) is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
(n,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
y is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
f is Relation-like Function-like complex-valued FinSequence-like set
(f) is Relation-like Function-like complex-valued set
(f,(- 1)) is Relation-like Function-like complex-valued FinSequence-like set
f is Relation-like Function-like complex-valued set
dom f is set
i is Relation-like Function-like set
dom i is set
n is set
i . n is set
f . n is complex set
(f . n) " is complex set
i is Relation-like Function-like complex-valued set
dom i is set
n is Relation-like Function-like complex-valued set
dom n is set
y is set
i . y is complex set
f . y is complex set
(f . y) " is complex set
n . y is complex set
i is Relation-like Function-like complex-valued set
dom i is set
n is Relation-like Function-like complex-valued set
dom n is set
y is set
n . y is complex set
i . y is complex set
(i . y) " is complex set
(n . y) " is complex set
((n . y) ") " is complex set
f is Relation-like Function-like complex-valued set
(f) is Relation-like Function-like complex-valued set
i is set
(f) . i is complex set
f . i is complex set
(f . i) " is complex set
dom (f) is set
dom f is set
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() set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f) is Relation-like Function-like complex-valued set
i is set
dom (f) is set
(f) . i is complex set
f . i is real complex ext-real set
(f . i) " is real complex ext-real set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is set
rng (f) is complex-membered ext-real-membered real-membered set
dom (f) is set
n is set
(f) . n is real complex ext-real set
f . n is real rational complex ext-real set
(f . n) " is real rational complex ext-real 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))
(n) 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) is set
dom n is Element of K19(f)
K19(f) is set
rng (n) 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))
(n) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(n) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) is complex-membered ext-real-membered real-membered Element of K19(REAL)
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))
(f,i,n) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
dom (f,i,n) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
y 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))
(f,i,n) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
y 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))
(f,i,n) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
y is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
f is Relation-like Function-like complex-valued FinSequence-like set
(f) is Relation-like Function-like complex-valued set
dom (f) 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
(f,f) is Relation-like Function-like complex-valued set
f is Relation-like Function-like complex-valued set
(f) is Relation-like Function-like set
(f,f) is Relation-like Function-like complex-valued set
dom (f) is set
dom f is set
(dom f) /\ (dom f) is set
i is set
(f) . i is set
f . i is complex set
(f . i) ^2 is set
(f . i) * (f . i) is set
0 ^2 is set
0 * 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() set
f is Relation-like Function-like complex-valued set
(f) is Relation-like Function-like set
(f,f) is Relation-like Function-like complex-valued set
f is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f) is Relation-like Function-like complex-valued set
(f,f) 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
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,f) 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
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,f) is Relation-like INT -valued 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 natural-valued set
(f) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
(f,f) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-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))
(n) is Relation-like Function-like complex-valued set
(n,n) 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) is set
dom n is Element of K19(f)
K19(f) is set
rng (n) 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,n) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,n) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,n) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(n) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
(n,n) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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))
(f,i,n) is Relation-like f -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(f,COMPLEX))
(n,n) is Relation-like Function-like complex-valued set
y 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))
(f,i,n) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
(n,n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
y 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))
(f,i,n) is Relation-like f -defined RAT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,RAT))
(n,n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
y 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))
(f,i,n) is Relation-like f -defined INT -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,INT))
(n,n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
y 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))
(f,i,n) 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))
(n,n) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
y 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
(f) is Relation-like Function-like complex-valued set
(f,f) 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
(i) is Relation-like Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued set
(f,(i)) is Relation-like Function-like complex-valued 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
(i) is Relation-like Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued 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 Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-valued set
(i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(i,(- 1)) is Relation-like 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
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
(i) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
(i,(- 1)) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued 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 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
(i) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
(i,(- 1)) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
(f,(i)) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued 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 complex-valued set
(i) is Relation-like Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued set
(f,(i)) is Relation-like Function-like complex-valued set
dom (f,i) is set
dom f is set
dom i is set
(dom f) /\ (dom i) 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 complex-valued set
(i) is Relation-like Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued set
(f,(i)) is Relation-like Function-like complex-valued set
dom (f,i) is set
n is set
(f,i) . n is complex set
f . n is complex set
i . n is complex set
(f . n) - (i . n) is set
- (i . n) is complex set
(f . n) + (- (i . n)) is set
(i) . n is complex set
(f . n) + ((i) . n) 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 complex-valued set
(i) is Relation-like Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued set
(f,(i)) is Relation-like Function-like complex-valued set
dom (f,i) is set
n is Relation-like Function-like set
dom n is set
y is set
n . y is set
(f,i) . y is complex set
f . y is complex set
i . y is complex set
(f . y) - (i . y) is set
- (i . y) is complex set
(f . y) + (- (i . y)) is set
(i) . y is complex set
(f . y) + ((i) . y) is 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
(m) is Relation-like Function-like complex-valued set
(m,(- 1)) is Relation-like Function-like complex-valued set
(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
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(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
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(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
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(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 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 complex-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
(m) is Relation-like Function-like complex-valued set
(m,(- 1)) is Relation-like Function-like complex-valued set
(y,(m)) is Relation-like Function-like complex-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
dom y is Element of K19(f)
(f,n,m) is Relation-like f -defined COMPLEX -valued Function-like total V29(f, COMPLEX ) complex-valued Element of K19(K20(f,COMPLEX))
dom (f,n,m) is Element of K19(f)
(dom y) /\ (dom (f,n,m)) is Element of K19(f)
f /\ (dom (f,n,m)) is Element of K19(f)
f /\ f is 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))
(m) is Relation-like Function-like complex-valued set
(m,(- 1)) is Relation-like Function-like complex-valued set
(y,(m)) is Relation-like Function-like complex-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(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))
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(y,(m)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(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))
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(y,(m)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(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))
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,(- 1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(y,(m)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(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 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
(m) is Relation-like Function-like complex-valued set
(m,(- 1)) is Relation-like Function-like complex-valued set
(y,(m)) is Relation-like Function-like complex-valued 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
- (m . m) is complex set
(y . m) + (- (m . m)) is set
dom (f,i,n,y,m) is Element of K19(f)
K19(f) is set
(f,n,m) is Relation-like f -defined COMPLEX -valued Function-like total V29(f, COMPLEX ) complex-valued Element of K19(K20(f,COMPLEX))
(f,n,m) . m is complex set
(y . m) + ((f,n,m) . m) is set
dom m 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
(i) is Relation-like Function-like complex-valued FinSequence-like set
(i,(- 1)) is Relation-like Function-like complex-valued FinSequence-like 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
(i) is Relation-like Function-like complex-valued set
(f,(i)) is Relation-like Function-like complex-valued 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
(i) is Relation-like Function-like complex-valued set
(f,(i)) is Relation-like Function-like complex-valued set
dom (f,i) is set
dom f is set
dom i is set
(dom f) /\ (dom i) 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
(i) is Relation-like Function-like complex-valued set
(f,(i)) is Relation-like Function-like complex-valued set
n is set
(f,i) . n is set
f . n is complex set
i . n is complex set
(f . n) / (i . n) is complex Element of COMPLEX
(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
(i) . n is complex set
(f . n) * ((i) . n) is set
0 / 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 COMPLEX
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() set
0 * (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() 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
(i) is Relation-like Function-like complex-valued 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 Relation-like Function-like complex-valued ext-real-valued real-valued set
(f,i) is Relation-like Function-like complex-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 ext-real-valued real-valued 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
(i) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
(f,(i)) is Relation-like RAT -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 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
(m) is Relation-like Function-like complex-valued set
(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
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(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
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(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 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 complex-valued Element of K19(K20(f,COMPLEX))
K20(f,COMPLEX) is Relation-like complex-valued set
K19(K20(f,COMPLEX)) is set
(m) is Relation-like Function-like complex-valued set
(y,(m)) is Relation-like Function-like complex-valued 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)
f /\ (dom m) is Element of K19(f)
f /\ f is 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))
(m) is Relation-like Function-like complex-valued set
(y,(m)) is Relation-like Function-like complex-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(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))
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(y,(m)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(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))
(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(y,(m)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (f,i,n,y,m) is Element of K19(f)
K19(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 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
(i) is Relation-like Function-like complex-valued FinSequence-like set
(f,(i)) is Relation-like Function-like complex-valued FinSequence-like set
f is Relation-like Function-like complex-valued set
dom f is set
i is Relation-like Function-like set
dom i is set
n is set
i . n is set
f . n is complex set
|.(f . n).| is real complex ext-real Element of REAL
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
n is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom n is set
y is set
i . y is real complex ext-real set
f . y is complex set
|.(f . y).| is real complex ext-real Element of REAL
n . y is real complex ext-real set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
n is Relation-like Function-like complex-valued set
dom n is set
y is set
i . y is real complex ext-real set
|.(i . y).| is real complex ext-real Element of REAL
n . y is complex set
|.(n . y).| is real complex ext-real Element of REAL
|.|.(n . y).|.| is real complex ext-real Element of REAL
f is Relation-like Function-like complex-valued set
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is set
(f) . i is real complex ext-real set
f . i is complex set
|.(f . i).| is real complex ext-real Element of REAL
dom (f) is set
dom f is set
f is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is set
rng (f) is complex-membered ext-real-membered real-membered set
dom (f) is set
n is set
(f) . n is real complex ext-real set
f . n is real rational complex ext-real set
|.(f . n).| is real rational complex ext-real Element of REAL
f is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is set
dom (f) is set
(f) . i is real complex ext-real set
f . i is real integer rational complex ext-real set
abs (f . i) 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
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))
(n) 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
dom (n) is set
dom n is Element of K19(f)
K19(f) is set
rng (n) is complex-membered ext-real-membered real-membered 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))
(n) 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) 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 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))
(n) 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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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 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))
(n) 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) 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
(f,i,n) 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 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-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) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
rng (f,i,n) 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 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))
(n) is Relation-like Function-like complex-valued ext-real-valued real-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) 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
(f,i,n) 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
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 Element of K19(K20(f,i))
(f,i,n) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
y 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))
(f,i,n) 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) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
y 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,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 Element of K19(K20(f,i))
(f,i,n) is Relation-like f -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
dom (f,i,n) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)
y 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
(f) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (f) is set
dom f 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
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)
i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is Relation-like Function-like set
dom f is set
{ (b1 + i) 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 : b1 in dom f } is set
y is set
m 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
m + i 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
f . m is set
y is Relation-like Function-like set
dom y is set
m 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
m + i 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
y . (m + i) is set
f . m is set
m 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
m + i 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
f . m 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
y . m is set
m 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
m + i 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
f . m is set
f is Relation-like Function-like 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 Function-like set
dom (f,i) is set
dom f is set
{ (b1 + i) 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 : b1 in dom f } is set
n is set
y 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
y + i 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
f is Relation-like Function-like set
i is Relation-like Function-like set
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,n) is Relation-like NAT -defined Function-like set
(i,n) is Relation-like NAT -defined Function-like set
dom f is set
dom i is set
dom (f,n) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ (b1 + n) 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 : b1 in dom f } is set
dom (i,n) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ (b1 + n) 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 : b1 in dom i } is set
y is set
m 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
m + n 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
y is set
m 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
m + n 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
(f,n) . y is set
(f,n) . (m + n) is set
f . m is set
i . m is set
(i,n) . (m + n) is set
(i,n) . y is set
i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i + f is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
n is Relation-like Function-like set
(n,i) is Relation-like NAT -defined Function-like set
((n,i),f) is Relation-like NAT -defined Function-like set
(n,(i + f)) is Relation-like NAT -defined Function-like set
dom n is set
{ (b1 + i) 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 : b1 in dom n } is set
dom (n,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
m 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
m + i 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
m + (i + 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
((n,i),f) . (m + (i + f)) is set
(m + i) + 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
((n,i),f) . ((m + i) + f) is set
(n,i) . (m + i) is set
n . m is set
{ (b1 + f) 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 : b1 in { (b1 + i) where b2 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 : b1 in dom n } } is set
{ (b1 + (i + f)) 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 : b1 in dom n } is set
m is set
m 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
m + 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
i2 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
i2 + i 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
i2 + (i + 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
m is set
m 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
m + (i + 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
m + i 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
(m + i) + 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
dom ((n,i),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 set
i is Relation-like Function-like set
f (#) i is Relation-like Function-like set
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
((f (#) i),n) is Relation-like NAT -defined Function-like set
(f,n) is Relation-like NAT -defined Function-like set
(f,n) (#) i is Relation-like NAT -defined Function-like set
dom (f (#) i) is set
dom f is set
dom (f,n) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ (b1 + n) 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 : b1 in dom f } is set
y is set
{ (b1 + n) 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 : b1 in dom (f (#) i) } is set
(f,n) . y is set
dom i is set
m 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
m + n 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
f . m is set
m 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
m + n 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
f . m is set
(f,n) " (dom i) is set
dom ((f,n) (#) i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
y 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
y + n 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
((f,n) (#) i) . (y + n) is set
(f,n) . (y + n) is set
i . ((f,n) . (y + n)) is set
f . y is set
i . (f . y) is set
(f (#) i) . y is set
f is Relation-like Function-like set
i is Relation-like Function-like set
f +* i is Relation-like Function-like set
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
((f +* i),n) is Relation-like NAT -defined Function-like set
(f,n) is Relation-like NAT -defined Function-like set
(i,n) is Relation-like NAT -defined Function-like set
(f,n) +* (i,n) is Relation-like NAT -defined Function-like set
dom (i,n) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
dom i is set
{ (b1 + n) 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 : b1 in dom i } is set
y 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
dom (f +* i) is set
y + n 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
((f,n) +* (i,n)) . (y + n) is set
(i,n) . (y + n) is set
i . y is set
(f +* i) . y is set
dom f is set
(dom f) \/ (dom i) is set
y + n 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
m 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
m + n 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
((f,n) +* (i,n)) . (y + n) is set
(f,n) . (y + n) is set
f . y is set
(f +* i) . y is set
dom (f,n) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
dom f is set
{ (b1 + n) 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 : b1 in dom f } is set
(dom (f,n)) \/ (dom (i,n)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
(dom f) \/ (dom i) is set
{ (b1 + n) 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 : b1 in (dom f) \/ (dom i) } is set
y is set
m 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
m + n 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
y is set
m 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
m + n 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
dom ((f,n) +* (i,n)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ (b1 + n) 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 : b1 in dom (f +* i) } is set
f is Relation-like Function-like set
dom f is set
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
n + i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,i) is Relation-like NAT -defined Function-like set
dom (f,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ (b1 + i) 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 : b1 in dom f } is set
y 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
y + i 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
f is Relation-like Function-like set
rng f is 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 NAT -defined Function-like set
rng (f,i) is set
n is set
dom (f,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
y is set
(f,i) . y is set
dom f is set
{ (b1 + i) 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 : b1 in dom f } is set
m 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
m + i 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
f . m is set
f is Relation-like Function-like set
dom f is set
rng f is 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 NAT -defined Function-like set
rng (f,i) is set
n is set
y is set
f . y is set
m 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
m + i 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
dom (f,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
(f,i) . (m + i) is set
f is Relation-like Function-like finite 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 NAT -defined Function-like set
dom f is finite set
{ H1(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 : b1 in dom f } is set
dom (f,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
f is non empty ext-real-membered set
K20(NAT,f) is Relation-like V12() ext-real-valued non finite set
K19(K20(NAT,f)) is V12() non finite set
i is Relation-like NAT -defined f -valued Function-like non empty total V29( NAT ,f) ext-real-valued Element of K19(K20(NAT,f))
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
n + 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
i . (n + 1) is ext-real Element of f
i . n is ext-real Element of f
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
n is ext-real set
dom i is non empty set
i . n is ext-real set
y is ext-real set
i . y is ext-real set
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
i2 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . i2 is ext-real Element of f
i2 + 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
i . (i2 + 1) is ext-real Element of f
i . 0 is ext-real Element of f
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . n is ext-real Element of f
n + 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
i . (n + 1) is ext-real Element of f
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
n is ext-real set
dom i is non empty set
i . n is ext-real set
y is ext-real set
i . y is ext-real set
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
i2 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . i2 is ext-real Element of f
i2 + 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
i . (i2 + 1) is ext-real Element of f
i . 0 is ext-real Element of f
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . n is ext-real Element of f
n + 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
i . (n + 1) is ext-real Element of f
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
n is ext-real set
dom i is non empty set
i . n is ext-real set
y is ext-real set
i . y is ext-real set
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
i2 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . i2 is ext-real Element of f
i2 + 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
i . (i2 + 1) is ext-real Element of f
i . 0 is ext-real Element of f
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
n + 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
i . (n + 1) is ext-real Element of f
i . n is ext-real Element of f
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
n is ext-real set
dom i is non empty set
i . n is ext-real set
y is ext-real set
i . y is ext-real set
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
i2 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . i2 is ext-real Element of f
i2 + 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
i . (i2 + 1) is ext-real Element of f
i . 0 is ext-real Element of f
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . m is ext-real Element of f
F1() is non empty set
K20(NAT,F1()) is Relation-like V12() non finite set
K19(K20(NAT,F1())) is V12() non finite set
F2() is Relation-like NAT -defined F1() -valued Function-like non empty total V29( NAT ,F1()) Element of K19(K20(NAT,F1()))
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
F2() . f is Element of F1()
i 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
n is set
y 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
y + 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
m 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
F2() . m is Element of F1()
m 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
i2 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
F2() . i2 is Element of F1()
m 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
m 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
F2() . m is Element of F1()
i is Relation-like Function-like set
dom i is set
i . 0 is set
rng i is set
n is set
y is set
i . y is set
m 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
i . m is set
m + 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
i . (m + 1) is set
m 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
i . m is set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() complex-valued ext-real-valued real-valued natural-valued non finite set
K19(K20(NAT,NAT)) is V12() non finite set
n is Relation-like NAT -defined NAT -valued Function-like non empty total V29( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))
y is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
y + 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
n . (y + 1) 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
n . y 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
m 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
m + 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
n . (m + 1) 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
n . m 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
y is Relation-like NAT -defined NAT -valued Function-like non empty total V29( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
F2() * y is Relation-like NAT -defined F1() -valued Function-like non empty total V29( NAT ,F1()) subsequence of F2()
m is Relation-like NAT -defined F1() -valued Function-like non empty total V29( NAT ,F1()) Element of K19(K20(NAT,F1()))
dom m is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
m is Relation-like NAT -defined F1() -valued Function-like non empty total V29( NAT ,F1()) subsequence of F2()
i2 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
m . i2 is Element of F1()
0 + 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
i2 - 1 is real integer rational complex ext-real set
i2 + (- 1) is real integer rational complex ext-real set
n9 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
n9 + 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
y . (n9 + 1) 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
y . n9 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
c10 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
c11 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
F2() . c11 is Element of F1()
k 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
F2() . k is Element of F1()
f is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i is Relation-like NAT -defined Function-like set
dom i is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
(i,f) is Relation-like NAT -defined Function-like set
dom (i,f) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
n is set
y 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
f + y 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
n is Relation-like Function-like set
dom n is set
rng n is set
y is set
m is set
n . y is set
n . m is set
m 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
f + m 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
i2 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
f + i2 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
{ (b1 + f) 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 : b1 in dom i } is set
y is set
m is set
n . m is set
m 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
f + m 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
y is set
m 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
m + 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
n . m is set
m 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
f + m 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
f is Relation-like NAT -defined Function-like set
(f,0) is Relation-like NAT -defined Function-like set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ (b1 + 0) 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 : b1 in dom f } is set
i is set
n 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
n + 0 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i is set
n 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
n + 0 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i 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
i + 0 is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f . (i + 0) is set
f . i is set
f is Relation-like NAT -defined Function-like set
(f,0) is Relation-like NAT -defined Function-like set
f is non empty set
i is Relation-like f -valued Function-like set
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(i,n) is Relation-like NAT -defined Function-like set
dom (i,n) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
dom i is set
{ (b1 + n) 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 : b1 in dom i } is set
rng (i,n) is set
y is set
m is set
(i,n) . m is set
m 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
m + n 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
(i,n) . (m + n) is set
i . m is set
i /. m is Element of f
id NAT is Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like one-to-one non empty total V29( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() complex-valued ext-real-valued real-valued natural-valued non finite set
K19(K20(NAT,NAT)) is V12() non finite set
f 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
i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,i) is Relation-like NAT -defined RAT -valued Function-like complex-valued ext-real-valued real-valued finite set
dom (f,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V66() V67() V68() Element of K19(NAT)
dom f 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
{ (b1 + i) 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 : b1 in dom f } is set
n is Relation-like Function-like non empty set
dom n is non empty set
y is set
m 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
m + i 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
f is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like set
dom (f,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
{ (b1 + i) 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 : b1 in dom f } is set
n is set
y 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
m is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
m 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
m + i 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
f is Relation-like Function-like 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 NAT -defined Function-like set
dom (f,i) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
dom f is set
{ (b1 + i) 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 : b1 in dom f } is set
n 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
n + i 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
{0} is functional non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
0 .--> 0 is Relation-like NAT -defined {0} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V12() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing finite Function-yielding V71() set
{0} --> 0 is Relation-like {0} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant non empty total V29({0},{0}) complex-valued ext-real-valued real-valued natural-valued finite Function-yielding V71() Element of K19(K20({0},{0}))
K20({0},{0}) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
K19(K20({0},{0})) is finite V57() set
f is Relation-like NAT -defined {0} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V12() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing finite Function-yielding V71() set
dom f is functional V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() V66() V67() V68() Element of K19({0})
K19({0}) is finite V57() set
f is Relation-like NAT -defined 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 NAT -defined Function-like non empty finite set
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is Relation-like NAT -defined Function-like non empty finite set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f . (f) is set
(f) .--> (f . (f)) is Relation-like NAT -defined {(f)} -defined Function-like one-to-one constant V12() finite set
{(f)} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{(f)} --> (f . (f)) is Relation-like {(f)} -defined {(f . (f))} -valued Function-like constant non empty total V29({(f)},{(f . (f))}) finite Element of K19(K20({(f)},{(f . (f))}))
{(f . (f))} is non empty V12() finite 1 -element set
K20({(f)},{(f . (f))}) is Relation-like finite set
K19(K20({(f)},{(f . (f))})) is finite V57() set
f \ ((f) .--> (f . (f))) is Relation-like NAT -defined Function-like finite Element of K19(f)
K19(f) is finite V57() set
f is Relation-like NAT -defined Function-like non empty finite set
(f) is Relation-like Function-like set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f . (f) is set
(f) .--> (f . (f)) is Relation-like NAT -defined {(f)} -defined Function-like one-to-one constant V12() finite set
{(f)} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{(f)} --> (f . (f)) is Relation-like {(f)} -defined {(f . (f))} -valued Function-like constant non empty total V29({(f)},{(f . (f))}) finite Element of K19(K20({(f)},{(f . (f))}))
{(f . (f))} is non empty V12() finite 1 -element set
K20({(f)},{(f . (f))}) is Relation-like finite set
K19(K20({(f)},{(f . (f))})) is finite V57() set
f \ ((f) .--> (f . (f))) is Relation-like NAT -defined Function-like finite Element of K19(f)
K19(f) is finite V57() set
f is Relation-like NAT -defined Function-like non empty finite set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is Relation-like NAT -defined Function-like non empty finite set
i is Relation-like NAT -defined Function-like non empty finite set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(i) 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
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom i) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i 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
f is Relation-like NAT -defined Function-like non empty finite set
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
(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
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is Relation-like NAT -defined Function-like non empty set
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V64() V66() Element of K19(NAT)
inf (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is Relation-like NAT -defined Function-like non empty finite set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
inf (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is Relation-like NAT -defined Function-like non empty finite set
i is Relation-like NAT -defined Function-like non empty finite set
(i) 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
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
inf (dom i) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
inf (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
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
i is Relation-like NAT -defined Function-like non empty finite set
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
(i) 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
inf (dom i) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f is Relation-like NAT -defined Function-like non empty finite set
(f) is Relation-like NAT -defined Function-like finite set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f . (f) is set
(f) .--> (f . (f)) is Relation-like NAT -defined {(f)} -defined Function-like one-to-one constant V12() finite set
{(f)} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{(f)} --> (f . (f)) is Relation-like {(f)} -defined {(f . (f))} -valued Function-like constant non empty total V29({(f)},{(f . (f))}) finite Element of K19(K20({(f)},{(f . (f))}))
{(f . (f))} is non empty V12() finite 1 -element set
K20({(f)},{(f . (f))}) is Relation-like finite set
K19(K20({(f)},{(f . (f))})) is finite V57() set
f \ ((f) .--> (f . (f))) is Relation-like NAT -defined Function-like finite Element of K19(f)
K19(f) is finite V57() set
dom (f) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V66() V67() V68() Element of K19(NAT)
(dom f) \ {(f)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V66() V67() V68() Element of K19(NAT)
dom ((f) .--> (f . (f))) is V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() V66() V67() V68() Element of K19({(f)})
K19({(f)}) is finite V57() set
[(f),(f . (f))] is set
{(f),(f . (f))} is non empty finite set
{{(f),(f . (f))},{(f)}} is non empty finite V57() set
{[(f),(f . (f))]} is Relation-like Function-like constant non empty V12() finite 1 -element set
i is Relation-like set
dom i is set
n is set
f \ i is Relation-like NAT -defined Function-like finite Element of K19(f)
y is set
[n,y] is set
{n,y} is non empty finite set
{n} is non empty V12() finite 1 -element set
{{n,y},{n}} is non empty finite V57() set
f is Relation-like NAT -defined Function-like non empty finite set
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
(f) is Relation-like NAT -defined Function-like finite set
(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
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f . (f) is set
(f) .--> (f . (f)) is Relation-like NAT -defined {(f)} -defined Function-like one-to-one constant V12() finite set
{(f)} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{(f)} --> (f . (f)) is Relation-like {(f)} -defined {(f . (f))} -valued Function-like constant non empty total V29({(f)},{(f . (f))}) finite Element of K19(K20({(f)},{(f . (f))}))
{(f . (f))} is non empty V12() finite 1 -element set
K20({(f)},{(f . (f))}) is Relation-like finite set
K19(K20({(f)},{(f . (f))})) is finite V57() set
f \ ((f) .--> (f . (f))) is Relation-like NAT -defined Function-like finite Element of K19(f)
K19(f) is finite V57() set
dom (f) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V66() V67() V68() Element of K19(NAT)
(dom (f)) \/ {(f)} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() set
(dom f) \ {(f)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V66() V67() V68() Element of K19(NAT)
0 .--> 0 is Relation-like NAT -defined {0} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V12() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing finite Function-yielding V71() set
{0} is functional non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{0} --> 0 is Relation-like {0} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant non empty total V29({0},{0}) complex-valued ext-real-valued real-valued natural-valued finite Function-yielding V71() Element of K19(K20({0},{0}))
K20({0},{0}) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
K19(K20({0},{0})) is finite V57() set
f is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element set
(f) is Relation-like NAT -defined Function-like finite set
(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
dom f is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite 1 -element V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f . (f) is set
(f) .--> (f . (f)) is Relation-like NAT -defined {(f)} -defined Function-like one-to-one constant V12() finite set
{(f)} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{(f)} --> (f . (f)) is Relation-like {(f)} -defined {(f . (f))} -valued Function-like constant non empty total V29({(f)},{(f . (f))}) finite Element of K19(K20({(f)},{(f . (f))}))
{(f . (f))} is non empty V12() finite 1 -element set
K20({(f)},{(f . (f))}) is Relation-like finite set
K19(K20({(f)},{(f . (f))})) is finite V57() set
f \ ((f) .--> (f . (f))) is Relation-like NAT -defined Function-like finite Element of K19(f)
K19(f) is finite V57() set
[(f),(f . (f))] is set
{(f),(f . (f))} is non empty finite set
{{(f),(f . (f))},{(f)}} is non empty finite V57() set
i is set
{[(f),(f . (f))]} is Relation-like Function-like constant non empty V12() finite 1 -element set
f is Relation-like NAT -defined Function-like non empty finite set
(f) is Relation-like NAT -defined Function-like finite set
(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
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom f) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
f . (f) is set
(f) .--> (f . (f)) is Relation-like NAT -defined {(f)} -defined Function-like one-to-one constant V12() finite set
{(f)} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{(f)} --> (f . (f)) is Relation-like {(f)} -defined {(f . (f))} -valued Function-like constant non empty total V29({(f)},{(f . (f))}) finite Element of K19(K20({(f)},{(f . (f))}))
{(f . (f))} is non empty V12() finite 1 -element set
K20({(f)},{(f . (f))}) is Relation-like finite set
K19(K20({(f)},{(f . (f))})) is finite V57() set
f \ ((f) .--> (f . (f))) is Relation-like NAT -defined Function-like finite Element of K19(f)
K19(f) is finite V57() set
card (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 omega
card f 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 omega
(card f) - 1 is real integer rational complex ext-real set
(card f) + (- 1) is real integer rational complex ext-real set
i is set
n is set
[i,n] is set
{i,n} is non empty finite set
{i} is non empty V12() finite 1 -element set
{{i,n},{i}} is non empty finite V57() set
[(f),(f . (f))] is set
{(f),(f . (f))} is non empty finite set
{{(f),(f . (f))},{(f)}} is non empty finite V57() set
{[(f),(f . (f))]} is Relation-like Function-like constant non empty V12() finite 1 -element set
card ((f) .--> (f . (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 omega
(card f) - (card ((f) .--> (f . (f)))) is real integer rational complex ext-real set
- (card ((f) .--> (f . (f)))) is real integer rational complex ext-real non positive set
(card f) + (- (card ((f) .--> (f . (f))))) is real integer rational complex ext-real set
[(f),(f . (f))] is set
{(f),(f . (f))} is non empty finite set
{{(f),(f . (f))},{(f)}} is non empty finite V57() set
{[(f),(f . (f))]} is Relation-like Function-like constant non empty V12() finite 1 -element set
card {[(f),(f . (f))]} 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 omega
(card f) - (card {[(f),(f . (f))]}) is real integer rational complex ext-real set
- (card {[(f),(f . (f))]}) is real integer rational complex ext-real non positive set
(card f) + (- (card {[(f),(f . (f))]})) is real integer rational complex ext-real set
f is set
i is Relation-like f -defined Function-like complex-valued set
(i) is Relation-like Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued set
dom (i) is set
dom i is Element of K19(f)
K19(f) is set
(i) is Relation-like Function-like complex-valued set
dom (i) is set
dom i is Element of K19(f)
K19(f) is set
(i) is Relation-like Function-like complex-valued set
(i,i) is Relation-like Function-like complex-valued set
dom (i) is set
dom i is Element of K19(f)
K19(f) is set
(i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (i) is set
dom i is Element of K19(f)
K19(f) is set
f 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
the Relation-like f -defined NAT -valued Function-like total V29(f, NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT)) is Relation-like f -defined NAT -valued Function-like total V29(f, NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,NAT))
f is set
i is Relation-like f -defined Function-like total complex-valued set
(i) is Relation-like f -defined Function-like complex-valued set
(i,(- 1)) is Relation-like Function-like complex-valued set
dom (i) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
(i) is Relation-like f -defined Function-like complex-valued set
dom (i) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
(i) is Relation-like f -defined Function-like complex-valued set
(i,i) is Relation-like Function-like complex-valued set
dom (i) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
(i) is Relation-like f -defined Function-like complex-valued ext-real-valued real-valued set
dom (i) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
f is set
i is Relation-like f -defined Function-like complex-valued set
n is complex set
(i,n) is Relation-like Function-like complex-valued set
dom (i,n) is set
dom i is Element of K19(f)
K19(f) is set
(i,n) is Relation-like Function-like complex-valued set
- n is complex set
(i,(- n)) is Relation-like f -defined Function-like complex-valued set
(i,n) is Relation-like Function-like complex-valued set
dom (i,n) is set
dom i is Element of K19(f)
K19(f) is set
f is set
i is Relation-like f -defined Function-like total complex-valued set
n is complex set
(i,n) is Relation-like f -defined Function-like complex-valued set
dom (i,n) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
(i,n) is Relation-like f -defined Function-like complex-valued set
- n is complex set
(i,(- n)) is Relation-like f -defined Function-like total complex-valued set
(i,n) is Relation-like f -defined Function-like complex-valued set
dom (i,n) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
f is set
i is Relation-like Function-like complex-valued set
n is Relation-like f -defined Function-like complex-valued set
(i,n) is Relation-like Function-like complex-valued set
dom (i,n) is set
dom i is set
dom n is Element of K19(f)
K19(f) is set
(dom i) /\ (dom n) is Element of K19(f)
(i,n) is Relation-like Function-like complex-valued set
(n) is Relation-like f -defined Function-like complex-valued set
(n,(- 1)) is Relation-like f -defined Function-like complex-valued set
(i,(n)) is Relation-like f -defined Function-like complex-valued set
(i,n) is Relation-like Function-like complex-valued set
dom (i,n) is set
dom i is set
dom n is Element of K19(f)
K19(f) is set
(dom i) /\ (dom n) is Element of K19(f)
(i,n) is Relation-like Function-like complex-valued set
(n) is Relation-like f -defined Function-like complex-valued set
(i,(n)) is Relation-like f -defined Function-like complex-valued set
f is set
i is Relation-like f -defined Function-like total complex-valued set
n is Relation-like f -defined Function-like total complex-valued set
(i,n) is Relation-like f -defined Function-like complex-valued set
dom (i,n) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
dom n is Element of K19(f)
(dom i) /\ (dom n) is Element of K19(f)
(i,n) is Relation-like f -defined Function-like complex-valued set
(n) is Relation-like f -defined Function-like total complex-valued set
(n,(- 1)) is Relation-like f -defined Function-like total complex-valued set
(i,(n)) is Relation-like f -defined Function-like total complex-valued set
(i,n) is Relation-like f -defined Function-like complex-valued set
dom (i,n) is Element of K19(f)
K19(f) is set
dom i is Element of K19(f)
dom n is Element of K19(f)
(dom i) /\ (dom n) is Element of K19(f)
(i,n) is Relation-like f -defined Function-like complex-valued set
(n) is Relation-like f -defined Function-like total complex-valued set
(i,(n)) is Relation-like f -defined Function-like total complex-valued set
f is non empty set
i is Relation-like NAT -defined f -valued Function-like non empty finite set
(i) is Relation-like NAT -defined Function-like finite set
(i) 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
dom i is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V64() V65() V66() V67() V68() Element of K19(NAT)
sup (dom i) is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
i . (i) is set
(i) .--> (i . (i)) is Relation-like NAT -defined {(i)} -defined Function-like one-to-one constant V12() finite set
{(i)} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite V57() 1 -element V64() V65() V66() V67() V68() set
{(i)} --> (i . (i)) is Relation-like {(i)} -defined {(i . (i))} -valued Function-like constant non empty total V29({(i)},{(i . (i))}) finite Element of K19(K20({(i)},{(i . (i))}))
{(i . (i))} is non empty V12() finite 1 -element set
K20({(i)},{(i . (i))}) is Relation-like finite set
K19(K20({(i)},{(i . (i))})) is finite V57() set
i \ ((i) .--> (i . (i))) is Relation-like NAT -defined f -valued Function-like finite Element of K19(i)
K19(i) is finite V57() set
f is Relation-like Function-like set
dom f is set
i is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural real integer rational complex ext-real non negative finite cardinal set
(f,n) is Relation-like NAT -defined Function-like set
dom (f,n) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K19(NAT)
{ (b1 + n) 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 : b1 in dom f } is set
y 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
y + n 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