:: VALUED_2 semantic presentation

K235() is set

K19(REAL) is set

K226() is set

K20(,K226()) is Relation-like set
K226() \/ K20(,K226()) is set
is set

is non empty set

(K226() \/ K20(,K226())) \ is Element of K19((K226() \/ K20(,K226())))
K19((K226() \/ K20(,K226()))) is set
K20(,K235()) is Relation-like set
K235() \/ K20(,K235()) is set
(K235() \/ K20(,K235())) \ is Element of K19((K235() \/ K20(,K235())))
K19((K235() \/ K20(,K235()))) is set
COMPLEX is non empty complex-membered V59() V60() set

Funcs ({{},1},REAL) is non empty FUNCTION_DOMAIN of {{},1}, REAL
{ } is set
(Funcs ({{},1},REAL)) \ { } is Element of K19((Funcs ({{},1},REAL)))
K19((Funcs ({{},1},REAL))) is set
((Funcs ({{},1},REAL)) \ { } ) \/ REAL is non empty set

omega \/ K20(,omega) is non empty set
() \ is Element of K19(())
K19(()) is set
K19(omega) is set
K19(NAT) is set
K19(K226()) is set
K19(K19(K226())) is set
K234() is Element of K19(K19(K226()))

ff is set
X is set
X1 is set
X /\ X1 is set
ff /\ (X /\ X1) is set
ff /\ ff is set
(ff /\ ff) /\ X is set
((ff /\ ff) /\ X) /\ X1 is set
ff /\ X is set
ff /\ (ff /\ X) is set
(ff /\ (ff /\ X)) /\ X1 is set
ff /\ X1 is set
(ff /\ X) /\ (ff /\ X1) is set
ff is functional set
{ (dom b1) where b1 is Relation-like Function-like Element of ff : verum } is set
union { (dom b1) where b1 is Relation-like Function-like Element of ff : verum } is set
ff is set
X is set
ff is set
X is set
ff is set
X is set
ff is set
X is set
ff is set
X is set
ff is set
X is set

{ff} is functional non empty set
X is set
ff is set
X is set
ff is set
X is set

{} is functional non empty () set
X is set
X is functional () set
K19(X) is set
X1 is functional Element of K19(X)
X2 is set
X is functional () set
K19(X) is set
X1 is functional Element of K19(X)
X2 is set
X is functional () () () set
K19(X) is set
X1 is functional () () Element of K19(X)
X2 is set
X is functional () () () () set
K19(X) is set
X1 is functional () () () Element of K19(X)
X2 is set
X is functional () () () () () set
K19(X) is set
X1 is functional () () () () Element of K19(X)
X2 is set
X is functional () () () () () () set
K19(X) is set
X1 is functional () () () () () Element of K19(X)
X2 is set
X1 is set

K19(K20(X1,COMPLEX)) is set
PFuncs (X1,COMPLEX) is set
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,COMPLEX)) is set
Funcs (X1,COMPLEX) is non empty FUNCTION_DOMAIN of X1, COMPLEX
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
ExtREAL is non empty ext-real-membered set
[K100(),REAL] is set
{K100(),REAL} is non empty set

{{K100(),REAL},{K100()}} is non empty set
{REAL,[K100(),REAL]} is non empty set
REAL \/ {REAL,[K100(),REAL]} is non empty set
X1 is set

K19(K20(X1,ExtREAL)) is set
PFuncs (X1,ExtREAL) is set
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,ExtREAL)) is set
Funcs (X1,ExtREAL) is non empty FUNCTION_DOMAIN of X1, ExtREAL
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,REAL)) is set
PFuncs (X1,REAL) is set
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,REAL)) is set
Funcs (X1,REAL) is non empty FUNCTION_DOMAIN of X1, REAL
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,RAT)) is set
PFuncs (X1,RAT) is set
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,RAT)) is set
Funcs (X1,RAT) is non empty FUNCTION_DOMAIN of X1, RAT
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,INT)) is set
PFuncs (X1,INT) is set
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,INT)) is set
Funcs (X1,INT) is non empty FUNCTION_DOMAIN of X1, INT
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,NAT)) is set
PFuncs (X1,NAT) is set
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X1 is set

K19(K20(X1,NAT)) is set
Funcs (X1,NAT) is non empty FUNCTION_DOMAIN of X1, NAT
X2 is set
Y is set
X2 is set
Y is set
Y1 is set
Y2 is set
Y1 is set
Y2 is set
X is set
(X) is set
(X) is set
K19((X)) is set
X1 is set

K19(K20(X,COMPLEX)) is set
X is set
(X) is set
(X) is set
K19((X)) is set
X1 is set

K19(K20(X,ExtREAL)) is set
X is set
(X) is set
(X) is set
K19((X)) is set
X1 is set

K19(K20(X,REAL)) is set
X is set
(X) is set
(X) is set
K19((X)) is set
X1 is set

K19(K20(X,RAT)) is set
X is set
(X) is set
(X) is set
K19((X)) is set
X1 is set

