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