:: VALUED_1 semantic presentation

REAL is non empty V12() complex-membered ext-real-membered real-membered V51() non finite V66() V67() V69() set

K19(REAL) is V12() non finite set
COMPLEX is non empty V12() complex-membered V51() non finite set

K19(omega) is V12() non finite set
K19(NAT) is V12() non finite set

dom i is set

{ } is set

dom n is set

{ } is set

{ } is set

dom f is set
dom i is set
(dom f) /\ (dom i) is set

dom y is set

dom y is 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

dom y is set

dom m is 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,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

n is set
dom (f,i) is set
(f,i) . n is complex set

(f . n) + (i . n) is real complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

(f . y) + (i . y) is real rational complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

(f . y) + (i . y) is real integer rational complex ext-real set

n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is 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

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,REAL)) is 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

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,RAT)) is 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

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,INT)) is 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)

K19(RAT) is V12() non finite set
f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,NAT)) is 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)

K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set

K19(K20(f,i)) is set
n is non empty complex-membered set

K19(K20(f,n)) is 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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,REAL)) is set

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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,RAT)) is set

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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,INT)) is set

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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,NAT)) is set

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

f is set
i is non empty complex-membered set

K19(K20(f,i)) is set
n is non empty complex-membered 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))

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)

dom (f,i) is set

i is complex set

dom f is set

dom n is set

dom n is 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

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

n is set
dom (f,i) is set
(f,i) . n is complex set

i + (f . n) is real complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

i + (f . y) is real rational complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set

f is set

K19(K20(f,i)) is set

y is complex 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

K19(K20(f,i)) is set

K19(K20(f,REAL)) is 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)

K19(COMPLEX) is V12() non finite set
f is set

K19(K20(f,i)) is set

K19(K20(f,RAT)) is 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

K19(K20(f,i)) is set

K19(K20(f,INT)) is 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)

K19(RAT) is V12() non finite set
f is set

K19(K20(f,i)) is set

K19(K20(f,NAT)) is 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)

K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is set

K19(K20(f,NAT)) is set

dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)

f is non empty set
i is non empty complex-membered 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))

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

i is complex set

dom (f,i) is set

i is complex set
- i is complex set
(f,(- i)) 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

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 set

K19(K20(f,i)) is set

y is complex set

- y is complex set
(n,(- y)) is Relation-like Function-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

K19(K20(f,i)) is set

K19(K20(f,REAL)) is 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)

K19(COMPLEX) is V12() non finite set
f is set

K19(K20(f,i)) is set

K19(K20(f,RAT)) is 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

K19(K20(f,i)) is set

K19(K20(f,INT)) is 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)

K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set

K19(K20(f,i)) is 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

f is set

K19(K20(f,i)) is set

K19(K20(f,REAL)) is set

f is set

K19(K20(f,i)) is set

K19(K20(f,RAT)) is set

f is set

K19(K20(f,i)) is set

K19(K20(f,INT)) is set

f is non empty set
i is non empty complex-membered 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))

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

i is complex set

- i is complex set

dom f is set
dom i is set
(dom f) /\ (dom i) is set

dom y is set

dom y is 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

dom y is set

dom m is 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,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,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

n is set
dom (f,i) is set
(f,i) . n is complex set

(f . n) * (i . n) is real complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

(f . y) * (i . y) is real rational complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

(f . y) * (i . y) is real integer rational complex ext-real set

n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is 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

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,REAL)) is 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

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,RAT)) is 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

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,INT)) is 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)

K19(RAT) is V12() non finite set
f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,NAT)) is 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)

K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set

K19(K20(f,i)) is set
n is non empty complex-membered set

K19(K20(f,n)) is 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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,REAL)) is set

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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,RAT)) is set

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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,INT)) is set

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

f is set

K19(K20(f,i)) is set

K19(K20(f,n)) is set

K19(K20(f,NAT)) is set

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

dom (f,i) is set

i is complex set

dom f is set

dom n is set

dom n is 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

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

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

n is set
dom (f,i) is set
(f,i) . n is complex set

i * (f . n) is real complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

i * (f . y) is real rational complex ext-real set

n is set

dom (f,i) is set
y is set
(f,i) . y is real complex ext-real set

n is set
dom (f,i) is set
(f,i) . n is real rational complex ext-real set

f is set

K19(K20(f,i)) is set

y is complex 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

K19(K20(f,i)) is set

K19(K20(f,REAL)) is 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)

K19(COMPLEX) is V12() non finite set
f is set

K19(K20(f,i)) is set

K19(K20(f,RAT)) is 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

K19(K20(f,i)) is set

K19(K20(f,INT)) is 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)

K19(RAT) is V12() non finite set
f is set

K19(K20(f,i)) is set

K19(K20(f,NAT)) is 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)

K19(RAT) is V12() non finite set
f is set
i is non empty complex-membered set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is 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)

f is set

K19(K20(f,i)) is set

K19(K20(f,NAT)) is set

dom (f,i,n,y) is Element of K19(f)
K19(f) is set
dom n is Element of K19(f)