K19(K20(X,INT)) is set
X is set
(X) is set
(X) is set
K19((X)) is set
X1 is set

K19(K20(X,NAT)) is set
X is set
(X) is set
X1 is set
(X) is set
K19((X)) is set
X1 is functional () Element of K19((X))
(X) is set
X1 is set
(X) is set
K19((X)) is set
X1 is functional () Element of K19((X))
(X) is set
X1 is set
(X) is set
K19((X)) is set
X1 is functional () () () Element of K19((X))
(X) is set
X1 is set
(X) is set
K19((X)) is set
X1 is functional () () () () Element of K19((X))
(X) is set
X1 is set
(X) is set
K19((X)) is set
X1 is functional () () () () () Element of K19((X))
(X) is set
X1 is set
(X) is set
K19((X)) is set
X1 is functional () () () () () () Element of K19((X))
X is functional () set

X is functional () set

X is functional () () () set

X is functional () () () () set

X is functional () () () () () set

X is functional () () () () () () set

X is set
X2 is functional () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

X is set
X2 is functional () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

X is set
X2 is functional () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

dom Y is Element of K19(X)
K19(X) is set
rng Y is functional () Element of K19(X2)
K19(X2) is set
dom Y is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
K19(X) is set
X is set
X2 is functional () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

dom Y is Element of K19(X)
K19(X) is set
rng Y is functional () Element of K19(X2)
K19(X2) is set
dom Y is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
K19(X) is set
X is set
X2 is functional () () () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

dom Y is Element of K19(X)
K19(X) is set
rng Y is functional () () () Element of K19(X2)
K19(X2) is set
dom Y is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
K19(X) is set
X is set
X2 is functional () () () () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

dom Y is Element of K19(X)
K19(X) is set
rng Y is functional () () () () Element of K19(X2)
K19(X2) is set
dom Y is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
K19(X) is set
X is set
X2 is functional () () () () () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

dom Y is Element of K19(X)
K19(X) is set
rng Y is functional () () () () () Element of K19(X2)
K19(X2) is set
dom Y is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
K19(X) is set
X is set
X2 is functional () () () () () () set
K20(X,X2) is Relation-like set
K19(K20(X,X2)) is set
Y is Relation-like X -defined X2 -valued Function-like Element of K19(K20(X,X2))
X1 is set

dom Y is Element of K19(X)
K19(X) is set
rng Y is functional () () () () () () Element of K19(X2)
K19(X2) is set
dom Y is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
K19(X) is set
X is set

PFuncs (X,X1) is set
X2 is set

dom Y is set
rng Y is set
K20(X,X1) is Relation-like complex-valued set
K19(K20(X,X1)) is set
Y1 is Relation-like X -defined X1 -valued Function-like complex-valued Element of K19(K20(X,X1))
X is set

PFuncs (X,X1) is set
X2 is set

dom Y is set
rng Y is set
K20(X,X1) is Relation-like ext-real-valued set
K19(K20(X,X1)) is set

X is set

PFuncs (X,X1) is functional () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is set

PFuncs (X,X1) is functional () () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is set

PFuncs (X,X1) is functional () () () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is set

PFuncs (X,X1) is functional () () () () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is set

Funcs (X,X1) is set
X2 is set

dom Y is set
rng Y is set
K20(X,X1) is Relation-like complex-valued set
K19(K20(X,X1)) is set
Y1 is Relation-like X -defined X1 -valued Function-like complex-valued Element of K19(K20(X,X1))
X is set

Funcs (X,X1) is set
X2 is set

dom Y is set
rng Y is set
K20(X,X1) is Relation-like ext-real-valued set
K19(K20(X,X1)) is set

X is set

Funcs (X,X1) is functional () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is set

Funcs (X,X1) is functional () () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is set

Funcs (X,X1) is functional () () () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is set

Funcs (X,X1) is functional () () () () () set
X2 is set

dom Y is set
rng Y is set

K19(K20(X,X1)) is set

X is functional () set

rng X1 is functional () Element of K19(X)
K19(X) is set

dom X is set
rng X is set
X1 is set
X . X1 is set
X1 is set
rng X is set
X2 is set
X . X2 is set
rng X is set
X1 is set
X . X1 is set
X1 is set
rng X is set
X2 is set
X . X2 is set
rng X is set
X1 is set
X . X1 is set
X1 is set
rng X is set
X2 is set
X . X2 is set
rng X is set
X1 is set
X . X1 is set
X1 is set
rng X is set
X2 is set
X . X2 is set
rng X is set
X1 is set
X . X1 is set
X1 is set
rng X is set
X2 is set
X . X2 is set
rng X is set
X1 is set
X . X1 is set
X1 is set
rng X is set
X2 is set
X . X2 is set

rng X is set
X1 is set

rng X is set
X1 is set

rng X is set
X1 is set

rng X is set
X1 is set

rng X is set
X1 is set

