:: RFUNCT_1 semantic presentation

K19(REAL) is set

{{},1} is non empty set
COMPLEX is non empty complex-membered V51() V52() 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

dom Y is set

dom X is set

Y " is set
(dom Y) \ (Y " ) is Element of K19((dom Y))
K19((dom Y)) is set
(dom X) /\ ((dom Y) \ (Y " )) is Element of K19((dom Y))

dom C is set

dom C is 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,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

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

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

K19(K20(X,Y)) is 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 " is Element of K19(X)
(dom f1) \ (f1 " ) is Element of K19(X)
(dom C) /\ ((dom f1) \ (f1 " )) is Element of K19(X)
X is set

K19(K20(X,Y)) is set

K19(K20(X,REAL)) is 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

dom X is set
X " is set
(dom X) \ (X " ) is Element of K19((dom X))
K19((dom X)) is set

dom Y is set

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

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

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

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

K19(K20(X,Y)) is 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 " is Element of K19(X)
(dom C) \ (C " ) is Element of K19(X)
X is set

K19(K20(X,Y)) is set

K19(K20(X,REAL)) is set

K19(K20(X,COMPLEX)) is set

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

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

dom (X) is set
dom X is set
X " is set
(dom X) \ (X " ) is Element of K19((dom X))
K19((dom X)) is set
(dom X) /\ ((dom X) \ (X " )) is Element of K19((dom X))

dom X is set
X " is set
(dom X) \ (X " ) is Element of K19((dom X))
K19((dom X)) is set

dom (X (#) Y) is set
(X (#) Y) " is set
(dom (X (#) Y)) \ ((X (#) Y) " ) is Element of K19((dom (X (#) Y)))
K19((dom (X (#) Y))) is set
dom Y is set
Y " is set
(dom Y) \ (Y " ) is Element of K19((dom Y))
K19((dom Y)) is set
((dom X) \ (X " )) /\ ((dom Y) \ (Y " )) 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

dom (C) is set
C . Y is complex set
dom C is set
C " is set
(dom C) \ (C " ) is Element of K19((dom C))
K19((dom C)) is set

(X) " is set
the Element of (X) " is Element of (X) "
dom (X) is set
dom X is set
X " is set
(dom X) \ (X " ) is Element of K19((dom X))
K19((dom X)) is set
X . the Element of (X) " is complex set
(X) . the Element of (X) " is complex set
(X . the Element of (X) " ) " is complex set

|.X.| " is set
X " is set

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

(- X) " is set
Y is 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

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

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

dom (- X) is set

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

dom (X | (dom (X))) is set
dom X is set
X " is set
(dom X) \ (X " ) is Element of K19((dom X))
K19((dom X)) is set
(X) " is set
(dom (X)) \ ((X) " ) 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 set
Y is complex set

(Y (#) X) " 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

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

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 (#) 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 (#) Y) + (X (#) C) is Relation-like Function-like complex-valued set

C is complex 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

C is complex 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

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

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

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

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

C is complex 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

Y is complex set
C is complex set
Y * C is complex 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

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

C is complex set

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

- 1 is non empty ext-real non positive negative complex real 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

- 1 is non empty ext-real non positive negative complex real 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

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

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

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

- 1 is non empty ext-real non positive negative complex real 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

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) * (abs (Y . C)) is ext-real complex real Element of REAL

(|.X.| . C) * (|.Y.| . C) is ext-real complex real set
() . 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) /\ () is set
dom |.X.| is set
() /\ () is set
dom () is set

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

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

dom (X) is 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

dom ((X (#) Y)) is set
dom (X (#) Y) is set
(X (#) Y) " is set
(dom (X (#) Y)) \ ((X (#) Y) " ) is Element of K19((dom (X (#) Y)))
K19((dom (X (#) Y))) is set
dom Y is set
dom X is set
X " is set
(dom X) \ (X " ) is Element of K19((dom X))
K19((dom X)) is set
Y " is set
(dom Y) \ (Y " ) is Element of K19((dom Y))
K19((dom Y)) is set
((dom X) \ (X " )) /\ ((dom Y) \ (Y " )) is Element of K19((dom Y))
dom (X) is set
(dom (X)) /\ ((dom Y) \ (Y " )) 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

Y is complex set

Y " is complex set

dom ((Y (#) X)) is set
dom (Y (#) X) is set
(Y (#) X) " is set
(dom (Y (#) X)) \ ((Y (#) X) " ) is Element of K19((dom (Y (#) X)))
K19((dom (Y (#) X))) is set
X " is set
(dom (Y (#) X)) \ (X " ) is Element of K19((dom (Y (#) X)))
dom X is set
(dom X) \ (X " ) 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

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

dom (|.X.|) is set
dom |.X.| is set
|.X.| " is set
() \ () is Element of K19(())
K19(()) is set
dom X is set
(dom X) \ () is Element of K19((dom X))
K19((dom X)) is set
X " is set
(dom X) \ (X " ) 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 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

C is set
dom (X,Y) is set
dom Y is set
dom X is set
Y " is set
(dom Y) \ (Y " ) is Element of K19((dom Y))
K19((dom Y)) is set
(dom X) /\ ((dom Y) \ (Y " )) 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

C is complex set

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

dom (Y) is 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 " is set
(dom Y) \ (Y " ) is Element of K19((dom Y))
K19((dom Y)) is set
(dom X) /\ ((dom Y) \ (Y " )) is Element of K19((dom Y))
((dom X) /\ ((dom Y) \ (Y " ))) /\ (dom Y) is Element of K19((dom Y))
((dom Y) \ (Y " )) /\ (dom Y) is Element of K19((dom Y))
(dom X) /\ (((dom Y) \ (Y " )) /\ (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)) . 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,Y) (#) (C,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

(X (#) (Y)) . f2 is complex set
((X (#) (Y)) . f2) * ((C,f1) . 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
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)) . 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 " is set
(dom Y) \ (Y " ) is Element of K19((dom Y))
K19((dom Y)) is set
(dom X) /\ ((dom Y) \ (Y " )) is Element of K19((dom Y))
((dom X) /\ ((dom Y) \ (Y " ))) /\ (dom (C,f1)) is Element of K19((dom Y))
dom f1 is set
dom C is set
f1 " is set
(dom f1) \ (f1 " ) is Element of K19((dom f1))
K19((dom f1)) is set
(dom C) /\ ((dom f1) \ (f1 " )) is Element of K19((dom f1))
((dom X) /\ ((dom Y) \ (Y " ))) /\ ((dom C) /\ ((dom f1) \ (f1 " ))) is Element of K19((dom f1))
((dom Y) \ (Y " )) /\ ((dom C) /\ ((dom f1) \ (f1 " ))) is Element of K19((dom f1))
(dom X) /\ (((dom Y) \ (Y " )) /\ ((dom C) /\ ((dom f1) \ (f1 " )))) is Element of K19((dom f1))
((dom Y) \ (Y " )) /\ ((dom f1) \ (f1 " )) is Element of K19((dom f1))
(dom C) /\ (((dom Y) \ (Y " )) /\ ((dom f1) \ (f1 " ))) is Element of K19((dom f1))
(dom X) /\ ((dom C) /\ (((dom Y) \ (Y " )) /\ ((dom f1) \ (f1 " )))) is Element of K19((dom f1))
(dom X) /\ (dom C) is set
((dom X) /\ (dom C)) /\ (((dom Y) \ (Y " )) /\ ((dom f1) \ (f1 " ))) is Element of K19((dom f1))
dom (X (#) C) is set
(dom (X (#) C)) /\ (((dom Y) \ (Y " )) /\ ((dom f1) \ (f1 " ))) is Element of K19((dom f1))
dom (Y (#) f1) is set
(Y (#) f1) " is set
(dom (Y (#) f1)) \ ((Y (#) f1) " ) is Element of K19((dom (Y (#) f1)))
K19((dom (Y (#) f1))) is set
(dom (X (#) C)) /\ ((dom (Y (#) f1)) \ ((Y (#) f1) " )) is Element of K19((dom (Y (#) f1)))
dom ((X (#) C),(Y (#) f1)) is set

dom (Y) is set

((Y | (dom (Y))),X) 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 (#) Y),C) is Relation-like Function-like complex-valued set

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

dom (C) is 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

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

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

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

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

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

- 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),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 + 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

(- 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,Y) + (C,f1) is Relation-like Function-like complex-valued set

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

(((X (#) f1) + (C (#) Y)),(Y (#) 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

dom (Y) is set
dom Y is 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

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

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