:: 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
(X . f2) * (((f1 . f2) * ((f1 . f2) ")) * ((Y . f2) ")) is complex set
1 * ((f1 . f2) ") is complex set
(C . f2) * (1 * ((f1 . f2) ")) is complex set
((X . f2) * (((f1 . f2) * ((f1 . f2) ")) * ((Y . f2) "))) + ((C . f2) * (1 * ((f1 . f2) "))) is complex set
((f1 . f2) ") * ((Y . f2) ") is complex set
(f1 . f2) * (((f1 . f2) ") * ((Y . f2) ")) is complex set
(X . f2) * ((f1 . f2) * (((f1 . f2) ") * ((Y . f2) "))) is complex set
(Y . f2) * ((Y . f2) ") is complex set
((Y . f2) * ((Y . f2) ")) * ((f1 . f2) ") is complex set
(C . f2) * (((Y . f2) * ((Y . f2) ")) * ((f1 . f2) ")) is complex set
((X . f2) * ((f1 . f2) * (((f1 . f2) ") * ((Y . f2) ")))) + ((C . f2) * (((Y . f2) * ((Y . f2) ")) * ((f1 . f2) "))) is complex set
(f1 . f2) * (Y . f2) is complex set
((f1 . f2) * (Y . f2)) " is complex set
(f1 . f2) * (((f1 . f2) * (Y . f2)) ") is complex set
(X . f2) * ((f1 . f2) * (((f1 . f2) * (Y . f2)) ")) is complex set
((Y . f2) ") * ((f1 . f2) ") is complex set
(Y . f2) * (((Y . f2) ") * ((f1 . f2) ")) is complex set
(C . f2) * ((Y . f2) * (((Y . f2) ") * ((f1 . f2) "))) is complex set
((X . f2) * ((f1 . f2) * (((f1 . f2) * (Y . f2)) "))) + ((C . f2) * ((Y . f2) * (((Y . f2) ") * ((f1 . f2) ")))) is complex set
(Y . f2) * (f1 . f2) is complex set
((Y . f2) * (f1 . f2)) " is complex set
(f1 . f2) * (((Y . f2) * (f1 . f2)) ") is complex set
(X . f2) * ((f1 . f2) * (((Y . f2) * (f1 . f2)) ")) is complex set
(Y . f2) * (((Y . f2) * (f1 . f2)) ") is complex set
(C . f2) * ((Y . f2) * (((Y . f2) * (f1 . f2)) ")) is complex set
((X . f2) * ((f1 . f2) * (((Y . f2) * (f1 . f2)) "))) + ((C . f2) * ((Y . f2) * (((Y . f2) * (f1 . f2)) "))) is complex set
(Y (#) f1) . f2 is complex set
((Y (#) f1) . f2) " is complex set
(f1 . f2) * (((Y (#) f1) . f2) ") is complex set
(X . f2) * ((f1 . f2) * (((Y (#) f1) . f2) ")) is complex set
((X . f2) * ((f1 . f2) * (((Y (#) f1) . f2) "))) + ((C . f2) * ((Y . f2) * (((Y . f2) * (f1 . f2)) "))) is complex set
(X . f2) * (f1 . f2) is complex set
((X . f2) * (f1 . f2)) * (((Y (#) f1) . f2) ") is complex set
(Y . f2) * (((Y (#) f1) . f2) ") is complex set
(C . f2) * ((Y . f2) * (((Y (#) f1) . f2) ")) is complex set
(((X . f2) * (f1 . f2)) * (((Y (#) f1) . f2) ")) + ((C . f2) * ((Y . f2) * (((Y (#) f1) . f2) "))) is complex set
(X (#) f1) . f2 is complex set
((X (#) f1) . f2) * (((Y (#) f1) . f2) ") is complex set
(C . f2) * (Y . f2) is complex set
((C . f2) * (Y . f2)) * (((Y (#) f1) . f2) ") is complex set
(((X (#) f1) . f2) * (((Y (#) f1) . f2) ")) + (((C . f2) * (Y . f2)) * (((Y (#) f1) . f2) ")) is complex set
(C (#) Y) . f2 is complex set
((C (#) Y) . f2) * (((Y (#) f1) . f2) ") is complex set
(((X (#) f1) . f2) * (((Y (#) f1) . f2) ")) + (((C (#) Y) . f2) * (((Y (#) f1) . f2) ")) is complex set
((X (#) f1) . f2) + ((C (#) Y) . f2) is complex set
(((X (#) f1) . f2) + ((C (#) Y) . f2)) * (((Y (#) f1) . f2) ") is complex set
((X (#) f1) + (C (#) Y)) . f2 is complex set
(((X (#) f1) + (C (#) Y)) . f2) * (((Y (#) f1) . f2) ") is complex set
(((X (#) f1) + (C (#) Y)),(Y (#) f1)) . f2 is complex 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))
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) /\ ((dom Y) \ (Y " {0})) is Element of K19((dom Y))
(dom X) /\ ((dom Y) /\ ((dom Y) \ (Y " {0}))) is Element of K19((dom Y))
((dom X) /\ ((dom Y) /\ ((dom Y) \ (Y " {0})))) /\ ((dom C) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
((dom Y) /\ ((dom Y) \ (Y " {0}))) /\ (dom X) is Element of K19((dom Y))
(dom f1) /\ ((dom f1) \ (f1 " {0})) is Element of K19((dom f1))
((dom f1) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C) is Element of K19((dom f1))
(((dom Y) /\ ((dom Y) \ (Y " {0}))) /\ (dom X)) /\ (((dom f1) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C)) is Element of K19((dom f1))
(dom X) /\ (((dom f1) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C)) is Element of K19((dom f1))
((dom Y) /\ ((dom Y) \ (Y " {0}))) /\ ((dom X) /\ (((dom f1) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C))) is Element of K19((dom f1))
(dom X) /\ ((dom f1) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
((dom X) /\ ((dom f1) /\ ((dom f1) \ (f1 " {0})))) /\ (dom C) is Element of K19((dom f1))
((dom Y) /\ ((dom Y) \ (Y " {0}))) /\ (((dom X) /\ ((dom f1) /\ ((dom f1) \ (f1 " {0})))) /\ (dom C)) is Element of K19((dom f1))
((dom X) /\ (dom f1)) /\ ((dom f1) \ (f1 " {0})) is Element of K19((dom f1))
(((dom X) /\ (dom f1)) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C) is Element of K19((dom f1))
((dom Y) /\ ((dom Y) \ (Y " {0}))) /\ ((((dom X) /\ (dom f1)) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C)) is Element of K19((dom f1))
(dom (X (#) f1)) /\ ((dom f1) \ (f1 " {0})) is Element of K19((dom f1))
((dom (X (#) f1)) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C) is Element of K19((dom f1))
((dom Y) /\ ((dom Y) \ (Y " {0}))) /\ (((dom (X (#) f1)) /\ ((dom f1) \ (f1 " {0}))) /\ (dom C)) is Element of K19((dom f1))
(dom (X (#) f1)) /\ ((dom C) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
((dom Y) /\ ((dom Y) \ (Y " {0}))) /\ ((dom (X (#) f1)) /\ ((dom C) /\ ((dom f1) \ (f1 " {0})))) is Element of K19((dom f1))
((dom Y) \ (Y " {0})) /\ (dom Y) is Element of K19((dom Y))
(((dom Y) \ (Y " {0})) /\ (dom Y)) /\ ((dom C) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
(dom (X (#) f1)) /\ ((((dom Y) \ (Y " {0})) /\ (dom Y)) /\ ((dom C) /\ ((dom f1) \ (f1 " {0})))) is Element of K19((dom f1))
(dom Y) /\ ((dom C) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
((dom Y) \ (Y " {0})) /\ ((dom Y) /\ ((dom C) /\ ((dom f1) \ (f1 " {0})))) is Element of K19((dom f1))
(dom (X (#) f1)) /\ (((dom Y) \ (Y " {0})) /\ ((dom Y) /\ ((dom C) /\ ((dom f1) \ (f1 " {0}))))) is Element of K19((dom f1))
((dom C) /\ (dom Y)) /\ ((dom f1) \ (f1 " {0})) is Element of K19((dom f1))
((dom Y) \ (Y " {0})) /\ (((dom C) /\ (dom Y)) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
(dom (X (#) f1)) /\ (((dom Y) \ (Y " {0})) /\ (((dom C) /\ (dom Y)) /\ ((dom f1) \ (f1 " {0})))) is Element of K19((dom f1))
(dom (C (#) Y)) /\ ((dom f1) \ (f1 " {0})) is Element of K19((dom f1))
((dom Y) \ (Y " {0})) /\ ((dom (C (#) Y)) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
(dom (X (#) f1)) /\ (((dom Y) \ (Y " {0})) /\ ((dom (C (#) Y)) /\ ((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 (#) Y)) /\ (((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
(dom (X (#) f1)) /\ ((dom (C (#) Y)) /\ (((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0})))) is Element of K19((dom f1))
((dom (X (#) f1)) /\ (dom (C (#) Y))) /\ (((dom Y) \ (Y " {0})) /\ ((dom f1) \ (f1 " {0}))) is Element of K19((dom f1))
(dom ((X (#) f1) + (C (#) Y))) /\ (((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 (#) f1) + (C (#) Y))) /\ ((dom (Y (#) f1)) \ ((Y (#) f1) " {0})) is Element of K19((dom (Y (#) f1)))
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
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
(f1) is Relation-like Function-like complex-valued set
dom (f1) is set
f1 | (dom (f1)) is Relation-like Function-like complex-valued set
X (#) (f1 | (dom (f1))) is Relation-like Function-like complex-valued set
((X (#) (f1 | (dom (f1)))),(Y (#) C)) 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
((f1 | (dom (f1))),C) is Relation-like Function-like complex-valued set
(X,Y) (#) ((f1 | (dom (f1))),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 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
- (C,f1) is Relation-like Function-like complex-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) (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
- (C (#) Y) is Relation-like Function-like complex-valued set
(- 1) (#) (C (#) Y) 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
(- 1) (#) C is Relation-like Function-like complex-valued set
(((- 1) (#) C),f1) is Relation-like Function-like complex-valued set
(X,Y) + (((- 1) (#) C),f1) is Relation-like Function-like complex-valued set
((- 1) (#) C) (#) Y is Relation-like Function-like complex-valued set
(X (#) f1) + (((- 1) (#) C) (#) Y) is Relation-like Function-like complex-valued set
(((X (#) f1) + (((- 1) (#) C) (#) Y)),(Y (#) f1)) 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
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
(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
(|.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
X is set
Y is Relation-like Function-like complex-valued set
Y | X 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
(Y + C) | X is Relation-like Function-like complex-valued set
C | X is Relation-like Function-like complex-valued set
(Y | X) + (C | X) is Relation-like Function-like complex-valued set
(Y | X) + C is Relation-like Function-like complex-valued set
Y + (C | X) is Relation-like Function-like complex-valued set
f1 is set
dom ((Y + C) | X) is set
dom (Y + C) is set
(dom (Y + C)) /\ X is set
dom Y is set
dom C is set
(dom Y) /\ (dom C) is set
(dom C) /\ X is set
dom (C | X) is set
(dom Y) /\ X is set
dom (Y | X) is set
(dom (Y | X)) /\ (dom (C | X)) is set
dom ((Y | X) + (C | X)) is set
((Y + C) | X) . f1 is complex set
(Y + C) . f1 is complex set
Y . f1 is complex set
C . f1 is complex set
(Y . f1) + (C . f1) is complex set
(Y | X) . f1 is complex set
((Y | X) . f1) + (C . f1) is complex set
(C | X) . f1 is complex set
((Y | X) . f1) + ((C | X) . f1) is complex set
((Y | X) + (C | X)) . f1 is complex set
X /\ X is set
((dom Y) /\ (dom C)) /\ (X /\ X) is set
(dom C) /\ (X /\ X) is set
(dom Y) /\ ((dom C) /\ (X /\ X)) is set
((dom C) /\ X) /\ X is set
(dom Y) /\ (((dom C) /\ X) /\ X) is set
X /\ (dom (C | X)) is set
(dom Y) /\ (X /\ (dom (C | X))) is set
((dom Y) /\ X) /\ (dom (C | X)) is set
f1 is set
(dom (Y | X)) /\ (dom C) is set
dom ((Y | X) + C) is set
((Y + C) | X) . f1 is complex set
(Y + C) . f1 is complex set
Y . f1 is complex set
C . f1 is complex set
(Y . f1) + (C . f1) is complex set
(Y | X) . f1 is complex set
((Y | X) . f1) + (C . f1) is complex set
((Y | X) + C) . f1 is complex set
((dom Y) /\ (dom C)) /\ X is set
((dom Y) /\ X) /\ (dom C) is set
f1 is set
(dom Y) /\ (dom (C | X)) is set
dom (Y + (C | X)) is set
((Y + C) | X) . f1 is complex set
(Y + C) . f1 is complex set
Y . f1 is complex set
C . f1 is complex set
(Y . f1) + (C . f1) is complex set
(C | X) . f1 is complex set
(Y . f1) + ((C | X) . f1) is complex set
(Y + (C | X)) . f1 is complex set
(dom Y) /\ ((dom C) /\ X) is set
X is set
Y is Relation-like Function-like complex-valued set
Y | X 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
(Y (#) C) | X is Relation-like Function-like complex-valued set
C | X is Relation-like Function-like complex-valued set
(Y | X) (#) (C | X) is Relation-like Function-like complex-valued set
(Y | X) (#) C is Relation-like Function-like complex-valued set
Y (#) (C | X) is Relation-like Function-like complex-valued set
f1 is set
dom ((Y (#) C) | X) is set
dom (Y (#) C) is set
(dom (Y (#) C)) /\ X is set
dom Y is set
dom C is set
(dom Y) /\ (dom C) is set
(dom Y) /\ X is set
dom (Y | X) is set
(dom C) /\ X is set
dom (C | X) is set
((Y (#) C) | X) . f1 is complex set
(Y (#) C) . f1 is complex set
Y . f1 is complex set
C . f1 is complex set
(Y . f1) * (C . f1) is complex set
(Y | X) . f1 is complex set
((Y | X) . f1) * (C . f1) is complex set
(C | X) . f1 is complex set
((Y | X) . f1) * ((C | X) . f1) is complex set
((Y | X) (#) (C | X)) . f1 is complex set
X /\ X is set
((dom Y) /\ (dom C)) /\ (X /\ X) is set
(dom C) /\ (X /\ X) is set
(dom Y) /\ ((dom C) /\ (X /\ X)) is set
((dom C) /\ X) /\ X is set
(dom Y) /\ (((dom C) /\ X) /\ X) is set
X /\ (dom (C | X)) is set
(dom Y) /\ (X /\ (dom (C | X))) is set
((dom Y) /\ X) /\ (dom (C | X)) is set
(dom (Y | X)) /\ (dom (C | X)) is set
dom ((Y | X) (#) (C | X)) is set
f1 is set
((Y (#) C) | X) . f1 is complex set
(Y (#) C) . f1 is complex set
Y . f1 is complex set
C . f1 is complex set
(Y . f1) * (C . f1) is complex set
(Y | X) . f1 is complex set
((Y | X) . f1) * (C . f1) is complex set
((Y | X) (#) C) . f1 is complex set
((dom Y) /\ (dom C)) /\ X is set
((dom Y) /\ X) /\ (dom C) is set
(dom (Y | X)) /\ (dom C) is set
dom ((Y | X) (#) C) is set
f1 is set
((Y (#) C) | X) . f1 is complex set
(Y (#) C) . f1 is complex set
Y . f1 is complex set
C . f1 is complex set
(Y . f1) * (C . f1) is complex set
(C | X) . f1 is complex set
(Y . f1) * ((C | X) . f1) is complex set
(Y (#) (C | X)) . f1 is complex set
(dom Y) /\ ((dom C) /\ X) is set
(dom Y) /\ (dom (C | X)) is set
dom (Y (#) (C | X)) is set
X is set
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
(- Y) | X is Relation-like Function-like complex-valued set
Y | 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
(Y) is Relation-like Function-like complex-valued set
(Y) | X is Relation-like Function-like complex-valued set
((Y | X)) is Relation-like Function-like complex-valued set
|.Y.| is Relation-like Function-like complex-valued ext-real-valued real-valued set
|.Y.| | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
|.(Y | X).| is Relation-like Function-like complex-valued ext-real-valued real-valued set
C is set
dom ((- Y) | X) is set
dom (- Y) is set
(dom (- Y)) /\ X is set
dom Y is set
(dom Y) /\ X is set
dom (Y | X) is set
((- Y) | X) . C is complex set
(- Y) . C is complex set
Y . C is complex set
- (Y . C) is complex set
(Y | X) . C is complex set
- ((Y | X) . C) is complex set
(- (Y | X)) . C is complex set
dom (- (Y | X)) is set
dom ((Y) | X) is set
dom (Y) is set
(dom (Y)) /\ X is set
Y " {0} is set
(dom Y) \ (Y " {0}) is Element of K19((dom Y))
K19((dom Y)) is set
((dom Y) \ (Y " {0})) /\ X is Element of K19((dom Y))
(Y " {0}) /\ X is set
((dom Y) /\ X) \ ((Y " {0}) /\ X) is Element of K19(((dom Y) /\ X))
K19(((dom Y) /\ X)) is set
X /\ (Y " {0}) is set
(dom (Y | X)) \ (X /\ (Y " {0})) is Element of K19((dom (Y | X)))
K19((dom (Y | X))) is set
(Y | X) " {0} is set
(dom (Y | X)) \ ((Y | X) " {0}) is Element of K19((dom (Y | X)))
dom ((Y | X)) is set
C is set
((Y) | X) . C is complex set
(Y) . C is complex set
Y . C is complex set
(Y . C) " is complex set
(Y | X) . C is complex set
((Y | X) . C) " is complex set
((Y | X)) . C is complex set
dom (|.Y.| | X) is set
dom |.Y.| is set
(dom |.Y.|) /\ X is set
dom |.(Y | X).| is set
C is set
(|.Y.| | X) . C is ext-real complex real set
|.Y.| . C is ext-real complex real set
Y . C is complex set
abs (Y . C) is ext-real complex real Element of REAL
(Y | X) . C is complex set
abs ((Y | X) . C) is ext-real complex real Element of REAL
|.(Y | X).| . C is ext-real complex real set
X is set
Y is Relation-like Function-like complex-valued set
Y | X 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
(Y - C) | X is Relation-like Function-like complex-valued set
C | X is Relation-like Function-like complex-valued set
(Y | X) - (C | X) is Relation-like Function-like complex-valued set
- (C | X) is Relation-like Function-like complex-valued set
(- 1) (#) (C | X) is Relation-like Function-like complex-valued set
(Y | X) + (- (C | X)) is Relation-like Function-like complex-valued set
(Y | X) - C is Relation-like Function-like complex-valued set
(Y | X) + (- C) is Relation-like Function-like complex-valued set
Y - (C | X) is Relation-like Function-like complex-valued set
Y + (- (C | X)) is Relation-like Function-like complex-valued set
(- C) | X is Relation-like Function-like complex-valued set
(Y | X) + ((- C) | X) is Relation-like Function-like complex-valued set
Y + ((- C) | X) is Relation-like Function-like complex-valued set
X is set
Y is Relation-like Function-like complex-valued set
Y | X 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
(Y,C) | X is Relation-like Function-like complex-valued set
C | X is Relation-like Function-like complex-valued set
((Y | X),(C | X)) is Relation-like Function-like complex-valued set
((Y | X),C) is Relation-like Function-like complex-valued set
(Y,(C | X)) 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
(Y (#) (C)) | X is Relation-like Function-like complex-valued set
(C) | X is Relation-like Function-like complex-valued set
(Y | X) (#) ((C) | X) is Relation-like Function-like complex-valued set
((C | X)) is Relation-like Function-like complex-valued set
(Y | X) (#) ((C | X)) is Relation-like Function-like complex-valued set
(Y | X) (#) (C) is Relation-like Function-like complex-valued set
Y (#) ((C) | X) is Relation-like Function-like complex-valued set
Y (#) ((C | X)) is Relation-like Function-like complex-valued set
X is set
Y is Relation-like Function-like complex-valued set
Y | X is Relation-like Function-like complex-valued set
C is complex set
C (#) Y is Relation-like Function-like complex-valued set
(C (#) Y) | X is Relation-like Function-like complex-valued set
C (#) (Y | X) is Relation-like Function-like complex-valued set
f1 is set
dom ((C (#) Y) | X) is set
dom (C (#) Y) is set
(dom (C (#) Y)) /\ X is set
dom Y is set
(dom Y) /\ X is set
dom (Y | X) is set
dom (C (#) (Y | X)) is set
((C (#) Y) | X) . f1 is complex set
(C (#) Y) . f1 is complex set
Y . f1 is complex set
C * (Y . f1) is complex set
(Y | X) . f1 is complex set
C * ((Y | X) . f1) is complex set
(C (#) (Y | X)) . f1 is complex set
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
Y + C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
Y - C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
- C is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) C is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
Y + (- C) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
Y (#) C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
dom (Y + C) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
dom (Y - C) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
dom (Y (#) C) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is ext-real complex real set
C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
Y (#) C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
dom (Y (#) C) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
C is non empty set
K20(C,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(C,REAL)) is set
Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
- Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) Y is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
f1 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
- f1 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(- 1) (#) f1 is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
abs Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
dom (abs Y) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,Y) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
Y " {0} is Element of K19(X)
K19(X) is set
dom (X,REAL,Y) is Element of K19(X)
dom Y is Element of K19(X)
(dom Y) \ (Y " {0}) is Element of K19(X)
(dom Y) \ {} is Element of K19(X)
dom (X,REAL,Y) is Element of K19(X)
dom Y is Element of K19(X)
(dom Y) \ (Y " {0}) is Element of K19(X)
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
C " {0} is Element of K19(X)
K19(X) is set
(X,REAL,Y,C) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,C) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
Y (#) (X,REAL,C) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,C) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
Y (#) (X,REAL,C) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Element of X
C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
C . Y is ext-real complex real set
f1 is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
C + f1 is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(C + f1) . Y is ext-real complex real set
f1 . Y is ext-real complex real set
(C . Y) + (f1 . Y) is ext-real complex real set
C - f1 is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
- f1 is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) f1 is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
C + (- f1) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
(C - f1) . Y is ext-real complex real set
(C . Y) - (f1 . Y) is ext-real complex real set
C (#) f1 is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(C (#) f1) . Y is ext-real complex real set
(C . Y) * (f1 . Y) is ext-real complex real set
dom (C + f1) is Element of K19(X)
K19(X) is set
dom (C - f1) is Element of K19(X)
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Element of X
C is ext-real complex real set
f1 is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
C (#) f1 is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(C (#) f1) . Y is ext-real complex real set
f1 . Y is ext-real complex real set
C * (f1 . Y) is ext-real complex real set
dom (C (#) f1) is Element of K19(X)
K19(X) is set
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
- C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) C is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
Y is Element of X
(- C) . Y is ext-real complex real set
C . Y is ext-real complex real set
- (C . Y) is ext-real complex real set
abs C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(abs C) . Y is ext-real complex real set
abs (C . Y) is ext-real complex real Element of REAL
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Element of X
C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,C) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,C) . Y is ext-real complex real set
C . Y is ext-real complex real set
(C . Y) " is ext-real complex real set
dom (X,REAL,C) is Element of K19(X)
K19(X) is set
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Element of X
C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
C . Y is ext-real complex real set
f1 is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,f1) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,C,f1) is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
(X,REAL,C,f1) . Y is ext-real complex real set
f1 . Y is ext-real complex real set
(f1 . Y) " is ext-real complex real set
(C . Y) * ((f1 . Y) ") is ext-real complex real set
f1 " {0} is Element of K19(X)
K19(X) is set
dom (X,REAL,C,f1) is Element of K19(X)
X is set
Y is set
chi (X,Y) is Relation-like Function-like set
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
C is set
chi (X,Y) is Relation-like Y -defined {{},1} -valued Function-like V18(Y,{{},1}) Element of K19(K20(Y,{{},1}))
K20(Y,{{},1}) is Relation-like set
K19(K20(Y,{{},1})) is set
rng (chi (X,Y)) is Element of K19({{},1})
K19({{},1}) is set
dom (chi (X,Y)) is Element of K19(Y)
K19(Y) is set
Y is set
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
X is set
(X,Y) is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
dom (X,Y) is Element of K19(Y)
K19(Y) is set
C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
X is set
Y is non empty set
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
(X,Y) is Relation-like Y -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
dom C is Element of K19(Y)
K19(Y) is set
f1 is Element of Y
C . f1 is ext-real complex real set
f2 is Element of Y
C . f2 is ext-real complex real set
f1 is set
C . f1 is ext-real complex real set
Y is non empty set
X is set
(X,Y) is Relation-like Y -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
Y is non empty set
f2 is non empty set
C is Element of Y
X is set
(X,Y) is Relation-like Y -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
(X,Y) . C is ext-real complex real set
f1 is set
(f1,f2) is Relation-like f2 -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(f2,REAL))
K20(f2,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f2,REAL)) is set
c is Element of f2
(f1,f2) . c is ext-real complex real set
Y is non empty set
f2 is non empty set
C is Element of Y
X is set
(X,Y) is Relation-like Y -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
(X,Y) . C is ext-real complex real set
f1 is set
(f1,f2) is Relation-like f2 -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(f2,REAL))
K20(f2,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(f2,REAL)) is set
c is Element of f2
(f1,f2) . c is ext-real complex real set
X is set
Y is non empty set
Y \ X is Element of K19(Y)
K19(Y) is set
(X,Y) is Relation-like Y -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
C is Element of Y
(X,Y) . C is ext-real complex real set
X is non empty set
(X,X) is Relation-like X -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Element of X
(X,X) . Y is ext-real complex real set
X is set
Y is non empty set
(X,Y) is Relation-like Y -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
C is Element of Y
(X,Y) . C is ext-real complex real set
dom (X,Y) is Element of K19(Y)
K19(Y) is set
rng (X,Y) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{0,1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
X is set
Y is set
X \/ Y is set
C is non empty set
(X,C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
K20(C,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(C,REAL)) is set
(Y,C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(X,C) + (Y,C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
((X \/ Y),C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
X /\ Y is set
f1 is Element of C
dom ((X,C) + (Y,C)) is Element of K19(C)
K19(C) is set
(Y,C) . f1 is ext-real complex real set
(X,C) . f1 is ext-real complex real set
((X,C) . f1) + ((Y,C) . f1) is ext-real complex real set
((X \/ Y),C) . f1 is ext-real complex real set
(X,C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) + ((Y,C) . f1) is ext-real complex real set
((X \/ Y),C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) + ((Y,C) . f1) is ext-real complex real set
((X \/ Y),C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) + ((Y,C) . f1) is ext-real complex real set
((X \/ Y),C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) + ((Y,C) . f1) is ext-real complex real set
((X \/ Y),C) . f1 is ext-real complex real set
(X,C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) + ((Y,C) . f1) is ext-real complex real set
((X \/ Y),C) . f1 is ext-real complex real set
(X,C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) + ((Y,C) . f1) is ext-real complex real set
((X \/ Y),C) . f1 is ext-real complex real set
((X,C) + (Y,C)) . f1 is ext-real complex real set
dom (X,C) is Element of K19(C)
dom (Y,C) is Element of K19(C)
(dom (X,C)) /\ (dom (Y,C)) is Element of K19(C)
C /\ (dom (Y,C)) is Element of K19(C)
C /\ C is set
dom ((X \/ Y),C) is Element of K19(C)
X is set
Y is set
X /\ Y is set
C is non empty set
(X,C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
K20(C,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(C,REAL)) is set
(Y,C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(X,C) (#) (Y,C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
((X /\ Y),C) is Relation-like C -defined REAL -valued Function-like total complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 is Element of C
dom ((X,C) (#) (Y,C)) is Element of K19(C)
K19(C) is set
(X,C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) * ((Y,C) . f1) is ext-real complex real set
((X /\ Y),C) . f1 is ext-real complex real set
((X /\ Y),C) . f1 is ext-real complex real set
((X /\ Y),C) . f1 is ext-real complex real set
((X /\ Y),C) . f1 is ext-real complex real set
(X,C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) * ((Y,C) . f1) is ext-real complex real set
((X /\ Y),C) . f1 is ext-real complex real set
(X,C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) * ((Y,C) . f1) is ext-real complex real set
((X /\ Y),C) . f1 is ext-real complex real set
(X,C) . f1 is ext-real complex real set
(Y,C) . f1 is ext-real complex real set
((X,C) . f1) * ((Y,C) . f1) is ext-real complex real set
((X /\ Y),C) . f1 is ext-real complex real set
((X,C) (#) (Y,C)) . f1 is ext-real complex real set
dom (X,C) is Element of K19(C)
dom (Y,C) is Element of K19(C)
(dom (X,C)) /\ (dom (Y,C)) is Element of K19(C)
C /\ (dom (Y,C)) is Element of K19(C)
C /\ C is set
dom ((X /\ Y),C) is Element of K19(C)
X is set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom Y is set
X /\ (dom Y) is set
dom (Y | X) is set
C is ext-real complex real set
f1 is set
Y . f1 is ext-real complex real set
(Y | X) . f1 is ext-real complex real set
C is ext-real complex real set
C + 1 is ext-real complex real Element of REAL
f1 is ext-real complex real set
dom (Y | X) is set
f2 is set
K260((Y | X),f2) is ext-real complex real Element of REAL
Y . f2 is ext-real complex real set
(Y | X) . f2 is ext-real complex real set
X is set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom Y is set
X /\ (dom Y) is set
dom (Y | X) is set
C is ext-real complex real set
f1 is set
Y . f1 is ext-real complex real set
(Y | X) . f1 is ext-real complex real set
C is ext-real complex real set
C - 1 is ext-real complex real Element of REAL
f1 is ext-real complex real set
dom (Y | X) is set
f2 is set
K260((Y | X),f2) is ext-real complex real Element of REAL
Y . f2 is ext-real complex real set
(Y | X) . f2 is ext-real complex real set
X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
Y is ext-real complex real set
C is ext-real complex real set
abs Y is ext-real complex real Element of REAL
abs C is ext-real complex real Element of REAL
(abs Y) + (abs C) is ext-real complex real Element of REAL
f1 is ext-real complex real Element of REAL
f2 is set
X . f2 is ext-real complex real set
abs (X . f2) is ext-real complex real Element of REAL
(X . f2) + 0 is ext-real complex real Element of REAL
- (abs C) is ext-real complex real Element of REAL
- (abs Y) is ext-real complex real Element of REAL
(- (abs Y)) + (- (abs C)) is ext-real complex real Element of REAL
0 + (X . f2) is ext-real complex real Element of REAL
- f1 is ext-real complex real Element of REAL
Y is ext-real complex real set
Y + 1 is ext-real complex real Element of REAL
C is set
K260(X,C) is ext-real complex real Element of REAL
X . C is ext-real complex real set
abs (X . C) is ext-real complex real Element of REAL
Y + 1 is ext-real complex real Element of REAL
- (Y + 1) is ext-real complex real Element of REAL
C is set
K260(X,C) is ext-real complex real Element of REAL
X . C is ext-real complex real set
abs (X . C) is ext-real complex real Element of REAL
- (abs (X . C)) is ext-real complex real Element of REAL
X is set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom Y is set
X /\ (dom Y) is set
C is ext-real complex real set
f1 is ext-real complex real set
abs C is ext-real complex real Element of REAL
abs f1 is ext-real complex real Element of REAL
(abs C) + (abs f1) is ext-real complex real Element of REAL
f2 is ext-real complex real Element of REAL
c is set
Y . c is ext-real complex real set
abs (Y . c) is ext-real complex real Element of REAL
- (abs f1) is ext-real complex real Element of REAL
- (abs C) is ext-real complex real Element of REAL
(- (abs C)) + (- (abs f1)) is ext-real complex real Element of REAL
0 + (Y . c) is ext-real complex real Element of REAL
(Y . c) + 0 is ext-real complex real Element of REAL
- f2 is ext-real complex real Element of REAL
C is ext-real complex real set
f1 is set
Y . f1 is ext-real complex real set
abs (Y . f1) is ext-real complex real Element of REAL
- C is ext-real complex real set
- (abs (Y . f1)) is ext-real complex real Element of REAL
f1 is set
Y . f1 is ext-real complex real set
abs (Y . f1) is ext-real complex real Element of REAL
X is set
Y is set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom C is set
Y /\ (dom C) is set
f1 is ext-real complex real set
c is set
X /\ (dom C) is set
C . c is ext-real complex real set
f2 is ext-real complex real set
f2 is ext-real complex real set
dom C is set
Y /\ (dom C) is set
f1 is ext-real complex real set
c is set
X /\ (dom C) is set
f2 is ext-real complex real set
C . c is ext-real complex real set
f2 is ext-real complex real set
X is set
Y is set
X /\ Y is set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom C is set
X /\ (dom C) is set
f1 is ext-real complex real set
f2 is set
(X /\ Y) /\ (dom C) is set
C . f2 is ext-real complex real set
Y /\ (dom C) is set
f2 is ext-real complex real set
c is set
C . c is ext-real complex real set
X is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y is ext-real complex real set
dom X is set
C is set
K260(X,C) is ext-real complex real Element of REAL
Y is ext-real complex real set
dom X is set
C is set
K260(X,C) is ext-real complex real Element of REAL
dom X is set
Y is ext-real complex real set
Y + 1 is ext-real complex real Element of REAL
C is set
K260(X,C) is ext-real complex real Element of REAL
X . C is ext-real complex real set
Y - 1 is ext-real complex real Element of REAL
C is set
K260(X,C) is ext-real complex real Element of REAL
X . C is ext-real complex real set
X is set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom Y is set
Y | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
X /\ (dom Y) is set
dom (Y | X) is set
X is set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
0 (#) Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
(0 (#) Y) | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
C is ext-real complex real Element of REAL
c is set
dom (0 (#) Y) is set
X /\ (dom (0 (#) Y)) is set
Y . c is ext-real complex real set
0 * (Y . c) is ext-real complex real Element of REAL
(0 (#) Y) . c is ext-real complex real set
f2 is ext-real complex real Element of REAL
f2 is ext-real complex real Element of REAL
c is set
Y . c is ext-real complex real set
0 * (Y . c) is ext-real complex real Element of REAL
f2 is ext-real complex real Element of REAL
(0 (#) Y) . c is ext-real complex real set
f2 is ext-real complex real Element of REAL
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above set
Y is set
X | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
C is ext-real complex real set
dom (X | Y) is set
f1 is set
K260((X | Y),f1) is ext-real complex real Element of REAL
X . f1 is ext-real complex real set
f1 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 bounded_below set
Y is set
X | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
C is ext-real complex real set
dom (X | Y) is set
f1 is set
K260((X | Y),f1) is ext-real complex real Element of REAL
X . f1 is ext-real complex real set
f1 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 bounded_above set
Y is ext-real non negative complex real set
Y (#) X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
C is ext-real complex real set
abs C is ext-real complex real Element of REAL
Y * (abs C) is ext-real complex real Element of REAL
(Y * (abs C)) + 1 is ext-real complex real Element of REAL
f2 is set
dom (Y (#) X) is set
X . f2 is ext-real complex real set
Y * (X . f2) is ext-real complex real set
(abs C) * Y is ext-real complex real Element of REAL
(Y (#) X) . f2 is ext-real complex real set
f1 is ext-real complex real Element of REAL
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f2 is ext-real complex real Element of REAL
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
Y is ext-real non negative complex real set
Y (#) X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
C is ext-real complex real set
abs C is ext-real complex real Element of REAL
- (abs C) is ext-real complex real Element of REAL
Y * (- (abs C)) is ext-real complex real Element of REAL
(Y * (- (abs C))) - 1 is ext-real complex real Element of REAL
f2 is set
dom (Y (#) X) is set
X . f2 is ext-real complex real set
(- (abs C)) * Y is ext-real complex real Element of REAL
Y * (X . f2) is ext-real complex real set
(Y (#) X) . f2 is ext-real complex real set
f1 is ext-real complex real Element of REAL
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f2 is ext-real complex real Element of REAL
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above set
Y is ext-real non positive complex real set
Y (#) X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
C is ext-real complex real set
abs C is ext-real complex real Element of REAL
Y * (abs C) is ext-real complex real Element of REAL
(Y * (abs C)) - 1 is ext-real complex real Element of REAL
f2 is set
dom (Y (#) X) is set
X . f2 is ext-real complex real set
Y * (X . f2) is ext-real complex real set
(Y (#) X) . f2 is ext-real complex real set
f1 is ext-real complex real Element of REAL
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f2 is ext-real complex real Element of REAL
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
Y is ext-real non positive complex real set
Y (#) X is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
C is ext-real complex real set
abs C is ext-real complex real Element of REAL
- (abs C) is ext-real complex real Element of REAL
Y * (- (abs C)) is ext-real complex real Element of REAL
(Y * (- (abs C))) + 1 is ext-real complex real Element of REAL
f2 is set
dom (Y (#) X) is set
X . f2 is ext-real complex real set
Y * (X . f2) is ext-real complex real set
(Y (#) X) . f2 is ext-real complex real set
f1 is ext-real complex real Element of REAL
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f2 is ext-real complex real Element of REAL
X is set
Y is ext-real complex real set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y (#) C is Relation-like Function-like complex-valued ext-real-valued real-valued set
(Y (#) C) | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y (#) (C | X) is Relation-like Function-like complex-valued ext-real-valued real-valued set
X is set
Y is ext-real complex real set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y (#) C is Relation-like Function-like complex-valued ext-real-valued real-valued set
(Y (#) C) | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y (#) (C | X) is Relation-like Function-like complex-valued ext-real-valued real-valued set
X is set
Y is ext-real complex real set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y (#) C is Relation-like Function-like complex-valued ext-real-valued real-valued set
(Y (#) C) | 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 ext-real-valued real-valued set
Y is ext-real complex real set
f1 is set
dom |.X.| is set
X . f1 is ext-real complex real set
abs (X . f1) is ext-real complex real Element of REAL
|.X.| . f1 is ext-real complex real set
C is ext-real complex real set
Y is ext-real complex real set
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 bounded_below set
X is set
|.Y.| | X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded set
|.X.| is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
dom X is set
Y is ext-real complex real set
f1 is set
dom |.X.| is set
X . f1 is ext-real complex real set
abs (X . f1) is ext-real complex real Element of REAL
abs (abs (X . f1)) is ext-real complex real Element of REAL
C is ext-real complex real set
|.X.| . f1 is ext-real complex real set
abs (|.X.| . f1) is ext-real complex real Element of REAL
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 is ext-real complex real set
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above set
- X is Relation-like Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
X is set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
Y | 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 bounded_below set
|.Y.| | X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
- Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
(- Y) | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
|.(Y | X).| is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above set
X + Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom Y is set
C is ext-real complex real set
dom X is set
f1 is ext-real complex real set
f1 + C is ext-real complex real set
c is set
dom (X + Y) is set
(dom X) /\ (dom Y) is set
X . c is ext-real complex real set
f2 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 + Y) . c is ext-real complex real set
f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
c is ext-real complex real set
X is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below set
X + Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom Y is set
C is ext-real complex real set
dom X is set
f1 is ext-real complex real set
f1 + C is ext-real complex real set
c is set
dom (X + Y) is set
(dom X) /\ (dom Y) is set
X . 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
f2 is ext-real complex real set
(X + Y) . c is ext-real complex real set
f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
c is ext-real complex real set
X is set
Y is set
X /\ Y is set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
C + f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C + f1) | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C | (X /\ Y)) + (f1 | (X /\ Y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f1 | Y) | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C | (X /\ Y)) + ((f1 | Y) | X) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C | X) | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
((C | X) | Y) + ((f1 | Y) | 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 bounded_above bounded_below bounded set
Y is Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded set
X (#) Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom Y is set
C is ext-real complex real set
dom X is set
f1 is ext-real complex real set
f1 * C is ext-real complex real set
c is set
Y . c is ext-real complex real set
abs (Y . c) is ext-real complex real Element of REAL
dom (X (#) Y) is set
(dom X) /\ (dom Y) is set
X . c is ext-real complex real set
abs (X . c) is ext-real complex real Element of REAL
(abs (X . c)) * (abs (Y . c)) is ext-real complex real Element of REAL
f2 is ext-real complex real set
(X . c) * (Y . c) is ext-real complex real set
abs ((X . c) * (Y . c)) is ext-real complex real Element of REAL
(X (#) Y) . c is ext-real complex real set
abs ((X (#) Y) . c) is ext-real complex real Element of REAL
f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
c is ext-real complex real set
X is set
Y is set
X /\ Y is set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
C (#) f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C (#) f1) | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
C - f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
- f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
C + (- f1) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C - f1) | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 | (X /\ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C | (X /\ Y)) (#) (f1 | (X /\ Y)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(f1 | Y) | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C | (X /\ Y)) (#) ((f1 | Y) | X) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(C | X) | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
((C | X) | Y) (#) ((f1 | Y) | X) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(- f1) | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
X is set
Y is set
X \/ Y is set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | (X \/ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom C is set
X /\ (dom C) is set
f1 is ext-real complex real set
Y /\ (dom C) is set
f2 is ext-real complex real set
abs f1 is ext-real complex real Element of REAL
abs f2 is ext-real complex real Element of REAL
(abs f1) + (abs f2) is ext-real complex real Element of REAL
r2 is set
(X \/ Y) /\ (dom C) is set
C . r2 is ext-real complex real set
(C . r2) + 0 is ext-real complex real Element of REAL
c is ext-real complex real Element of REAL
C . r2 is ext-real complex real set
0 + (C . r2) is ext-real complex real Element of REAL
c is ext-real complex real Element of REAL
C . r2 is ext-real complex real set
c is ext-real complex real Element of REAL
C . r2 is ext-real complex real set
c is ext-real complex real Element of REAL
c is ext-real complex real Element of REAL
X is set
Y is set
X \/ Y is set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | (X \/ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom C is set
X /\ (dom C) is set
f1 is ext-real complex real set
Y /\ (dom C) is set
f2 is ext-real complex real set
abs f1 is ext-real complex real Element of REAL
- (abs f1) is ext-real complex real Element of REAL
abs f2 is ext-real complex real Element of REAL
(- (abs f1)) - (abs f2) is ext-real complex real Element of REAL
r2 is set
(X \/ Y) /\ (dom C) is set
C . r2 is ext-real complex real set
c is ext-real complex real Element of REAL
(C . r2) - 0 is ext-real complex real Element of REAL
C . r2 is ext-real complex real set
- (abs f2) is ext-real complex real Element of REAL
(- (abs f2)) - (abs f1) is ext-real complex real Element of REAL
(C . r2) - 0 is ext-real complex real Element of REAL
c is ext-real complex real Element of REAL
c is ext-real complex real Element of REAL
C . r2 is ext-real complex real set
c is ext-real complex real Element of REAL
C . r2 is ext-real complex real set
c is ext-real complex real Element of REAL
X is set
Y is set
X \/ Y is set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | X is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | Y is Relation-like Function-like complex-valued ext-real-valued real-valued set
C | (X \/ Y) is Relation-like Function-like complex-valued ext-real-valued real-valued set
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Relation-like X -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of K19(K20(X,REAL))
C is Relation-like X -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of K19(K20(X,REAL))
Y + C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of K19(K20(X,REAL))
dom C is Element of K19(X)
K19(X) is set
f1 is ext-real complex real Element of REAL
dom Y is Element of K19(X)
f2 is ext-real complex real Element of REAL
c is Element of X
dom (Y + C) is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
(Y + C) . c is ext-real complex real set
Y . c is ext-real complex real set
C . c is ext-real complex real set
(Y . c) + (C . c) is ext-real complex real set
(Y . c) + f1 is ext-real complex real Element of REAL
f2 + f1 is ext-real complex real Element of REAL
Y - C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
- C is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued bounded_below set
(- 1) (#) C is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded set
Y + (- C) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued bounded_below set
dom C is Element of K19(X)
K19(X) is set
f1 is ext-real complex real Element of REAL
dom Y is Element of K19(X)
f2 is ext-real complex real Element of REAL
c is Element of X
dom (Y - C) is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
(Y - C) . c is ext-real complex real set
Y . c is ext-real complex real set
C . c is ext-real complex real set
(Y . c) - (C . c) is ext-real complex real set
(Y . c) - f1 is ext-real complex real Element of REAL
f2 - f1 is ext-real complex real Element of REAL
Y (#) C is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of K19(K20(X,REAL))
dom C is Element of K19(X)
K19(X) is set
f1 is ext-real complex real Element of REAL
dom Y is Element of K19(X)
f2 is ext-real complex real Element of REAL
c is Element of X
dom (Y (#) C) is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
(Y (#) C) . c is ext-real complex real set
Y . c is ext-real complex real set
C . c is ext-real complex real set
(Y . c) * (C . c) is ext-real complex real set
(Y . c) * f1 is ext-real complex real Element of REAL
f2 * f1 is ext-real complex real Element of REAL
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(C,REAL)) is set
f1 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 | X is Relation-like X -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f2 | Y is Relation-like Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 + f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(f1 + f2) | (X /\ Y) is Relation-like X /\ Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 - f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
- f2 is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) f2 is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
f1 + (- f2) is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
(f1 - f2) | (X /\ Y) is Relation-like X /\ Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 (#) f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(f1 (#) f2) | (X /\ Y) is Relation-like X /\ Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
dom f1 is Element of K19(C)
K19(C) is set
X /\ (dom f1) is Element of K19(C)
c is ext-real complex real Element of REAL
dom f2 is Element of K19(C)
Y /\ (dom f2) is Element of K19(C)
r2 is ext-real complex real Element of REAL
c is Element of C
dom (f1 + f2) is Element of K19(C)
(X /\ Y) /\ (dom (f1 + f2)) is Element of K19(C)
(dom f1) /\ (dom f2) is Element of K19(C)
(f1 + f2) . c is ext-real complex real set
f1 . c is ext-real complex real set
f2 . c is ext-real complex real set
(f1 . c) + (f2 . c) is ext-real complex real set
c + (f2 . c) is ext-real complex real Element of REAL
c + r2 is ext-real complex real Element of REAL
c is Element of C
dom (f1 - f2) is Element of K19(C)
(X /\ Y) /\ (dom (f1 - f2)) is Element of K19(C)
(f1 - f2) . c is ext-real complex real set
f1 . c is ext-real complex real set
f2 . c is ext-real complex real set
(f1 . c) - (f2 . c) is ext-real complex real set
c - (f2 . c) is ext-real complex real Element of REAL
c - r2 is ext-real complex real Element of REAL
c is Element of C
dom (f1 (#) f2) is Element of K19(C)
(X /\ Y) /\ (dom (f1 (#) f2)) is Element of K19(C)
(f1 (#) f2) . c is ext-real complex real set
f1 . c is ext-real complex real set
f2 . c is ext-real complex real set
(f1 . c) * (f2 . c) is ext-real complex real set
c * (f2 . c) is ext-real complex real Element of REAL
c * r2 is ext-real complex real Element of REAL
X is non empty set
K20(X,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(X,REAL)) is set
Y is Relation-like X -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of K19(K20(X,REAL))
- Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K19(K20(X,REAL))
(- 1) (#) Y is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded set
dom Y is Element of K19(X)
K19(X) is set
C is ext-real complex real Element of REAL
- C is ext-real complex real Element of REAL
f2 is Element of X
dom (- Y) is Element of K19(X)
Y . f2 is ext-real complex real set
- (Y . f2) is ext-real complex real set
f1 is ext-real complex real Element of REAL
(- Y) . f2 is ext-real complex real set
f1 is ext-real complex real Element of REAL
abs Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of K19(K20(X,REAL))
dom Y is Element of K19(X)
K19(X) is set
C is ext-real complex real Element of REAL
abs C is ext-real complex real Element of REAL
f2 is Element of X
dom (abs Y) is Element of K19(X)
Y . f2 is ext-real complex real set
abs (Y . f2) is ext-real complex real Element of REAL
f1 is ext-real complex real Element of REAL
(abs Y) . f2 is ext-real complex real set
f1 is ext-real complex real Element of REAL
C is ext-real complex real set
C (#) Y is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(X,REAL))
dom Y is Element of K19(X)
K19(X) is set
f1 is ext-real complex real Element of REAL
C * f1 is ext-real complex real Element of REAL
c is Element of X
dom (C (#) Y) is Element of K19(X)
Y . c is ext-real complex real set
C * (Y . c) is ext-real complex real set
f2 is ext-real complex real Element of REAL
(C (#) Y) . c is ext-real complex real set
f2 is ext-real complex real Element of REAL
X is set
Y is non empty set
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
C is ext-real complex real set
f1 is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
f1 | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
C (#) f1 is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
(C (#) f1) | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
C (#) (f1 | X) is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
X is set
Y is non empty set
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
C | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
- C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
(- 1) (#) C is Relation-like Y -defined Function-like complex-valued ext-real-valued real-valued set
(- C) | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
- (C | X) is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
(- 1) (#) (C | X) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set
X is set
Y is non empty set
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
C | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
abs C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K19(K20(Y,REAL))
(abs C) | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K19(K20(Y,REAL))
abs (C | X) is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K19(K20(Y,REAL))
X is set
Y is non empty set
K20(Y,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(Y,REAL)) is set
C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
C | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
- C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
(- 1) (#) C is Relation-like Y -defined Function-like complex-valued ext-real-valued real-valued set
(- C) | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
abs C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K19(K20(Y,REAL))
(abs C) | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K19(K20(Y,REAL))
f1 is ext-real complex real set
f1 (#) C is Relation-like Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
(f1 (#) C) | X is Relation-like X -defined Y -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(Y,REAL))
C is non empty set
K20(C,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(C,REAL)) is set
c is non empty set
K20(c,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(c,REAL)) is set
c₁₃ is non empty set
K20(c₁₃,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(c₁₃,REAL)) is set
f1 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
X is set
f1 | X is Relation-like C -defined X -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
Y is set
f2 | Y is Relation-like C -defined Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 + f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
X /\ Y is set
(f1 + f2) | (X /\ Y) is Relation-like C -defined X /\ Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
c₉ is Relation-like c -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c,REAL))
c is set
c₉ | c is Relation-like c -defined c -defined c -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c,REAL))
c₁₀ is Relation-like c -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c,REAL))
r2 is set
c₁₀ | r2 is Relation-like c -defined r2 -defined c -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c,REAL))
c₉ + c₁₀ is Relation-like c -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c,REAL))
c /\ r2 is set
(c₉ + c₁₀) | (c /\ r2) is Relation-like c -defined c /\ r2 -defined c -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c,REAL))
c₁₄ is Relation-like c₁₃ -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c₁₃,REAL))
c₁₁ is set
c₁₄ | c₁₁ is Relation-like c₁₃ -defined c₁₁ -defined c₁₃ -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c₁₃,REAL))
c₁₅ is Relation-like c₁₃ -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c₁₃,REAL))
c₁₂ is set
c₁₅ | c₁₂ is Relation-like c₁₃ -defined c₁₂ -defined c₁₃ -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c₁₃,REAL))
c₁₄ + c₁₅ is Relation-like c₁₃ -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c₁₃,REAL))
c₁₁ /\ c₁₂ is set
(c₁₄ + c₁₅) | (c₁₁ /\ c₁₂) is Relation-like c₁₃ -defined c₁₁ /\ c₁₂ -defined c₁₃ -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(c₁₃,REAL))
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(C,REAL)) is set
f1 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 | X is Relation-like X -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f2 | Y is Relation-like Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 - f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
- f2 is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) f2 is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
f1 + (- f2) is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
(f1 - f2) | (X /\ Y) is Relation-like X /\ Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f2 - f1 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
- f1 is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) f1 is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
f2 + (- f1) is Relation-like C -defined Function-like complex-valued ext-real-valued real-valued set
(f2 - f1) | (X /\ Y) is Relation-like X /\ Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
f1 (#) f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(f1 (#) f2) | (X /\ Y) is Relation-like X /\ Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
- f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(- f2) | Y is Relation-like Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
- f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(- f2) | Y is Relation-like Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
- f2 is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))
(- f2) | Y is Relation-like Y -defined C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(C,REAL))