X1 is set
rng X is set
X is Relation-like () set
rng X is set
X is Relation-like () set
rng X is set
X is Relation-like () () () set
rng X is functional () () set
X is Relation-like () () () () set
rng X is functional () () () set
X is Relation-like () () () () () set
rng X is functional () () () () set
X is Relation-like () () () () () () set
rng X is functional () () () () () set
X is set
X1 is functional () set
K20(X,X1) is Relation-like set
K19(K20(X,X1)) is set
X2 is Relation-like X -defined X1 -valued Function-like () Element of K19(K20(X,X1))
X is set
X1 is functional () set
K20(X,X1) is Relation-like set
K19(K20(X,X1)) is set
X2 is Relation-like X -defined X1 -valued Function-like Element of K19(K20(X,X1))
Y is set
dom X2 is set

X is set
X1 is functional () () () set
K20(X,X1) is Relation-like set
K19(K20(X,X1)) is set
X2 is Relation-like X -defined X1 -valued Function-like () () Element of K19(K20(X,X1))
Y is set
dom X2 is set

X is set
X1 is functional () () () () set
K20(X,X1) is Relation-like set
K19(K20(X,X1)) is set
X2 is Relation-like X -defined X1 -valued Function-like () () () Element of K19(K20(X,X1))
Y is set
dom X2 is set

X is set
X1 is functional () () () () () set
K20(X,X1) is Relation-like set
K19(K20(X,X1)) is set
X2 is Relation-like X -defined X1 -valued Function-like () () () () Element of K19(K20(X,X1))
Y is set
dom X2 is set

X is set
X1 is functional () () () () () () set
K20(X,X1) is Relation-like set
K19(K20(X,X1)) is set
X2 is Relation-like X -defined X1 -valued Function-like () () () () () Element of K19(K20(X,X1))
Y is set
dom X2 is set

X1 is set
X . X1 is set
dom X is set
rng X is functional () set
dom X is set
dom X is set

X1 is set
X . X1 is set
dom X is set
rng X is functional () set
dom X is set
dom X is set

X1 is set

dom X is set
rng X is functional () set
dom X is set
dom X is set

X1 is set

dom X is set
rng X is functional () set
dom X is set
dom X is set
X is Relation-like Function-like () () () set
X1 is set

dom X is set
rng X is functional () () () set
dom X is set
dom X is set
X is Relation-like Function-like () () () () set
X1 is set

dom X is set
rng X is functional () () () () set
dom X is set
dom X is set
X is Relation-like Function-like () () () () () set
X1 is set

dom X is set
rng X is functional () () () () () set
dom X is set
dom X is set
X is Relation-like Function-like () () () () () () set
X1 is set

dom X is set
rng X is functional () () () () () () set
dom X is set
dom X is set
X is complex set
X1 is complex set

dom X2 is set
Y is set
dom (X1 + X2) is set
(X1 + X2) . Y is complex set
X2 . Y is complex set
(X2 . Y) + X1 is complex set
dom (X + X2) is set
(X + X2) . Y is complex set
(X2 . Y) + X is complex set
X is complex set
X1 is complex set

- X is complex set

- X1 is complex set

dom X2 is set
Y is set
dom (X2 - X1) is set
(X2 - X1) . Y is complex set
X2 . Y is complex set
(X2 . Y) - X1 is complex set
(X2 . Y) + (- X1) is complex set
dom (X2 - X) is set
(X2 - X) . Y is complex set
(X2 . Y) - X is complex set
(X2 . Y) + (- X) is complex set
X is complex set
X1 is complex set

dom X2 is set
Y is set
X2 . Y is complex set

