:: VALUED_1 semantic presentation

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)

{ b

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)

{ b

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)

{ b

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