:: RFUNCT_1 semantic presentation

REAL is non empty complex-membered ext-real-membered real-membered V51() V52() set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() Element of K19(REAL)

K19(REAL) is set

{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() set

RAT is non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() set

the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() set

1 is non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

{{},1} is non empty set

COMPLEX is non empty complex-membered V51() V52() set

INT is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered V51() V52() set

0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() Element of NAT

0 " is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative complex real complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() set

- 1 is non empty ext-real non positive negative complex real Element of REAL

(- 1) " is non empty ext-real non positive negative complex real Element of REAL

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

dom Y is set

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

dom X is set

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

Y " {0} is set

(dom Y) \ (Y " {0}) is Element of K19((dom Y))

K19((dom Y)) is set

(dom X) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))

C is Relation-like Function-like set

dom C is set

C is Relation-like Function-like set

dom C is set

f1 is Relation-like Function-like set

dom f1 is set

f2 is set

C . f2 is set

X . f2 is complex set

Y . f2 is complex set

(Y . f2) " is complex set

(X . f2) * ((Y . f2) ") is complex set

f1 . f2 is set

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

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

(X,Y) is Relation-like Function-like set

C is set

dom (X,Y) is set

(X,Y) . C is set

X . C is complex set

Y . C is complex set

(Y . C) " is complex set

(X . C) * ((Y . C) ") is complex set

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

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

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

C is set

dom (X,Y) is set

(X,Y) . C is complex set

X . C is ext-real complex real set

Y . C is ext-real complex real set

(Y . C) " is ext-real complex real set

(X . C) * ((Y . C) ") is ext-real complex real set

X is set

Y is complex-membered set

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

K19(K20(X,Y)) is set

C is Relation-like X -defined Y -valued Function-like complex-valued Element of K19(K20(X,Y))

f1 is Relation-like X -defined Y -valued Function-like complex-valued Element of K19(K20(X,Y))

(C,f1) is Relation-like Function-like complex-valued set

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

K19(K20(X,COMPLEX)) is set

rng (C,f1) is complex-membered set

dom (C,f1) is set

dom C is Element of K19(X)

K19(X) is set

dom f1 is Element of K19(X)

f1 " {0} is Element of K19(X)

(dom f1) \ (f1 " {0}) is Element of K19(X)

(dom C) /\ ((dom f1) \ (f1 " {0})) is Element of K19(X)

X is set

Y is complex-membered ext-real-membered real-membered set

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

K19(K20(X,Y)) is set

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

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

(C,f1) is Relation-like Function-like complex-valued ext-real-valued real-valued set

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

K19(K20(X,REAL)) is set

(X,Y,C,f1) is Relation-like X -defined COMPLEX -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,COMPLEX))

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

K19(K20(X,COMPLEX)) is set

rng (X,Y,C,f1) is complex-membered ext-real-membered real-membered Element of K19(COMPLEX)

K19(COMPLEX) is set

dom (X,Y,C,f1) is Element of K19(X)

K19(X) is set

K20((dom (X,Y,C,f1)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20((dom (X,Y,C,f1)),REAL)) is set

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

dom X is set

X " {0} is set

(dom X) \ (X " {0}) is Element of K19((dom X))

K19((dom X)) is set

Y is Relation-like Function-like set

dom Y is set

Y is Relation-like Function-like set

dom Y is set

C is Relation-like Function-like set

dom C is set

f1 is set

Y . f1 is set

X . f1 is complex set

(X . f1) " is complex set

C . f1 is set

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

(X) is Relation-like Function-like set

Y is set

dom (X) is set

(X) . Y is set

X . Y is complex set

(X . Y) " is complex set

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

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

Y is set

dom (X) is set

(X) . Y is complex set

X . Y is ext-real complex real set

(X . Y) " is ext-real complex real set

X is set

Y is complex-membered set

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

K19(K20(X,Y)) is set

C is Relation-like X -defined Y -valued Function-like complex-valued Element of K19(K20(X,Y))

(C) is Relation-like Function-like complex-valued set

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

K19(K20(X,COMPLEX)) is set

rng (C) is complex-membered set

dom (C) is set

dom C is Element of K19(X)

K19(X) is set

C " {0} is Element of K19(X)

(dom C) \ (C " {0}) is Element of K19(X)

X is set

Y is complex-membered ext-real-membered real-membered set

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

K19(K20(X,Y)) is set

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

(C) is Relation-like Function-like complex-valued ext-real-valued real-valued set

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

K19(K20(X,REAL)) is set

(X,Y,C) is Relation-like X -defined COMPLEX -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,COMPLEX))

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

K19(K20(X,COMPLEX)) is set

rng (X,Y,C) is complex-membered ext-real-membered real-membered Element of K19(COMPLEX)

K19(COMPLEX) is set

dom (X,Y,C) is Element of K19(X)

K19(X) is set

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

K19(K20((dom (X,Y,C)),REAL)) is set

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

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

dom (X) is set

dom X is set

X " {0} is set

(dom X) \ (X " {0}) is Element of K19((dom X))

K19((dom X)) is set

(dom X) /\ ((dom X) \ (X " {0})) is Element of K19((dom X))

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

dom X is set

X " {0} is set

(dom X) \ (X " {0}) is Element of K19((dom X))

K19((dom X)) is set

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

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

dom (X (#) Y) is set

(X (#) Y) " {0} is set

(dom (X (#) Y)) \ ((X (#) Y) " {0}) is Element of K19((dom (X (#) Y)))

K19((dom (X (#) Y))) is set

dom Y is set

Y " {0} is set

(dom Y) \ (Y " {0}) is Element of K19((dom Y))

K19((dom Y)) is set

((dom X) \ (X " {0})) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))

C is set

(X (#) Y) . C is complex set

X . C is complex set

Y . C is complex set

(X . C) * (Y . C) is complex set

(dom X) /\ (dom Y) is set

C is set

Y . C is complex set

X . C is complex set

(X . C) * (Y . C) is complex set

(X (#) Y) . C is complex set

(dom X) /\ (dom Y) is set

X is non empty set

Y is Element of X

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

(C) is Relation-like Function-like complex-valued set

dom (C) is set

C . Y is complex set

dom C is set

C " {0} is set

(dom C) \ (C " {0}) is Element of K19((dom C))

K19((dom C)) is set

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

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

(X) " {0} is set

the Element of (X) " {0} is Element of (X) " {0}

dom (X) is set

dom X is set

X " {0} is set

(dom X) \ (X " {0}) is Element of K19((dom X))

K19((dom X)) is set

X . the Element of (X) " {0} is complex set

(X) . the Element of (X) " {0} is complex set

(X . the Element of (X) " {0}) " is complex set

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

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

|.X.| " {0} is set

X " {0} is set

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

- 1 is non empty ext-real non positive negative complex real set

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

(- X) " {0} is set

Y is set

|.X.| . Y is ext-real complex real set

X . Y is complex set

abs (X . Y) is ext-real complex real Element of REAL

dom |.X.| is set

dom X is set

X . Y is complex set

abs (X . Y) is ext-real complex real Element of REAL

|.X.| . Y is ext-real complex real set

dom X is set

dom |.X.| is set

Y is set

(- X) . Y is complex set

X . Y is complex set

- (X . Y) is complex set

- (- (X . Y)) is complex set

- 0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative complex real complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() Element of REAL

dom (- X) is set

X . Y is complex set

(- X) . Y is complex set

- 0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative complex real complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() Element of REAL

dom (- X) is set

X 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

dom ((X)) is set

dom (X) is set

X | (dom (X)) is Relation-like Function-like complex-valued set

dom (X | (dom (X))) is set

dom X is set

X " {0} is set

(dom X) \ (X " {0}) is Element of K19((dom X))

K19((dom X)) is set

(X) " {0} is set

(dom (X)) \ ((X) " {0}) is Element of K19((dom (X)))

K19((dom (X))) is set

(dom (X)) \ {} is Element of K19((dom (X)))

(dom X) /\ (dom (X)) is set

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

X " {0} is set

Y is complex set

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

(Y (#) X) " {0} is set

C is set

dom (Y (#) X) is set

(Y (#) X) . C is complex set

X . C is complex set

Y * (X . C) is complex set

dom X is set

X . C is complex set

Y * (X . C) is complex set

dom X is set

dom (Y (#) X) is set

(Y (#) X) . C is complex set

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

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

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

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

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

Y + C is Relation-like Function-like complex-valued set

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

dom ((X + Y) + C) is set

dom (X + Y) is set

dom C is set

(dom (X + Y)) /\ (dom C) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

((dom X) /\ (dom Y)) /\ (dom C) is set

(dom Y) /\ (dom C) is set

(dom X) /\ ((dom Y) /\ (dom C)) is set

dom (Y + C) is set

(dom X) /\ (dom (Y + C)) is set

dom (X + (Y + C)) is set

f1 is set

((X + Y) + C) . f1 is complex set

(X + Y) . f1 is complex set

C . f1 is complex set

((X + Y) . f1) + (C . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) + (Y . f1) is complex set

((X . f1) + (Y . f1)) + (C . f1) is complex set

(Y . f1) + (C . f1) is complex set

(X . f1) + ((Y . f1) + (C . f1)) is complex set

(Y + C) . f1 is complex set

(X . f1) + ((Y + C) . f1) is complex set

(X + (Y + C)) . f1 is complex set

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

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

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

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

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

Y (#) C is Relation-like Function-like complex-valued set

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

f1 is set

dom ((X (#) Y) (#) C) is set

((X (#) Y) (#) C) . f1 is complex set

(X (#) Y) . f1 is complex set

C . f1 is complex set

((X (#) Y) . f1) * (C . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) * (Y . f1) is complex set

((X . f1) * (Y . f1)) * (C . f1) is complex set

(Y . f1) * (C . f1) is complex set

(X . f1) * ((Y . f1) * (C . f1)) is complex set

(Y (#) C) . f1 is complex set

(X . f1) * ((Y (#) C) . f1) is complex set

(X (#) (Y (#) C)) . f1 is complex set

dom (X (#) Y) is set

dom C is set

(dom (X (#) Y)) /\ (dom C) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

((dom X) /\ (dom Y)) /\ (dom C) is set

(dom Y) /\ (dom C) is set

(dom X) /\ ((dom Y) /\ (dom C)) is set

dom (Y (#) C) is set

(dom X) /\ (dom (Y (#) C)) is set

dom (X (#) (Y (#) C)) is set

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

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

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

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

(X + Y) (#) C is Relation-like Function-like complex-valued set

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

Y (#) C is Relation-like Function-like complex-valued set

(X (#) C) + (Y (#) C) is Relation-like Function-like complex-valued set

dom ((X + Y) (#) C) is set

dom (X + Y) is set

dom C is set

(dom (X + Y)) /\ (dom C) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

(dom C) /\ (dom C) is set

((dom X) /\ (dom Y)) /\ ((dom C) /\ (dom C)) is set

((dom X) /\ (dom Y)) /\ (dom C) is set

(((dom X) /\ (dom Y)) /\ (dom C)) /\ (dom C) is set

(dom X) /\ (dom C) is set

((dom X) /\ (dom C)) /\ (dom Y) is set

(((dom X) /\ (dom C)) /\ (dom Y)) /\ (dom C) is set

(dom Y) /\ (dom C) is set

((dom X) /\ (dom C)) /\ ((dom Y) /\ (dom C)) is set

dom (X (#) C) is set

(dom (X (#) C)) /\ ((dom Y) /\ (dom C)) is set

dom (Y (#) C) is set

(dom (X (#) C)) /\ (dom (Y (#) C)) is set

dom ((X (#) C) + (Y (#) C)) is set

f1 is set

((X + Y) (#) C) . f1 is complex set

(X + Y) . f1 is complex set

C . f1 is complex set

((X + Y) . f1) * (C . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) + (Y . f1) is complex set

((X . f1) + (Y . f1)) * (C . f1) is complex set

(X . f1) * (C . f1) is complex set

(Y . f1) * (C . f1) is complex set

((X . f1) * (C . f1)) + ((Y . f1) * (C . f1)) is complex set

(X (#) C) . f1 is complex set

((X (#) C) . f1) + ((Y . f1) * (C . f1)) is complex set

(Y (#) C) . f1 is complex set

((X (#) C) . f1) + ((Y (#) C) . f1) is complex set

((X (#) C) + (Y (#) C)) . f1 is complex set

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

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

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

Y + C is Relation-like Function-like complex-valued set

X (#) (Y + C) is Relation-like Function-like complex-valued set

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

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

(X (#) Y) + (X (#) C) is Relation-like Function-like complex-valued set

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

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

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

C is complex set

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

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

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

dom (C (#) (X (#) Y)) is set

dom (X (#) Y) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

dom (C (#) X) is set

(dom (C (#) X)) /\ (dom Y) is set

dom ((C (#) X) (#) Y) is set

f1 is set

(C (#) (X (#) Y)) . f1 is complex set

(X (#) Y) . f1 is complex set

C * ((X (#) Y) . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) * (Y . f1) is complex set

C * ((X . f1) * (Y . f1)) is complex set

C * (X . f1) is complex set

(C * (X . f1)) * (Y . f1) is complex set

(C (#) X) . f1 is complex set

((C (#) X) . f1) * (Y . f1) is complex set

((C (#) X) (#) Y) . f1 is complex set

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

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

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

C is complex set

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

C (#) Y is Relation-like Function-like complex-valued set

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

dom (C (#) (X (#) Y)) is set

dom (X (#) Y) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

dom (C (#) Y) is set

(dom X) /\ (dom (C (#) Y)) is set

dom (X (#) (C (#) Y)) is set

f1 is set

(C (#) (X (#) Y)) . f1 is complex set

(X (#) Y) . f1 is complex set

C * ((X (#) Y) . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) * (Y . f1) is complex set

C * ((X . f1) * (Y . f1)) is complex set

C * (Y . f1) is complex set

(X . f1) * (C * (Y . f1)) is complex set

(C (#) Y) . f1 is complex set

(X . f1) * ((C (#) Y) . f1) is complex set

(X (#) (C (#) Y)) . f1 is complex set

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

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

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

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

- 1 is non empty ext-real non positive negative complex real set

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

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

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

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

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

Y (#) C is Relation-like Function-like complex-valued set

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

- (Y (#) C) is Relation-like Function-like complex-valued set

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

(X (#) C) + (- (Y (#) C)) is Relation-like Function-like complex-valued set

dom ((X - Y) (#) C) is set

dom (X - Y) is set

dom C is set

(dom (X - Y)) /\ (dom C) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

(dom C) /\ (dom C) is set

((dom X) /\ (dom Y)) /\ ((dom C) /\ (dom C)) is set

((dom X) /\ (dom Y)) /\ (dom C) is set

(((dom X) /\ (dom Y)) /\ (dom C)) /\ (dom C) is set

(dom X) /\ (dom C) is set

((dom X) /\ (dom C)) /\ (dom Y) is set

(((dom X) /\ (dom C)) /\ (dom Y)) /\ (dom C) is set

(dom Y) /\ (dom C) is set

((dom X) /\ (dom C)) /\ ((dom Y) /\ (dom C)) is set

dom (X (#) C) is set

(dom (X (#) C)) /\ ((dom Y) /\ (dom C)) is set

dom (Y (#) C) is set

(dom (X (#) C)) /\ (dom (Y (#) C)) is set

dom ((X (#) C) - (Y (#) C)) is set

f1 is set

((X - Y) (#) C) . f1 is complex set

(X - Y) . f1 is complex set

C . f1 is complex set

((X - Y) . f1) * (C . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) - (Y . f1) is complex set

((X . f1) - (Y . f1)) * (C . f1) is complex set

(X . f1) * (C . f1) is complex set

(Y . f1) * (C . f1) is complex set

((X . f1) * (C . f1)) - ((Y . f1) * (C . f1)) is complex set

(X (#) C) . f1 is complex set

((X (#) C) . f1) - ((Y . f1) * (C . f1)) is complex set

(Y (#) C) . f1 is complex set

((X (#) C) . f1) - ((Y (#) C) . f1) is complex set

((X (#) C) - (Y (#) C)) . f1 is complex set

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

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

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

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

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

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

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

- 1 is non empty ext-real non positive negative complex real set

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

(X (#) Y) + (- (X (#) C)) is Relation-like Function-like complex-valued set

Y - C is Relation-like Function-like complex-valued set

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

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

Y + (- C) is Relation-like Function-like complex-valued set

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

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

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

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

C is complex set

C (#) (X + Y) is Relation-like Function-like complex-valued set

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

C (#) Y is Relation-like Function-like complex-valued set

(C (#) X) + (C (#) Y) is Relation-like Function-like complex-valued set

dom (C (#) (X + Y)) is set

dom (X + Y) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

dom (C (#) Y) is set

(dom X) /\ (dom (C (#) Y)) is set

dom (C (#) X) is set

(dom (C (#) X)) /\ (dom (C (#) Y)) is set

dom ((C (#) X) + (C (#) Y)) is set

f1 is set

(C (#) (X + Y)) . f1 is complex set

(X + Y) . f1 is complex set

C * ((X + Y) . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) + (Y . f1) is complex set

C * ((X . f1) + (Y . f1)) is complex set

C * (X . f1) is complex set

C * (Y . f1) is complex set

(C * (X . f1)) + (C * (Y . f1)) is complex set

(C (#) X) . f1 is complex set

((C (#) X) . f1) + (C * (Y . f1)) is complex set

(C (#) Y) . f1 is complex set

((C (#) X) . f1) + ((C (#) Y) . f1) is complex set

((C (#) X) + (C (#) Y)) . f1 is complex set

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

Y is complex set

C is complex set

Y * C is complex set

(Y * C) (#) X is Relation-like Function-like complex-valued set

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

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

dom ((Y * C) (#) X) is set

dom X is set

dom (C (#) X) is set

dom (Y (#) (C (#) X)) is set

f1 is set

((Y * C) (#) X) . f1 is complex set

X . f1 is complex set

(Y * C) * (X . f1) is complex set

C * (X . f1) is complex set

Y * (C * (X . f1)) is complex set

(C (#) X) . f1 is complex set

Y * ((C (#) X) . f1) is complex set

(Y (#) (C (#) X)) . f1 is complex set

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

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

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

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

- 1 is non empty ext-real non positive negative complex real set

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

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

C is complex set

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

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

C (#) Y is Relation-like Function-like complex-valued set

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

- (C (#) Y) is Relation-like Function-like complex-valued set

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

(C (#) X) + (- (C (#) Y)) is Relation-like Function-like complex-valued set

dom (C (#) (X - Y)) is set

dom (X - Y) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

dom (C (#) Y) is set

(dom X) /\ (dom (C (#) Y)) is set

dom (C (#) X) is set

(dom (C (#) X)) /\ (dom (C (#) Y)) is set

dom ((C (#) X) - (C (#) Y)) is set

f1 is set

(C (#) (X - Y)) . f1 is complex set

(X - Y) . f1 is complex set

C * ((X - Y) . f1) is complex set

X . f1 is complex set

Y . f1 is complex set

(X . f1) - (Y . f1) is complex set

C * ((X . f1) - (Y . f1)) is complex set

C * (X . f1) is complex set

C * (Y . f1) is complex set

(C * (X . f1)) - (C * (Y . f1)) is complex set

(C (#) X) . f1 is complex set

((C (#) X) . f1) - (C * (Y . f1)) is complex set

(C (#) Y) . f1 is complex set

((C (#) X) . f1) - ((C (#) Y) . f1) is complex set

((C (#) X) - (C (#) Y)) . f1 is complex set

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

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

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

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

- 1 is non empty ext-real non positive negative complex real set

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

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

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

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

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

dom (X - Y) is set

dom Y is set

dom X is set

(dom Y) /\ (dom X) is set

dom (Y - X) is set

dom ((- 1) (#) (Y - X)) is set

C is set

(X - Y) . C is complex set

X . C is complex set

Y . C is complex set

(X . C) - (Y . C) is complex set

(Y . C) - (X . C) is complex set

(- 1) * ((Y . C) - (X . C)) is complex set

(Y - X) . C is complex set

(- 1) * ((Y - X) . C) is complex set

((- 1) (#) (Y - X)) . C is complex set

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

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

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

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

- 1 is non empty ext-real non positive negative complex real set

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

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

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

Y + C is Relation-like Function-like complex-valued set

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

- (Y + C) is Relation-like Function-like complex-valued set

(- 1) (#) (Y + C) is Relation-like Function-like complex-valued set

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

(X - Y) - C is Relation-like Function-like complex-valued set

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

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

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

dom (X - (Y + C)) is set

dom X is set

dom (Y + C) is set

(dom X) /\ (dom (Y + C)) is set

dom Y is set

dom C is set

(dom Y) /\ (dom C) is set

(dom X) /\ ((dom Y) /\ (dom C)) is set

(dom X) /\ (dom Y) is set

((dom X) /\ (dom Y)) /\ (dom C) is set

dom (X - Y) is set

(dom (X - Y)) /\ (dom C) is set

dom ((X - Y) - C) is set

f1 is set

(X - (Y + C)) . f1 is complex set

X . f1 is complex set

(Y + C) . f1 is complex set

(X . f1) - ((Y + C) . f1) is complex set

Y . f1 is complex set

C . f1 is complex set

(Y . f1) + (C . f1) is complex set

(X . f1) - ((Y . f1) + (C . f1)) is complex set

(X . f1) - (Y . f1) is complex set

((X . f1) - (Y . f1)) - (C . f1) is complex set

(X - Y) . f1 is complex set

((X - Y) . f1) - (C . f1) is complex set

((X - Y) - C) . f1 is complex set

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

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

Y is set

dom (1 (#) X) is set

(1 (#) X) . Y is complex set

X . Y is complex set

1 * (X . Y) is complex set

dom X is set

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

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

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

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

- 1 is non empty ext-real non positive negative complex real set

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

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

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

Y - C is Relation-like Function-like complex-valued set

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

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

Y + (- C) is Relation-like Function-like complex-valued set

X - (Y - C) is Relation-like Function-like complex-valued set

- (Y - C) is Relation-like Function-like complex-valued set

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

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

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

dom (X - (Y - C)) is set

dom X is set

dom (Y - C) is set

(dom X) /\ (dom (Y - C)) is set

dom Y is set

dom C is set

(dom Y) /\ (dom C) is set

(dom X) /\ ((dom Y) /\ (dom C)) is set

(dom X) /\ (dom Y) is set

((dom X) /\ (dom Y)) /\ (dom C) is set

dom (X - Y) is set

(dom (X - Y)) /\ (dom C) is set

dom ((X - Y) + C) is set

f1 is set

(X - (Y - C)) . f1 is complex set

X . f1 is complex set

(Y - C) . f1 is complex set

(X . f1) - ((Y - C) . f1) is complex set

Y . f1 is complex set

C . f1 is complex set

(Y . f1) - (C . f1) is complex set

(X . f1) - ((Y . f1) - (C . f1)) is complex set

(X . f1) - (Y . f1) is complex set

((X . f1) - (Y . f1)) + (C . f1) is complex set

(X - Y) . f1 is complex set

((X - Y) . f1) + (C . f1) is complex set

((X - Y) + C) . f1 is complex set

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

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

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

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

Y - C is Relation-like Function-like complex-valued set

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

- 1 is non empty ext-real non positive negative complex real set

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

Y + (- C) is Relation-like Function-like complex-valued set

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

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

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

dom (X + (Y - C)) is set

dom X is set

dom (Y - C) is set

(dom X) /\ (dom (Y - C)) is set

dom Y is set

dom C is set

(dom Y) /\ (dom C) is set

(dom X) /\ ((dom Y) /\ (dom C)) is set

(dom X) /\ (dom Y) is set

((dom X) /\ (dom Y)) /\ (dom C) is set

dom (X + Y) is set

(dom (X + Y)) /\ (dom C) is set

dom ((X + Y) - C) is set

f1 is set

(X + (Y - C)) . f1 is complex set

X . f1 is complex set

(Y - C) . f1 is complex set

(X . f1) + ((Y - C) . f1) is complex set

Y . f1 is complex set

C . f1 is complex set

(Y . f1) - (C . f1) is complex set

(X . f1) + ((Y . f1) - (C . f1)) is complex set

(X . f1) + (Y . f1) is complex set

((X . f1) + (Y . f1)) - (C . f1) is complex set

(X + Y) . f1 is complex set

((X + Y) . f1) - (C . f1) is complex set

((X + Y) - C) . f1 is complex set

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

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

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

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

|.(X (#) Y).| is Relation-like Function-like complex-valued ext-real-valued real-valued set

|.Y.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

|.X.| (#) |.Y.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

C is set

dom |.(X (#) Y).| is set

|.(X (#) Y).| . C is ext-real complex real set

(X (#) Y) . C is complex set

abs ((X (#) Y) . C) is ext-real complex real Element of REAL

X . C is complex set

Y . C is complex set

(X . C) * (Y . C) is complex set

abs ((X . C) * (Y . C)) is ext-real complex real Element of REAL

abs (X . C) is ext-real complex real Element of REAL

abs (Y . C) is ext-real complex real Element of REAL

(abs (X . C)) * (abs (Y . C)) is ext-real complex real Element of REAL

|.X.| . C is ext-real complex real set

(|.X.| . C) * (abs (Y . C)) is ext-real complex real Element of REAL

|.Y.| . C is ext-real complex real set

(|.X.| . C) * (|.Y.| . C) is ext-real complex real set

(|.X.| (#) |.Y.|) . C is ext-real complex real set

dom (X (#) Y) is set

dom X is set

dom Y is set

(dom X) /\ (dom Y) is set

dom |.Y.| is set

(dom X) /\ (dom |.Y.|) is set

dom |.X.| is set

(dom |.X.|) /\ (dom |.Y.|) is set

dom (|.X.| (#) |.Y.|) is set

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

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

Y is complex set

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

|.(Y (#) X).| is Relation-like Function-like complex-valued ext-real-valued real-valued set

abs Y is ext-real complex real Element of REAL

(abs Y) (#) |.X.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom |.(Y (#) X).| is set

dom (Y (#) X) is set

dom X is set

dom |.X.| is set

dom ((abs Y) (#) |.X.|) is set

C is set

|.(Y (#) X).| . C is ext-real complex real set

(Y (#) X) . C is complex set

abs ((Y (#) X) . C) is ext-real complex real Element of REAL

X . C is complex set

Y * (X . C) is complex set

abs (Y * (X . C)) is ext-real complex real Element of REAL

abs (X . C) is ext-real complex real Element of REAL

(abs Y) * (abs (X . C)) is ext-real complex real Element of REAL

|.X.| . C is ext-real complex real set

(abs Y) * (|.X.| . C) is ext-real complex real Element of REAL

((abs Y) (#) |.X.|) . C is ext-real complex real set

X 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

dom (X) is set

X | (dom (X)) is Relation-like Function-like complex-valued set

dom ((X)) is set

dom (X | (dom (X))) is set

Y is set

dom X is set

(dom X) /\ (dom (X)) is set

((X)) . Y is complex set

(X) . Y is complex set

((X) . Y) " is complex set

X . Y is complex set

(X . Y) " is complex set

((X . Y) ") " is complex set

(X | (dom (X))) . Y is complex set

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

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

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

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

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

(Y) is Relation-like Function-like complex-valued set

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

dom ((X (#) Y)) is set

dom (X (#) Y) is set

(X (#) Y) " {0} is set

(dom (X (#) Y)) \ ((X (#) Y) " {0}) is Element of K19((dom (X (#) Y)))

K19((dom (X (#) Y))) is set

dom Y is set

dom X is set

X " {0} is set

(dom X) \ (X " {0}) is Element of K19((dom X))

K19((dom X)) is set

Y " {0} is set

(dom Y) \ (Y " {0}) is Element of K19((dom Y))

K19((dom Y)) is set

((dom X) \ (X " {0})) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))

dom (X) is set

(dom (X)) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))

dom (Y) is set

(dom (X)) /\ (dom (Y)) is set

dom ((X) (#) (Y)) is set

C is set

((X (#) Y)) . C is complex set

(X (#) Y) . C is complex set

((X (#) Y) . C) " is complex set

X . C is complex set

Y . C is complex set

(X . C) * (Y . C) is complex set

((X . C) * (Y . C)) " is complex set

(X . C) " is complex set

(Y . C) " is complex set

((X . C) ") * ((Y . C) ") is complex set

(X) . C is complex set

((X) . C) * ((Y . C) ") is complex set

(Y) . C is complex set

((X) . C) * ((Y) . C) is complex set

((X) (#) (Y)) . C is complex set

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

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

Y is complex set

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

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

Y " is complex set

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

dom ((Y (#) X)) is set

dom (Y (#) X) is set

(Y (#) X) " {0} is set

(dom (Y (#) X)) \ ((Y (#) X) " {0}) is Element of K19((dom (Y (#) X)))

K19((dom (Y (#) X))) is set

X " {0} is set

(dom (Y (#) X)) \ (X " {0}) is Element of K19((dom (Y (#) X)))

dom X is set

(dom X) \ (X " {0}) is Element of K19((dom X))

K19((dom X)) is set

dom (X) is set

dom ((Y ") (#) (X)) is set

C is set

((Y (#) X)) . C is complex set

(Y (#) X) . C is complex set

((Y (#) X) . C) " is complex set

X . C is complex set

Y * (X . C) is complex set

(Y * (X . C)) " is complex set

(X . C) " is complex set

(Y ") * ((X . C) ") is complex set

(X) . C is complex set

(Y ") * ((X) . C) is complex set

((Y ") (#) (X)) . C 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 ext-real non positive negative complex real set

(- 1) (#) X 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) (#) (X) 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 ext-real-valued real-valued set

(|.X.|) is Relation-like Function-like complex-valued ext-real-valued real-valued set

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

|.(X).| is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom (|.X.|) is set

dom |.X.| is set

|.X.| " {0} is set

(dom |.X.|) \ (|.X.| " {0}) is Element of K19((dom |.X.|))

K19((dom |.X.|)) is set

dom X is set

(dom X) \ (|.X.| " {0}) is Element of K19((dom X))

K19((dom X)) is set

X " {0} is set

(dom X) \ (X " {0}) is Element of K19((dom X))

dom (X) is set

dom |.(X).| is set

Y is set

(|.X.|) . Y is ext-real complex real set

|.X.| . Y is ext-real complex real set

(|.X.| . Y) " is ext-real complex real set

X . Y is complex set

abs (X . Y) is ext-real complex real Element of REAL

(abs (X . Y)) " is ext-real complex real Element of REAL

1 / (abs (X . Y)) is ext-real complex real Element of REAL

1 / (X . Y) is complex Element of COMPLEX

abs (1 / (X . Y)) is ext-real complex real Element of REAL

(X . Y) " is complex set

abs ((X . Y) ") is ext-real complex real Element of REAL

(X) . Y is complex set

abs ((X) . Y) is ext-real complex real Element of REAL

|.(X).| . Y is ext-real complex real set

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

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

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

(Y) is Relation-like Function-like complex-valued set

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

C is set

dom (X,Y) is set

dom Y is set

dom X is set

Y " {0} is set

(dom Y) \ (Y " {0}) is Element of K19((dom Y))

K19((dom Y)) is set

(dom X) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))

dom (Y) is set

(dom X) /\ (dom (Y)) is set

(X,Y) . C is complex set

X . C is complex set

Y . C is complex set

(Y . C) " is complex set

(X . C) * ((Y . C) ") is complex set

(Y) . C is complex set

(X . C) * ((Y) . C) is complex set

(X (#) (Y)) . C is complex set

dom (X (#) (Y)) is set

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

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

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

C is complex set

C (#) (X,Y) is Relation-like Function-like complex-valued set

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

((C (#) X),Y) is Relation-like Function-like complex-valued set

(Y) is Relation-like Function-like complex-valued set

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

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

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

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

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

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

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

(Y) is Relation-like Function-like complex-valued set

dom (Y) is set

X | (dom (Y)) is Relation-like Function-like complex-valued set

dom ((X,Y) (#) Y) is set

dom (X,Y) is set

dom Y is set

(dom (X,Y)) /\ (dom Y) is set

dom X is set

Y " {0} is set

(dom Y) \ (Y " {0}) is Element of K19((dom Y))

K19((dom Y)) is set

(dom X) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))

((dom X) /\ ((dom Y) \ (Y " {0}))) /\ (dom Y) is Element of K19((dom Y))

((dom Y) \ (Y " {0})) /\ (dom Y) is Element of K19((dom Y))

(dom X) /\ (((dom Y) \ (Y " {0})) /\ (dom Y)) is Element of K19((dom Y))

(dom (Y)) /\ (dom Y) is set

(dom X) /\ ((dom (Y)) /\ (dom Y)) is set

(dom X) /\ (dom (Y)) is set

dom (X | (dom (Y))) is set

C is set

Y . C is complex set

((X,Y) (#) Y) . C is complex set

(X,Y) . C is complex set

((X,Y) . C) * (Y . C) is complex set

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

(X (#) (Y)) . C is complex set

((X (#) (Y)) . C) * (Y . C) is complex set

X . C is complex set

(Y) . C is complex set

(X . C) * ((Y) . C) is complex set

((X . C) * ((Y) . C)) * (Y . C) is complex set

(Y . C) " is complex set

(X . C) * ((Y . C) ") is complex set

((X . C) * ((Y . C) ")) * (Y . C) is complex set

((Y . C) ") * (Y . C) is complex set

(X . C) * (((Y . C) ") * (Y . C)) is complex set

(X . C) * 1 is complex set

(X | (dom (Y))) . C is complex set

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

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

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

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

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

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

(C,f1) is Relation-like Function-like complex-valued set

(X,Y) (#) (C,f1) is Relation-like Function-like complex-valued set

Y (#) f1 is Relation-like Function-like complex-valued set

((X (#) C),(Y (#) f1)) is Relation-like Function-like complex-valued set

f2 is set

dom ((X,Y) (#) (C,f1)) is set

((X,Y) (#) (C,f1)) . f2 is complex set

(X,Y) . f2 is complex set

(C,f1) . f2 is complex set

((X,Y) . f2) * ((C,f1) . f2) is complex set

(Y) is Relation-like Function-like complex-valued set

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

(X (#) (Y)) . f2 is complex set

((X (#) (Y)) . f2) * ((C,f1) . f2) is complex set

(f1) is Relation-like Function-like complex-valued set

C (#) (f1) is Relation-like Function-like complex-valued set

(C (#) (f1)) . f2 is complex set

((X (#) (Y)) . f2) * ((C (#) (f1)) . f2) is complex set

X . f2 is complex set

(Y) . f2 is complex set

(X . f2) * ((Y) . f2) is complex set

((X . f2) * ((Y) . f2)) * ((C (#) (f1)) . f2) is complex set

C . f2 is complex set

(f1) . f2 is complex set

(C . f2) * ((f1) . f2) is complex set

((X . f2) * ((Y) . f2)) * ((C . f2) * ((f1) . f2)) is complex set

((Y) . f2) * ((f1) . f2) is complex set

(C . f2) * (((Y) . f2) * ((f1) . f2)) is complex set

(X . f2) * ((C . f2) * (((Y) . f2) * ((f1) . f2))) is complex set

(Y) (#) (f1) is Relation-like Function-like complex-valued set

((Y) (#) (f1)) . f2 is complex set

(C . f2) * (((Y) (#) (f1)) . f2) is complex set

(X . f2) * ((C . f2) * (((Y) (#) (f1)) . f2)) is complex set

(X . f2) * (C . f2) is complex set

((X . f2) * (C . f2)) * (((Y) (#) (f1)) . f2) is complex set

((Y (#) f1)) is Relation-like Function-like complex-valued set

((Y (#) f1)) . f2 is complex set

((X . f2) * (C . f2)) * (((Y (#) f1)) . f2) is complex set

(X (#) C) . f2 is complex set

((X (#) C) . f2) * (((Y (#) f1)) . f2) is complex set

(X (#) C) (#) ((Y (#) f1)) is Relation-like Function-like complex-valued set

((X (#) C) (#) ((Y (#) f1))) . f2 is complex set

((X (#) C),(Y (#) f1)) . f2 is complex set

dom (X,Y) is set

dom (C,f1) is set

(dom (X,Y)) /\ (dom (C,f1)) is set

dom Y is set

dom X is set

Y " {0} is set

(dom Y) \ (Y " {0}) is Element of K19((dom Y))

K19((dom Y)) is set

(dom X) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))

((dom X) /\ ((dom Y) \ (Y " {0}))) /\ (dom (C,f1)) is Element of K19((dom Y))

dom f1 is set

dom C is set

f1 " {0} is set

(dom f1) \ (f1 " {0}) is Element of K19((dom f1))

K19((dom f1)) is set

(dom C) /\ ((dom f1) \ (f1 " {0})) is Element of K19((dom f1))

((dom X) /\ ((dom Y) \ (Y " {0}))) /\ ((dom C) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))

((dom Y) \ (Y " {0})) /\ ((dom C) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))

(dom X) /\ (((dom Y) \ (Y " {0})) /\ ((dom C) /\ ((dom f1) \ (f1 " {0})))) is Element of K19((dom f1))

((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0})) is Element of K19((dom f1))

(dom C) /\ (((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))

(dom X) /\ ((dom C) /\ (((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0})))) is Element of K19((dom f1))

(dom X) /\ (dom C) is set

((dom X) /\ (dom C)) /\ (((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))

dom (X (#) C) is set

(dom (X (#) C)) /\ (((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))

dom (Y (#) f1) is set

(Y (#) f1) " {0} is set

(dom (Y (#) f1)) \ ((Y (#) f1) " {0}) is Element of K19((dom (Y (#) f1)))

K19((dom (Y (#) f1))) is set

(dom (X (#) C)) /\ ((dom (Y (#) f1)) \ ((Y (#) f1) " {0})) is Element of K19((dom (Y (#) f1)))

dom ((X (#) C),(Y (#) f1)) is set

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

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

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

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

(Y) is Relation-like Function-like complex-valued set

dom (Y) is set

Y | (dom (Y)) is Relation-like Function-like complex-valued set

((Y | (dom (Y))),X) is Relation-like Function-like complex-valued set

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

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

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

((Y)) is Relation-like Function-like complex-valued set

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

(Y | (dom (Y))) (#) (X) is Relation-like Function-like complex-valued set

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

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

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

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

(Y,C) is Relation-like Function-like complex-valued set

X (#) (Y,C) is Relation-like Function-like complex-valued set

((X (#) Y),C) is Relation-like Function-like complex-valued set

(C) is Relation-like Function-like complex-valued set

Y (#) (C) is Relation-like Function-like complex-valued set

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

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

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

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

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

(Y,C) is Relation-like Function-like complex-valued set

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

(C) is Relation-like Function-like complex-valued set

dom (C) is set

C | (dom (C)) is Relation-like Function-like complex-valued set

X (#) (C | (dom (C))) is Relation-like Function-like complex-valued set

((X (#) (C | (dom (C)))),Y) is Relation-like Function-like complex-valued set

((Y,C)) is Relation-like Function-like complex-valued set

X (#) ((Y,C)) is Relation-like Function-like complex-valued set

((C | (dom (C))),Y) is Relation-like Function-like complex-valued set

X (#) ((C | (dom (C))),Y) 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 ext-real non positive negative complex real set

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

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

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

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

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

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

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

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

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

((- Y)) is Relation-like Function-like complex-valued set

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

(Y) is Relation-like Function-like complex-valued set

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

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

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

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

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

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

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

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

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

(C,Y) is Relation-like Function-like complex-valued set

(X,Y) + (C,Y) is Relation-like Function-like complex-valued set

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

((X + C),Y) is Relation-like Function-like complex-valued set

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

- (C,Y) is Relation-like Function-like complex-valued set

- 1 is non empty ext-real non positive negative complex real set

(- 1) (#) (C,Y) is Relation-like Function-like complex-valued set

(X,Y) + (- (C,Y)) is Relation-like Function-like complex-valued set

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

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

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

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

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

(Y) is Relation-like Function-like complex-valued set

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

(X (#) (Y)) + (C,Y) is Relation-like Function-like complex-valued set

C (#) (Y) is Relation-like Function-like complex-valued set

(X (#) (Y)) + (C (#) (Y)) is Relation-like Function-like complex-valued set

(X + C) (#) (Y) is Relation-like Function-like complex-valued set

(X (#) (Y)) - (C,Y) is Relation-like Function-like complex-valued set

(X (#) (Y)) + (- (C,Y)) is Relation-like Function-like complex-valued set

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

- (C (#) (Y)) is Relation-like Function-like complex-valued set

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

(X (#) (Y)) + (- (C (#) (Y))) is Relation-like Function-like complex-valued set

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

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

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

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

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

C (#) Y is Relation-like Function-like complex-valued set

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

(C,f1) is Relation-like Function-like complex-valued set

(X,Y) + (C,f1) is Relation-like Function-like complex-valued set

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

(X (#) f1) + (C (#) Y) is Relation-like Function-like complex-valued set

Y (#) f1 is Relation-like Function-like complex-valued set

(((X (#) f1) + (C (#) Y)),(Y (#) f1)) is Relation-like Function-like complex-valued set

(f1) is Relation-like Function-like complex-valued set

dom (f1) is set

dom f1 is set

f2 is set

dom ((X,Y) + (C,f1)) is set

dom (X,Y) is set

dom (C,f1) is set

(dom (X,Y)) /\ (dom (C,f1)) is set

(Y) is Relation-like Function-like complex-valued set

dom (Y) is set

dom Y is set

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

dom (X (#) (Y)) is set

(dom (X (#) (Y))) /\ (dom (C,f1)) is set

dom X is set

(dom X) /\ (dom (Y)) is set

Y . f2 is complex set

C (#) (f1) is Relation-like Function-like complex-valued set

dom (C (#) (f1)) is set

(dom (X (#) (Y))) /\ (dom (C (#) (f1))) is set

dom C is set

(dom C) /\ (dom (f1)) is set

f1 . f2 is complex set

(dom C) /\ (dom Y) is set

dom (C (#) Y) is set

(dom X) /\ (dom f1) is set

dom (X (#) f1) is set

(dom (X (#) f1)) /\ (dom (C (#) Y)) is set

dom ((X (#) f1) + (C (#) Y)) is set

(dom (Y)) /\ (dom (f1)) is set

(Y) (#) (f1) is Relation-like Function-like complex-valued set

dom ((Y) (#) (f1)) is set

((Y (#) f1)) is Relation-like Function-like complex-valued set

dom ((Y (#) f1)) is set

(dom ((X (#) f1) + (C (#) Y))) /\ (dom ((Y (#) f1))) is set

((X (#) f1) + (C (#) Y)) (#) ((Y (#) f1)) is Relation-like Function-like complex-valued set

dom (((X (#) f1) + (C (#) Y)) (#) ((Y (#) f1))) is set

dom (((X (#) f1) + (C (#) Y)),(Y (#) f1)) is set

((X,Y) + (C,f1)) . f2 is complex set

(X,Y) . f2 is complex set

(C,f1) . f2 is complex set

((X,Y) . f2) + ((C,f1) . f2) is complex set

X . f2 is complex set

(Y . f2) " is complex set

(X . f2) * ((Y . f2) ") is complex set

((X . f2) * ((Y . f2) ")) + ((C,f1) . f2) is complex set

1 * ((Y . f2) ") is complex set

(X . f2) * (1 * ((Y . f2) ")) is complex set

C . f2 is complex set

(C . f2) * 1 is complex set

(f1 . f2) " is complex set

((C . f2) * 1) * ((f1 . f2) ") is complex set

((X . f2) * (1 * ((Y . f2) "))) + (((C . f2) * 1) * ((f1 . f2) ")) is complex set

(f1 . f2) * ((f1 . f2) ") is complex set

((f1 . f2) * ((f1 . f2) ")) * ((Y . f2) ") is complex set