(X (#) X2) . Y is complex set
(X2 . Y) * X is complex set
(X1 (#) X2) . Y is complex set
(X2 . Y) * X1 is complex set
X is complex set

- 1 is non empty complex V37() real integer rational set
(- 1) (#) (X + X1) is Relation-like Function-like complex-valued set

- X is complex set

dom (- (X + X1)) is set
dom (X + X1) is set
dom X1 is set
dom ((- X1) - X) is set
dom (- X1) is set
X2 is set
(- (X + X1)) . X2 is complex set
((- X1) - X) . X2 is complex set
(X + X1) . X2 is complex set
- ((X + X1) . X2) is complex set
X1 . X2 is complex set
(X1 . X2) + X is complex set
- ((X1 . X2) + X) is complex set
- (X1 . X2) is complex set
(- (X1 . X2)) - X is complex set
(- (X1 . X2)) + (- X) is complex set
(- X1) . X2 is complex set
((- X1) . X2) - X is complex set
((- X1) . X2) + (- X) is complex set
X is complex set

- X is complex set

- 1 is non empty complex V37() real integer rational set
(- 1) (#) (X1 - X) is Relation-like Function-like complex-valued set

dom (- (X1 - X)) is set
dom (X1 - X) is set
dom X1 is set
dom (X + (- X1)) is set
dom (- X1) is set
X2 is set
(- (X1 - X)) . X2 is complex set
(X + (- X1)) . X2 is complex set
(X1 - X) . X2 is complex set
- ((X1 - X) . X2) is complex set
X1 . X2 is complex set
(X1 . X2) - X is complex set
(X1 . X2) + (- X) is complex set
- ((X1 . X2) - X) is complex set
- (X1 . X2) is complex set
(- (X1 . X2)) + X is complex set
(- X1) . X2 is complex set
((- X1) . X2) + X is complex set
X is complex set
X1 is complex set
X + X1 is complex set

dom (X1 + (X + X2)) is set
dom (X + X2) is set
dom X2 is set
dom ((X + X1) + X2) is set
Y is set
(X1 + (X + X2)) . Y is complex set
((X + X1) + X2) . Y is complex set
(X + X2) . Y is complex set
((X + X2) . Y) + X1 is complex set
X2 . Y is complex set
(X2 . Y) + X is complex set
((X2 . Y) + X) + X1 is complex set
(X2 . Y) + (X + X1) is complex set
X is complex set
X1 is complex set
X - X1 is complex set
- X1 is complex set
X + (- X1) is complex set

(- X1) + (X + X2) is Relation-like Function-like complex-valued set

dom ((X + X2) - X1) is set
dom (X + X2) is set
dom X2 is set
dom ((X - X1) + X2) is set
Y is set
((X + X2) - X1) . Y is complex set
((X - X1) + X2) . Y is complex set
(X + X2) . Y is complex set
((X + X2) . Y) - X1 is complex set
((X + X2) . Y) + (- X1) is complex set
X2 . Y is complex set
(X2 . Y) + X is complex set
((X2 . Y) + X) - X1 is complex set
((X2 . Y) + X) + (- X1) is complex set
(X2 . Y) + (X - X1) is complex set
X is complex set
X1 is complex set
X - X1 is complex set
- X1 is complex set
X + (- X1) is complex set

- X is complex set

- (X - X1) is complex set
(- (X - X1)) + X2 is Relation-like Function-like complex-valued set
dom (X1 + (X2 - X)) is set
dom (X2 - X) is set
dom X2 is set
dom (X2 - (X - X1)) is set
Y is set
(X1 + (X2 - X)) . Y is complex set
(X2 - (X - X1)) . Y is complex set
(X2 - X) . Y is complex set
((X2 - X) . Y) + X1 is complex set
X2 . Y is complex set
(X2 . Y) - X is complex set
(X2 . Y) + (- X) is complex set
((X2 . Y) - X) + X1 is complex set
(X2 . Y) - (X - X1) is complex set
(X2 . Y) + (- (X - X1)) is complex set
X is complex set
X1 is complex set
X + X1 is complex set

- X is complex set

- X1 is complex set
(- X1) + (X2 - X) is Relation-like Function-like complex-valued set

- (X + X1) is complex set
(- (X + X1)) + X2 is Relation-like Function-like complex-valued set
dom ((X2 - X) - X1) is set
dom (X2 - X) is set
dom X2 is set
dom (X2 - (X + X1)) is set
Y is set
((X2 - X) - X1) . Y is complex set
(X2 - (X + X1)) . Y is complex set
(X2 - X) . Y is complex set
((X2 - X) . Y) - X1 is complex set
((X2 - X) . Y) + (- X1) is complex set
X2 . Y is complex set
(X2 . Y) - X is complex set
(X2 . Y) + (- X) is complex set
((X2 . Y) - X) - X1 is complex set
((X2 . Y) - X) + (- X1) is complex set
(X2 . Y) - (X + X1) is complex set
(X2 . Y) + (- (X + X1)) is complex set
X is complex set
X1 is complex set
X * X1 is complex set

dom (X1 (#) (X (#) X2)) is set
dom (X (#) X2) is set
dom X2 is set
dom ((X * X1) (#) X2) is set
Y is set
(X1 (#) (X (#) X2)) . Y is complex set
((X * X1) (#) X2) . Y is complex set
(X (#) X2) . Y is complex set
((X (#) X2) . Y) * X1 is complex set
X2 . Y is complex set
(X2 . Y) * X is complex set
((X2 . Y) * X) * X1 is complex set
(X2 . Y) * (X * X1) is complex set

- 1 is non empty complex V37() real integer rational set

(- 1) (#) (X + X1) is Relation-like Function-like complex-valued set

dom (- (X + X1)) is set
dom (X + X1) is set
dom X is set
dom X1 is set
(dom X) /\ (dom X1) is set
dom ((- X) - X1) is set
dom (- X) is set
(dom (- X)) /\ (dom X1) is set
X2 is set
(- (X + X1)) . X2 is complex set
((- X) - X1) . X2 is complex set
(X + X1) . X2 is complex set
- ((X + X1) . X2) is complex set
X . X2 is complex set
X1 . X2 is complex set
(X . X2) + (X1 . X2) is complex set
- ((X . X2) + (X1 . X2)) is complex set
- (X . X2) is complex set
(- (X . X2)) - (X1 . X2) is complex set
- (X1 . X2) is complex set
(- (X . X2)) + (- (X1 . X2)) is complex set
(- X) . X2 is complex set
((- X) . X2) - (X1 . X2) is complex set
((- X) . X2) + (- (X1 . X2)) is complex set

- 1 is non empty complex V37() real integer rational set

(- 1) (#) (X1 - X) is Relation-like Function-like complex-valued set
dom (- (X1 - X)) is set
dom (X1 - X) is set
dom (X - X1) is set
dom X is set
dom X1 is set
(dom X) /\ (dom X1) is set
X2 is set
(X - X1) . X2 is complex set
(- (X1 - X)) . X2 is complex set
X . X2 is complex set
X1 . X2 is complex set
(X . X2) - (X1 . X2) is complex set
- (X1 . X2) is complex set
(X . X2) + (- (X1 . X2)) is complex set
(X1 . X2) - (X . X2) is complex set
- (X . X2) is complex set
(X1 . X2) + (- (X . X2)) is complex set
- ((X1 . X2) - (X . X2)) is complex set
(X1 - X) . X2 is complex set
- ((X1 - X) . X2) is complex set

(X (#) X1) (#) (X2 ") is Relation-like Function-like complex-valued set

dom (X (#) (X1 /" X2)) is set
dom X is set
dom (X1 /" X2) is set
(dom X) /\ (dom (X1 /" X2)) is set
dom ((X (#) X1) /" X2) is set
dom (X (#) X1) is set
dom X2 is set
(dom (X (#) X1)) /\ (dom X2) is set
dom X1 is set
(dom X) /\ (dom X1) is set
(dom X1) /\ (dom X2) is set
Y is set
((X (#) X1) /" X2) . Y is complex set
(X (#) (X1 /" X2)) . Y is complex set
(X (#) X1) . Y is complex set
X2 . Y is complex set
((X (#) X1) . Y) / (X2 . Y) is complex set
(X2 . Y) " is complex set
((X (#) X1) . Y) * ((X2 . Y) ") is complex set
X . Y is complex set
X1 . Y is complex set
(X . Y) * (X1 . Y) is complex set
((X . Y) * (X1 . Y)) / (X2 . Y) is complex set
((X . Y) * (X1 . Y)) * ((X2 . Y) ") is complex set
(X1 . Y) / (X2 . Y) is complex set
(X1 . Y) * ((X2 . Y) ") is complex set
(X . Y) * ((X1 . Y) / (X2 . Y)) is complex set
(X1 /" X2) . Y is complex set
(X . Y) * ((X1 /" X2) . Y) is complex set

(X (#) X2) (#) (X1 ") is Relation-like Function-like complex-valued set
dom ((X /" X1) (#) X2) is set
dom (X /" X1) is set
dom X2 is set
(dom (X /" X1)) /\ (dom X2) is set
dom ((X (#) X2) /" X1) is set
dom (X (#) X2) is set
dom X1 is set
(dom (X (#) X2)) /\ (dom X1) is set
dom X is set
(dom X) /\ (dom X1) is set
(dom X) /\ (dom X2) is set
Y is set
((X /" X1) (#) X2) . Y is complex set
((X (#) X2) /" X1) . Y is complex set
(X /" X1) . Y is complex set
X2 . Y is complex set
((X /" X1) . Y) * (X2 . Y) is complex set
X . Y is complex set
X1 . Y is complex set
(X . Y) / (X1 . Y) is complex set
(X1 . Y) " is complex set
(X . Y) * ((X1 . Y) ") is complex set
((X . Y) / (X1 . Y)) * (X2 . Y) is complex set
(X . Y) * (X2 . Y) is complex set
((X . Y) * (X2 . Y)) / (X1 . Y) is complex set
((X . Y) * (X2 . Y)) * ((X1 . Y) ") is complex set
(X (#) X2) . Y is complex set
((X (#) X2) . Y) / (X1 . Y) is complex set
((X (#) X2) . Y) * ((X1 . Y) ") is complex set

(X /" X1) (#) (X2 ") is Relation-like Function-like complex-valued set

X (#) ((X1 (#) X2) ") is Relation-like Function-like complex-valued set
dom ((X /" X1) /" X2) is set
dom (X /" X1) is set
dom X2 is set
(dom (X /" X1)) /\ (dom X2) is set
dom (X /" (X1 (#) X2)) is set
dom X is set
dom (X1 (#) X2) is set
(dom X) /\ (dom (X1 (#) X2)) is set
dom X1 is set
(dom X) /\ (dom X1) is set
(dom X1) /\ (dom X2) is set
Y is set
((X /" X1) /" X2) . Y is complex set
(X /" (X1 (#) X2)) . Y is complex set
(X /" X1) . Y is complex set
X2 . Y is complex set
((X /" X1) . Y) / (X2 . Y) is complex set
(X2 . Y) " is complex set
((X /" X1) . Y) * ((X2 . Y) ") is complex set
X . Y is complex set
X1 . Y is complex set
(X . Y) / (X1 . Y) is complex set
(X1 . Y) " is complex set
(X . Y) * ((X1 . Y) ") is complex set
((X . Y) / (X1 . Y)) / (X2 . Y) is complex set
((X . Y) / (X1 . Y)) * ((X2 . Y) ") is complex set
(X1 . Y) * (X2 . Y) is complex set
(X . Y) / ((X1 . Y) * (X2 . Y)) is complex set
((X1 . Y) * (X2 . Y)) " is complex set
(X . Y) * (((X1 . Y) * (X2 . Y)) ") is complex set
(X1 (#) X2) . Y is complex set
(X . Y) / ((X1 (#) X2) . Y) is complex set
((X1 (#) X2) . Y) " is complex set
(X . Y) * (((X1 (#) X2) . Y) ") is complex set
X is complex set
- X is complex set

- 1 is non empty complex V37() real integer rational set

dom (X (#) (- X1)) is set
dom (- X1) is set
dom X1 is set
dom ((- X) (#) X1) is set
X2 is set
(X (#) (- X1)) . X2 is complex set
((- X) (#) X1) . X2 is complex set
(- X1) . X2 is complex set
X * ((- X1) . X2) is complex set
X1 . X2 is complex set
- (X1 . X2) is complex set
X * (- (X1 . X2)) is complex set
(- X) * (X1 . X2) is complex set
X is complex set

- 1 is non empty complex V37() real integer rational set

(- 1) (#) (X (#) X1) is Relation-like Function-like complex-valued set
dom (- (X (#) X1)) is set
dom (X (#) X1) is set
dom X1 is set
dom (X (#) (- X1)) is set
dom (- X1) is set
X2 is set
(X (#) (- X1)) . X2 is complex set
(- (X (#) X1)) . X2 is complex set
(- X1) . X2 is complex set
X * ((- X1) . X2) is complex set
X1 . X2 is complex set
- (X1 . X2) is complex set
X * (- (X1 . X2)) is complex set
X * (X1 . X2) is complex set
- (X * (X1 . X2)) is complex set
(X (#) X1) . X2 is complex set
- ((X (#) X1) . X2) is complex set
X is complex set
- X is complex set

- 1 is non empty complex V37() real integer rational set
(- 1) (#) (X (#) X1) is Relation-like Function-like complex-valued set

- 1 is non empty complex V37() real integer rational set

(- 1) (#) (X (#) X1) is Relation-like Function-like complex-valued set

dom (- (X (#) X1)) is set
dom (X (#) X1) is set
dom X is set
dom X1 is set
(dom X) /\ (dom X1) is set
dom ((- X) (#) X1) is set
dom (- X) is set
(dom (- X)) /\ (dom X1) is set
X2 is set
(- (X (#) X1)) . X2 is complex set
((- X) (#) X1) . X2 is complex set
(X (#) X1) . X2 is complex set
- ((X (#) X1) . X2) is complex set
X . X2 is complex set
X1 . X2 is complex set
(X . X2) * (X1 . X2) is complex set
- ((X . X2) * (X1 . X2)) is complex set
- (X . X2) is complex set
(- (X . X2)) * (X1 . X2) is complex set
(- X) . X2 is complex set
((- X) . X2) * (X1 . X2) is complex set

- 1 is non empty complex V37() real integer rational set

(- 1) (#) (X /" X1) is Relation-like Function-like complex-valued set

dom (- (X /" X1)) is set
dom (X /" X1) is set
dom X is set
dom X1 is set
(dom X) /\ (dom X1) is set
dom ((- X) /" X1) is set
dom (- X) is set
(dom (- X)) /\ (dom X1) is set
X2 is set
(- (X /" X1)) . X2 is complex set
((- X) /" X1) . X2 is complex set
(X /" X1) . X2 is complex set
- ((X /" X1) . X2) is complex set
X . X2 is complex set
X1 . X2 is complex set
(X . X2) / (X1 . X2) is complex set
(X1 . X2) " is complex set
(X . X2) * ((X1 . X2) ") is complex set
- ((X . X2) / (X1 . X2)) is complex set
- (X . X2) is complex set
(- (X . X2)) / (X1 . X2) is complex set
(- (X . X2)) * ((X1 . X2) ") is complex set
(- X) . X2 is complex set
((- X) . X2) / (X1 . X2) is complex set
((- X) . X2) * ((X1 . X2) ") is complex set

- 1 is non empty complex V37() real integer rational set
(- 1) (#) (X /" X1) is Relation-like Function-like complex-valued set

dom (- X1) is set
dom X1 is set
dom (X /" X1) is set
dom X is set
(dom X) /\ (dom X1) is set
dom (X /" (- X1)) is set
(dom X) /\ (dom (- X1)) is set
dom (- (X /" X1)) is set
X2 is set
(- (X /" X1)) . X2 is complex set
(X /" (- X1)) . X2 is complex set
(X /" X1) . X2 is complex set
- ((X /" X1) . X2) is complex set
X . X2 is complex set
X1 . X2 is complex set
(X . X2) / (X1 . X2) is complex set
(X1 . X2) " is complex set
(X . X2) * ((X1 . X2) ") is complex set
- ((X . X2) / (X1 . X2)) is complex set
- (X1 . X2) is complex set
(X . X2) / (- (X1 . X2)) is complex set
(- (X1 . X2)) " is complex set
(X . X2) * ((- (X1 . X2)) ") is complex set
(- X1) . X2 is complex set
(X . X2) / ((- X1) . X2) is complex set
((- X1) . X2) " is complex set
(X . X2) * (((- X1) . X2) ") is complex set

X1 is complex set
1 / X1 is complex set
X1 " is complex set
1 * (X1 ") is complex set

X1 is complex set
(X,X1) is Relation-like Function-like set
1 / X1 is complex set
X1 " is complex set
1 * (X1 ") is complex set

X1 is complex V37() real set

1 / X1 is complex V37() real set
X1 " is complex V37() real set
1 * (X1 ") is complex V37() real set

1 / X1 is complex V37() real rational set

1 * (X1 ") is complex V37() real rational set

X1 is complex set

1 / X1 is complex set
X1 " is complex set
1 * (X1 ") is complex set

X is complex set

1 / X is complex set
X " is complex set
1 * (X ") is complex set

dom (X1,X) is set
dom X1 is set

X1 is complex set

1 / X1 is complex set
X1 " is complex set
1 * (X1 ") is complex set

X is set
(X2,X1) . X is complex set
X2 . X is complex set
(X2 . X) / X1 is complex set
(X2 . X) * (X1 ") is complex set
X is complex set

- 1 is non empty complex V37() real integer rational set

((- X1),X) is Relation-like Function-like complex-valued set
1 / X is complex set
X " is complex set
1 * (X ") is complex set
(1 / X) (#) (- X1) is Relation-like Function-like complex-valued set

(- 1) (#) (X1,X) is Relation-like Function-like complex-valued set
- (1 / X) is complex set
(- (1 / X)) (#) X1 is Relation-like Function-like complex-valued set
X is complex set
- X is complex set

(X1,(- X)) is Relation-like Function-like complex-valued set
1 / (- X) is complex set
(- X) " is complex set
1 * ((- X) ") is complex set
(1 / (- X)) (#) X1 is Relation-like Function-like complex-valued set

1 / X is complex set
X " is complex set
1 * (X ") is complex set

- 1 is non empty complex V37() real integer rational set
(- 1) (#) (X1,X) is Relation-like Function-like complex-valued set
- (1 / X) is complex set
(- (1 / X)) (#) X1 is Relation-like Function-like complex-valued set
X is complex set
- X is complex set

(X1,(- X)) is Relation-like Function-like complex-valued set
1 / (- X) is complex set
(- X) " is complex set
1 * ((- X) ") is complex set
(1 / (- X)) (#) X1 is Relation-like Function-like complex-valued set

- 1 is non empty complex V37() real integer rational set

((- X1),X) is Relation-like Function-like complex-valued set
1 / X is complex set
X " is complex set
1 * (X ") is complex set
(1 / X) (#) (- X1) is Relation-like Function-like complex-valued set

(- 1) (#) (X1,X) is Relation-like Function-like complex-valued set
X is complex set
X1 is complex set

1 / X is complex set
X " is complex set
1 * (X ") is complex set

1 / X1 is complex set
X1 " is complex set
1 * (X1 ") is complex set

dom X2 is set
Y is set
X2 . Y is complex set

(X2,X) . Y is complex set
(X2 . Y) / X is complex set
(X2 . Y) * (X ") is complex set
(X2,X1) . Y is complex set
(X2 . Y) / X1 is complex set
(X2 . Y) * (X1 ") is complex set
X is complex set
X1 is complex set
X / X1 is complex set
X1 " is complex set
X * (X1 ") is complex set

((X (#) X2),X1) is Relation-like Function-like complex-valued set
1 / X1 is complex set
1 * (X1 ") is complex set
(1 / X1) (#) (X (#) X2) is Relation-like Function-like complex-valued set

dom (X (#) X2) is set
dom X2 is set
dom ((X (#) X2),X1) is set
dom ((X / X1) (#) X2) is set
Y is set
((X (#) X2),X1) . Y is complex set
((X / X1) (#) X2) . Y is complex set
(X (#) X2) . Y is complex set
((X (#) X2) . Y) * (X1 ") is complex set
X2 . Y is complex set
(X2 . Y) * X is complex set
((X2 . Y) * X) * (X1 ") is complex set
(X2 . Y) * (X / X1) is complex set
X is complex set
X1 is complex set

1 / X is complex set
X " is complex set
1 * (X ") is complex set

((X1 (#) X2),X) is Relation-like Function-like complex-valued set
(1 / X) (#) (X1 (#) X2) is Relation-like Function-like complex-valued set
dom (X1 (#) (X2,X)) is set
dom (X2,X) is set
dom X2 is set
dom (X1 (#) X2) is set
dom ((X1 (#) X2),X) is set
Y is set
(X1 (#) (X2,X)) . Y is complex set
((X1 (#) X2),X) . Y is complex set
(X2,X) . Y is complex set
((X2,X) . Y) * X1 is complex set
X2 . Y is complex set
(X2 . Y) * (X ") is complex set
((X2 . Y) * (X ")) * X1 is complex set
(X2 . Y) * X1 is complex set
((X2 . Y) * X1) * (X ") is complex set
(X1 (#) X2) . Y is complex set
((X1 (#) X2) . Y) * (X ") is complex set
X is complex set
X1 is complex set
X * X1 is complex set

1 / X is complex set
X " is complex set
1 * (X ") is complex set

((X2,X),X1) is Relation-like Function-like complex-valued set
1 / X1 is complex set
X1 " is complex set
1 * (X1 ") is complex set
(1 / X1) (#) (X2,X) is Relation-like Function-like complex-valued set
(X2,(X * X1)) is Relation-like Function-like complex-valued set
1 / (X * X1) is complex set
(X * X1) " is complex set
1 * ((X * X1) ") is complex set
(1 / (X * X1)) (#) X2 is Relation-like Function-like complex-valued set
dom (X2,X) is set
dom X2 is set
dom (X2,(X * X1)) is set
dom ((X2,X),X1) is set
Y is set
((X2,X),X1) . Y is complex set
(X2,(X * X1)) . Y is complex set
(X2,X) . Y is complex set
((X2,X) . Y) * (X1 ") is complex set
X2 . Y is complex set
(X2 . Y) * (X ") is complex set
((X2 . Y) * (X ")) * (X1 ") is complex set
(X ") * (X1 ") is complex set
(X2 . Y) * ((X ") * (X1 ")) is complex set
(X2 . Y) * ((X * X1) ") is complex set
X is complex set

1 / X is complex set
X " is complex set
1 * (X ") is complex set

((X1 + X2),X) is Relation-like Function-like complex-valued set
(1 / X) (#) (X1 + X2) is Relation-like Function-like complex-valued set

(X1,X) + (X2,X) is Relation-like Function-like complex-valued set
dom ((X1 + X2),X) is set
dom (X1 + X2) is set
dom X1 is set
dom X2 is set
(dom X1) /\ (dom X2) is set
dom (X1,X) is set
dom (X2,X) is set
dom ((X1,X) + (X2,X)) is set
Y is set
((X1 + X2),X) . Y is complex set
((X1,X) + (X2,X)) . Y is complex set
(X1 + X2) . Y is complex set
((X1 + X2) . Y) * (X ") is complex set
X1 . Y is complex set
X2 . Y is complex set
(X1 . Y) + (X2 . Y) is complex set
((X1 . Y) + (X2 . Y)) * (X ") is complex set
(X1 . Y) * (X ") is complex set
(X2 . Y) * (X ") is complex set
((X1 . Y) * (X ")) + ((X2 . Y) * (X ")) is complex set
(X1,X) . Y is complex set
((X1,X) . Y) + ((X2 . Y) * (X ")) is complex set
(X2,X) . Y is complex set
((X1,X) . Y) + ((X2,X) . Y) is complex set
X is complex set

1 / X is complex set
X " is complex set
1 * (X ") is complex set

- 1 is non empty complex V37() real integer rational set

((X1 - X2),X) is Relation-like Function-like complex-valued set
(1 / X) (#) (X1 - X2) is Relation-like Function-like complex-valued set

(X1,X) - (X2,X) is Relation-like Function-like complex-valued set

(- 1) (#) (X2,X) is Relation-like Function-like complex-valued set
(X1,X) + (- (X2,X)) is Relation-like Function-like complex-valued set
dom ((X1 - X2),X) is set
dom (X1 - X2) is set
dom X1 is set
dom X2 is set
(dom X1) /\ (dom X2) is set
dom (X1,X) is set
dom (X2,X) is set
dom ((X1,X) - (X2,X)) is set
Y is set
((X1 - X2),X) . Y is complex set
((X1,X) - (X2,X)) . Y is complex set
(X1 - X2) . Y is complex set
((X1 - X2) . Y) * (X ") is complex set
X1 . Y is complex set
X2 . Y is complex set
(X1 . Y) - (X2 . Y) is complex set
- (X2 . Y) is complex set
(X1 . Y) + (- (X2 . Y)) is complex set
((X1 . Y) - (X2 . Y)) * (X ") is complex set
(X1 . Y) * (X ") is complex set
(X2 . Y) * (X ") is complex set
((X1 . Y) * (X ")) - ((X2 . Y) * (X ")) is complex set
- ((X2 . Y) * (X ")) is complex set
((X1 . Y) * (X ")) + (- ((X2 . Y) * (X "))) is complex set
(X1,X) . Y is complex set
((X1,X) . Y) - ((X2 . Y) * (X ")) is complex set
((X1,X) . Y) + (- ((X2 . Y) * (X "))) is complex set
(X2,X) . Y is complex set
((X1,X) . Y) - ((X2,X) . Y) is complex set
- ((X2,X) . Y) is complex set
((X1,X) . Y) + (- ((X2,X) . Y)) is complex set
X is complex set

((X1 (#) X2),X) is Relation-like Function-like complex-valued set
1 / X is complex set
X " is complex set
1 * (X ") is complex set
(1 / X) (#) (X1 (#) X2) is Relation-like Function-like complex-valued set

dom ((X1 (#) X2),X) is set
dom (