:: VALUED_2 semantic presentation

REAL is non empty complex-membered ext-real-membered real-membered V59() V60() set

K235() is set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V37() complex-valued ext-real-valued real-valued natural-valued real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V59() V60() FinSequence-like FinSubsequence-like FinSequence-membered set

NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V59() Element of K19(REAL)

K19(REAL) is set

RAT is non empty complex-membered ext-real-membered real-membered rational-membered V59() V60() set

K226() is set

{{}} is functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

K20({{}},K226()) is Relation-like set

K226() \/ K20({{}},K226()) is set

[{},{}] is set

{{},{}} is functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{{{},{}},{{}}} is non empty set

{[{},{}]} is Relation-like Function-like 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

1 is non empty complex epsilon-transitive epsilon-connected ordinal natural V37() V38() real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

{{},1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

Funcs ({{},1},REAL) is non empty FUNCTION_DOMAIN of {{},1}, REAL

{ b

(Funcs ({{},1},REAL)) \ { b

K19((Funcs ({{},1},REAL))) is set

((Funcs ({{},1},REAL)) \ { b

INT is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered V59() V60() set

omega is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V59() set

K20({{}},omega) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

omega \/ K20({{}},omega) is non empty set

(omega \/ K20({{}},omega)) \ {[{},{}]} is Element of K19((omega \/ K20({{}},omega)))

K19((omega \/ K20({{}},omega))) 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()))

2 is non empty complex epsilon-transitive epsilon-connected ordinal natural V37() V38() real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

3 is non empty complex epsilon-transitive epsilon-connected ordinal natural V37() V38() real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

K100() is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V37() complex-valued ext-real-valued real-valued natural-valued real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V59() V60() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

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 b

union { (dom b

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 Relation-like Function-like complex-valued set

{ff} is functional non empty set

X is set

ff is set

X is set

ff is set

X is set

the Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

{ the Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued 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

K20(X1,COMPLEX) is Relation-like complex-valued 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

K20(X1,COMPLEX) is Relation-like complex-valued 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()} is functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered () 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

K20(X1,ExtREAL) is Relation-like ext-real-valued 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

K20(X1,ExtREAL) is Relation-like ext-real-valued 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

K20(X1,REAL) is Relation-like complex-valued ext-real-valued real-valued 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

K20(X1,REAL) is Relation-like complex-valued ext-real-valued real-valued 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

K20(X1,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued 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

K20(X1,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued 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

K20(X1,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued 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

K20(X1,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued 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

K20(X1,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued 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

K20(X1,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued 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

K20(X,COMPLEX) is Relation-like complex-valued set

K19(K20(X,COMPLEX)) is set

X is set

(X) is set

(X) is set

K19((X)) is set

X1 is set

K20(X,ExtREAL) is Relation-like ext-real-valued set

K19(K20(X,ExtREAL)) is set

X is set

(X) is set

(X) is set

K19((X)) is set

X1 is set

K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(X,REAL)) is set

X is set

(X) is set

(X) is set

K19((X)) is set

X1 is set

K20(X,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(X,RAT)) is set

X is set

(X) is set

(X) is set

K19((X)) is set

X1 is set

K20(X,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(X,INT)) is set

X is set

(X) is set

(X) is set

K19((X)) is set

X1 is set

K20(X,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued 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

X1 is Relation-like Function-like Element of X

X is functional () set

X1 is Relation-like Function-like Element of X

X is functional () () () set

X1 is Relation-like Function-like complex-valued ext-real-valued Element of X

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

X1 is Relation-like Function-like complex-valued ext-real-valued real-valued Element of X

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

X1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued Element of X

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

X1 is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued Element of X

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

Y . X1 is Relation-like Function-like 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

Y . X1 is Relation-like Function-like 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

Y . X1 is Relation-like Function-like 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

Y . X1 is Relation-like Function-like 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

Y . X1 is Relation-like Function-like complex-valued ext-real-valued 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

Y . X1 is Relation-like Function-like complex-valued ext-real-valued real-valued 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

Y . X1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued 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

Y . X1 is Relation-like RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued 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

X1 is complex-membered set

PFuncs (X,X1) is set

X2 is set

Y is Relation-like Function-like 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

X1 is ext-real-membered set

PFuncs (X,X1) is set

X2 is set

Y is Relation-like Function-like 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

Y1 is Relation-like X -defined X1 -valued Function-like ext-real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered rational-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered rational-membered integer-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered set

Funcs (X,X1) is set

X2 is set

Y is Relation-like Function-like 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

X1 is ext-real-membered set

Funcs (X,X1) is set

X2 is set

Y is Relation-like Function-like 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

Y1 is Relation-like X -defined X1 -valued Function-like ext-real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered rational-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered rational-membered integer-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,X1))

X is set

X1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

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

X2 is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

K20(X,X1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(X,X1)) is set

Y1 is Relation-like X -defined X1 -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(X,X1))

X is functional () set

X1 is Relation-like X -valued Function-like set

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

K19(X) is set

X is Relation-like Function-like 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

X is Relation-like set

rng X is set

X1 is set

X is Relation-like set

rng X is set

X1 is set

X is Relation-like set

rng X is set

X1 is set

X is Relation-like set

rng X is set

X1 is set

X is Relation-like set

rng X is set

X1 is set

X is Relation-like 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

X2 . Y is Relation-like Function-like ext-real-valued 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

X2 . Y is Relation-like Function-like complex-valued ext-real-valued real-valued 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

X2 . Y is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued 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

X2 . Y is Relation-like RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued 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

X2 . Y is Relation-like RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

X is Relation-like Function-like () 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

X is Relation-like Function-like () 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

X is Relation-like Function-like () set

X1 is set

X . X1 is Relation-like Function-like 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

X . X1 is Relation-like Function-like 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

X . X1 is Relation-like Function-like complex-valued ext-real-valued 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

X . X1 is Relation-like Function-like complex-valued ext-real-valued real-valued 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

X . X1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued 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

X . X1 is Relation-like RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued 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

X2 is Relation-like Function-like complex-valued set

X + X2 is Relation-like Function-like complex-valued set

X1 + X2 is Relation-like Function-like complex-valued 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

X2 is Relation-like Function-like complex-valued set

X2 - X is Relation-like Function-like complex-valued set

- X is complex set

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

X2 - X1 is Relation-like Function-like complex-valued set

- X1 is complex set

(- X1) + X2 is Relation-like Function-like complex-valued 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

X2 is Relation-like Function-like complex-valued set

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

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

dom X2 is set

Y is set

X2 . Y is complex set

rng X2 is complex-membered 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

X1 is Relation-like Function-like complex-valued set

X + X1 is Relation-like Function-like complex-valued set

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

- X1 is Relation-like Function-like complex-valued set

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

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

- X is complex set

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

X1 is Relation-like Function-like complex-valued set

X1 - X is Relation-like Function-like complex-valued set

- X is complex set

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

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

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

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

- X1 is Relation-like Function-like complex-valued set

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

X + (- X1) 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

X2 is Relation-like Function-like complex-valued set

X + X2 is Relation-like Function-like complex-valued set

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

(X + X1) + X2 is Relation-like Function-like complex-valued 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

X2 is Relation-like Function-like complex-valued set

X + X2 is Relation-like Function-like complex-valued set

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

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

(X - X1) + 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

X2 is Relation-like Function-like complex-valued set

X2 - X is Relation-like Function-like complex-valued set

- X is complex set

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

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

X2 - (X - X1) 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 (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

X2 is Relation-like Function-like complex-valued set

X2 - X is Relation-like Function-like complex-valued set

- X is complex set

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

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

- X1 is complex set

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

X2 - (X + X1) 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

X2 is Relation-like Function-like complex-valued set

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

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

(X * X1) (#) X2 is Relation-like Function-like complex-valued 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 Relation-like Function-like complex-valued set

- X is Relation-like Function-like complex-valued set

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

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

X1 is Relation-like Function-like complex-valued set

X + X1 is Relation-like Function-like complex-valued set

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

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

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

- X1 is Relation-like Function-like complex-valued set

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

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

X is Relation-like Function-like complex-valued set

X1 is Relation-like Function-like complex-valued set

X - X1 is Relation-like Function-like complex-valued set

- X1 is Relation-like Function-like complex-valued set

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

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

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

X1 - X is Relation-like Function-like complex-valued set

- X is Relation-like Function-like complex-valued set

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

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

- (X1 - X) is Relation-like Function-like complex-valued 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 is Relation-like Function-like complex-valued set

X1 is Relation-like Function-like complex-valued set

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

X2 is Relation-like Function-like complex-valued set

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

X2 " is Relation-like Function-like complex-valued set

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

X1 /" X2 is Relation-like Function-like complex-valued set

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 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 is Relation-like Function-like complex-valued set

X1 is Relation-like Function-like complex-valued set

X /" X1 is Relation-like Function-like complex-valued set

X1 " is Relation-like Function-like complex-valued set

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

X2 is Relation-like Function-like complex-valued set

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

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

(X (#) X2) /" X1 is Relation-like Function-like complex-valued 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 is Relation-like Function-like complex-valued set

X1 is Relation-like Function-like complex-valued set

X /" X1 is Relation-like Function-like complex-valued set

X1 " is Relation-like Function-like complex-valued set

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

X2 is Relation-like Function-like complex-valued set

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

X2 " is Relation-like Function-like complex-valued set

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

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

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

(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

X1 is Relation-like Function-like complex-valued set

- X1 is Relation-like Function-like complex-valued set

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

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

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

(- X) (#) X1 is Relation-like Function-like complex-valued 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

X1 is Relation-like Function-like complex-valued set

- X1 is Relation-like Function-like complex-valued set

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

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

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

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

- (X (#) X1) is Relation-like Function-like complex-valued 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

X1 is Relation-like Function-like complex-valued set

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

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

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

- X1 is Relation-like Function-like complex-valued set

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

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

X is Relation-like Function-like complex-valued set

- X is Relation-like Function-like complex-valued set

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

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

X1 is Relation-like Function-like complex-valued set

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

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

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

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

X is Relation-like Function-like complex-valued set

- X is Relation-like Function-like complex-valued set

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

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

X1 is Relation-like Function-like complex-valued set

X /" X1 is Relation-like Function-like complex-valued set

X1 " is Relation-like Function-like complex-valued set

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

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

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

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

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

X is Relation-like Function-like complex-valued set

X1 is Relation-like Function-like complex-valued set

X /" X1 is Relation-like Function-like complex-valued set

X1 " is Relation-like Function-like complex-valued set

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

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

- X1 is Relation-like Function-like complex-valued set

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

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

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

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

X is Relation-like Function-like complex-valued set

X1 is complex set

1 / X1 is complex set

X1 " is complex set

1 * (X1 ") is complex set

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

X is Relation-like Function-like complex-valued 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

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

X is Relation-like Function-like complex-valued ext-real-valued real-valued set

X1 is complex V37() real set

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

1 / X1 is complex V37() real set

X1 " is complex V37() real set

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

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

X is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set

X1 is complex V37() real rational set

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

1 / X1 is complex V37() real rational set

X1 " is complex V37() real rational set

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

(1 / X1) (#) X is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued set

X is Relation-like NAT -defined Function-like complex-valued V60() FinSequence-like FinSubsequence-like set

X1 is complex set

(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) (#) X is Relation-like NAT -defined Function-like complex-valued V60() FinSequence-like FinSubsequence-like set

X1 is Relation-like Function-like complex-valued 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

dom (X1,X) is set

dom X1 is set

X2 is Relation-like Function-like complex-valued set

X1 is complex set

(X2,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 is Relation-like Function-like complex-valued 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

X1 is Relation-like Function-like complex-valued set

- X1 is Relation-like Function-like complex-valued set

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

(- 1) (#) X1 is Relation-like Function-like complex-valued 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

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

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

- (X1,X) 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 is Relation-like Function-like complex-valued 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

(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

- (X1,X) is Relation-like Function-like complex-valued 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 is Relation-like Function-like complex-valued 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

- X1 is Relation-like Function-like complex-valued set

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

(- 1) (#) X1 is Relation-like Function-like complex-valued 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

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

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

- (X1,X) 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

X2 is Relation-like Function-like complex-valued set

(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) (#) X2 is Relation-like Function-like complex-valued set

(X2,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 is Relation-like Function-like complex-valued set

dom X2 is set

Y is set

X2 . Y is complex set

rng X2 is complex-membered 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

X2 is Relation-like Function-like complex-valued set

X (#) X2 is Relation-like Function-like complex-valued 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

(X / X1) (#) 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

X2 is Relation-like Function-like complex-valued set

(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) (#) X2 is Relation-like Function-like complex-valued set

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

X1 (#) X2 is Relation-like Function-like complex-valued 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

X2 is Relation-like Function-like complex-valued set

(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) (#) X2 is Relation-like Function-like complex-valued 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

X1 is Relation-like Function-like complex-valued 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

X2 is Relation-like Function-like complex-valued set

X1 + X2 is Relation-like Function-like complex-valued set

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

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

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

(1 / X) (#) 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

X1 is Relation-like Function-like complex-valued 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

X2 is Relation-like Function-like complex-valued set

X1 - X2 is Relation-like Function-like complex-valued set

- X2 is Relation-like Function-like complex-valued set

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

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

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

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

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

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

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

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

- (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 is Relation-like Function-like complex-valued set

X2 is Relation-like Function-like complex-valued set

X1 (#) X2 is Relation-like Function-like complex-valued 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

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

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

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

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

dom (