:: CFUNCT_1 semantic presentation

REAL is non empty V48() V49() V50() V54() V55() set
NAT is V48() V49() V50() V51() V52() V53() V54() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V48() V54() V55() set
RAT is non empty V48() V49() V50() V51() V54() V55() set
INT is non empty V48() V49() V50() V51() V52() V54() V55() set
{} is set
the empty V48() V49() V50() V51() V52() V53() V54() set is empty V48() V49() V50() V51() V52() V53() V54() set
1 is non empty ext-real natural complex real V36() V37() V48() V49() V50() V51() V52() V53() Element of NAT
{{},1} is set
0 is ext-real natural complex real V36() V37() V48() V49() V50() V51() V52() V53() Element of NAT
{0} is V48() V49() V50() V51() V52() V53() set
1r is complex Element of COMPLEX
|.0.| is ext-real complex real Element of REAL
|.1r.| is ext-real complex real Element of REAL
0 " is ext-real complex real set
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
C " {0} is Element of K19(X)
(dom C) \ (C " {0}) is Element of K19(X)
(dom Y) /\ ((dom C) \ (C " {0})) is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
(dom Y) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom f1 is Element of K19(X)
f2 is Element of X
f1 /. f2 is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(C /. f2) " is complex Element of COMPLEX
(Y /. f2) * ((C /. f2) ") is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
Y " {0} is Element of K19(X)
(dom Y) \ (Y " {0}) is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom C is Element of K19(X)
f1 is Element of X
C /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
(Y /. f1) " is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y + C) is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
f1 is Element of X
Y . f1 is complex set
Y /. f1 is complex Element of COMPLEX
C . f1 is complex set
C /. f1 is complex Element of COMPLEX
(Y + C) /. f1 is complex Element of COMPLEX
(Y + C) . f1 is complex set
(Y /. f1) + (C /. f1) is complex Element of COMPLEX
f1 is Element of X
(Y + C) /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
(Y /. f1) + (C /. f1) is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y + (- C) is V1() Function-like set
dom (Y - C) is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
- C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (- C) is Element of K19(X)
(dom Y) /\ (dom (- C)) is Element of K19(X)
f1 is Element of X
Y /. f1 is complex Element of COMPLEX
Y . f1 is complex set
(Y - C) /. f1 is complex Element of COMPLEX
(Y - C) . f1 is complex set
C . f1 is complex set
(Y . f1) - (C . f1) is set
C /. f1 is complex Element of COMPLEX
(Y /. f1) - (C /. f1) is complex Element of COMPLEX
f1 is Element of X
(Y - C) /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
(Y /. f1) - (C /. f1) is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y (#) C) is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
f1 is Element of X
Y . f1 is complex set
Y /. f1 is complex Element of COMPLEX
C . f1 is complex set
C /. f1 is complex Element of COMPLEX
(Y (#) C) /. f1 is complex Element of COMPLEX
(Y (#) C) . f1 is complex set
(Y /. f1) * (C /. f1) is complex Element of COMPLEX
f1 is Element of X
(Y (#) C) /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
(Y /. f1) * (C /. f1) is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
C is complex Element of COMPLEX
C (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (C (#) Y) is Element of K19(X)
f1 is Element of X
(C (#) Y) /. f1 is complex Element of COMPLEX
(C (#) Y) . f1 is complex set
Y . f1 is complex set
C * (Y . f1) is set
Y /. f1 is complex Element of COMPLEX
C * (Y /. f1) is complex Element of COMPLEX
f1 is Element of X
(C (#) Y) /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C * (Y /. f1) is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) Y is V1() Function-like set
dom (- Y) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
C is Element of X
(- Y) /. C is complex Element of COMPLEX
(- Y) . C is complex set
Y . C is complex set
- (Y . C) is complex set
Y /. C is complex Element of COMPLEX
- (Y /. C) is complex Element of COMPLEX
C is Element of X
(- Y) /. C is complex Element of COMPLEX
Y /. C is complex Element of COMPLEX
- (Y /. C) is complex Element of COMPLEX
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
cr2 is non empty set
K20(cr2,COMPLEX) is V38() set
K19(K20(cr2,COMPLEX)) is set
X is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
Y is set
f1 " Y is Element of K19(C)
K19(C) is set
dom f1 is Element of K19(C)
f1 /. X is complex Element of COMPLEX
f2 is set
c is V1() V4(cr2) V5( COMPLEX ) Function-like V38() Element of K19(K20(cr2,COMPLEX))
dom c is Element of K19(cr2)
K19(cr2) is set
c /. f2 is complex Element of COMPLEX
c is set
c " c is Element of K19(cr2)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,Y) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
Y " {0} is Element of K19(X)
(dom Y) \ (Y " {0}) is Element of K19(X)
(dom Y) /\ ((dom Y) \ (Y " {0})) is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
Y " {0} is Element of K19(X)
(dom Y) \ (Y " {0}) is Element of K19(X)
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y (#) C) is Element of K19(X)
(Y (#) C) " {0} is Element of K19(X)
(dom (Y (#) C)) \ ((Y (#) C) " {0}) is Element of K19(X)
dom C is Element of K19(X)
C " {0} is Element of K19(X)
(dom C) \ (C " {0}) is Element of K19(X)
((dom Y) \ (Y " {0})) /\ ((dom C) \ (C " {0})) is Element of K19(X)
f1 is set
0c is complex Element of COMPLEX
{0c} is V48() set
(Y (#) C) " {0c} is Element of K19(X)
f2 is Element of X
(Y (#) C) /. f2 is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) * (C /. f2) is complex Element of COMPLEX
C " {0c} is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
f1 is set
0c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
f2 is Element of X
C /. f2 is complex Element of COMPLEX
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
Y /. f2 is complex Element of COMPLEX
(Y /. f2) * (C /. f2) is complex Element of COMPLEX
(Y (#) C) /. f2 is complex Element of COMPLEX
(Y (#) C) " {0c} is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is Element of X
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,C) is Element of K19(X)
K19(X) is set
C /. Y is complex Element of COMPLEX
dom C is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) " {0} is Element of K19(X)
K19(X) is set
0c is complex Element of COMPLEX
{0c} is V48() set
(X,Y) " {0c} is Element of K19(X)
the Element of (X,Y) " {0c} is Element of (X,Y) " {0c}
dom (X,Y) is Element of K19(X)
(X,Y) /. the Element of (X,Y) " {0c} is complex Element of COMPLEX
f1 is Element of X
dom Y is Element of K19(X)
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
Y /. f1 is complex Element of COMPLEX
(X,Y) /. f1 is complex Element of COMPLEX
(Y /. f1) " is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
|.Y.| " {0} is Element of K19(X)
K19(X) is set
Y " {0} is Element of K19(X)
- Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) Y is V1() Function-like set
(- Y) " {0} is Element of K19(X)
dom |.Y.| is Element of K19(X)
dom Y is Element of K19(X)
C is Element of X
0c is complex Element of COMPLEX
{0c} is V48() set
Y " {0c} is Element of K19(X)
|.Y.| . C is ext-real complex real set
Y . C is complex set
|.(Y . C).| is ext-real complex real Element of REAL
Y /. C is complex Element of COMPLEX
Y /. C is complex Element of COMPLEX
|.(Y /. C).| is ext-real complex real Element of REAL
Y . C is complex set
|.Y.| . C is ext-real complex real set
C is Element of X
(- Y) " {0c} is Element of K19(X)
dom (- Y) is Element of K19(X)
(- Y) /. C is complex Element of COMPLEX
Y /. C is complex Element of COMPLEX
- (Y /. C) is complex Element of COMPLEX
- (- (Y /. C)) is complex Element of COMPLEX
- 0c is complex Element of COMPLEX
Y /. C is complex Element of COMPLEX
dom (- Y) is Element of K19(X)
(- Y) /. C is complex Element of COMPLEX
- 0c is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(X,Y)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,(X,Y)) is Element of K19(X)
K19(X) is set
dom (X,Y) is Element of K19(X)
Y | (dom (X,Y)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y | (dom (X,Y))) is Element of K19(X)
dom Y is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
(X,Y) " {0c} is Element of K19(X)
(dom (X,Y)) \ ((X,Y) " {0c}) is Element of K19(X)
(dom (X,Y)) \ {} is Element of K19(X)
(dom Y) /\ (dom (X,Y)) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y " {0} is Element of K19(X)
K19(X) is set
C is complex Element of COMPLEX
C (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(C (#) Y) " {0} is Element of K19(X)
f1 is Element of X
0c is complex Element of COMPLEX
{0c} is V48() set
(C (#) Y) " {0c} is Element of K19(X)
Y " {0c} is Element of K19(X)
dom (C (#) Y) is Element of K19(X)
(C (#) Y) /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C * (Y /. f1) is complex Element of COMPLEX
dom Y is Element of K19(X)
Y /. f1 is complex Element of COMPLEX
C * (Y /. f1) is complex Element of COMPLEX
dom Y is Element of K19(X)
dom (C (#) Y) is Element of K19(X)
(C (#) Y) /. f1 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y + C) + f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C + f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + (C + f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((Y + C) + f1) is Element of K19(X)
K19(X) is set
dom (Y + C) is Element of K19(X)
dom f1 is Element of K19(X)
(dom (Y + C)) /\ (dom f1) is Element of K19(X)
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) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(dom C) /\ (dom f1) is Element of K19(X)
(dom Y) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
dom (C + f1) is Element of K19(X)
(dom Y) /\ (dom (C + f1)) is Element of K19(X)
dom (Y + (C + f1)) is Element of K19(X)
f2 is Element of X
((Y + C) + f1) /. f2 is complex Element of COMPLEX
(Y + C) /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
((Y + C) /. f2) + (f1 /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) + (C /. f2) is complex Element of COMPLEX
((Y /. f2) + (C /. f2)) + (f1 /. f2) is complex Element of COMPLEX
(C /. f2) + (f1 /. f2) is complex Element of COMPLEX
(Y /. f2) + ((C /. f2) + (f1 /. f2)) is complex Element of COMPLEX
(C + f1) /. f2 is complex Element of COMPLEX
(Y /. f2) + ((C + f1) /. f2) is complex Element of COMPLEX
(Y + (C + f1)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) C) (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (C (#) f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((Y (#) C) (#) f1) is Element of K19(X)
K19(X) is set
dom (Y (#) C) is Element of K19(X)
dom f1 is Element of K19(X)
(dom (Y (#) C)) /\ (dom f1) is Element of K19(X)
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) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(dom C) /\ (dom f1) is Element of K19(X)
(dom Y) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
dom (C (#) f1) is Element of K19(X)
(dom Y) /\ (dom (C (#) f1)) is Element of K19(X)
dom (Y (#) (C (#) f1)) is Element of K19(X)
f2 is Element of X
((Y (#) C) (#) f1) /. f2 is complex Element of COMPLEX
(Y (#) C) /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
((Y (#) C) /. f2) * (f1 /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) * (C /. f2) is complex Element of COMPLEX
((Y /. f2) * (C /. f2)) * (f1 /. f2) is complex Element of COMPLEX
(C /. f2) * (f1 /. f2) is complex Element of COMPLEX
(Y /. f2) * ((C /. f2) * (f1 /. f2)) is complex Element of COMPLEX
(C (#) f1) /. f2 is complex Element of COMPLEX
(Y /. f2) * ((C (#) f1) /. f2) is complex Element of COMPLEX
(Y (#) (C (#) f1)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y + C) (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) f1) + (C (#) f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((Y + C) (#) f1) is Element of K19(X)
K19(X) is set
dom (Y + C) is Element of K19(X)
dom f1 is Element of K19(X)
(dom (Y + C)) /\ (dom f1) is Element of K19(X)
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
(dom f1) /\ (dom f1) is Element of K19(X)
((dom Y) /\ (dom C)) /\ ((dom f1) /\ (dom f1)) is Element of K19(X)
((dom Y) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(((dom Y) /\ (dom C)) /\ (dom f1)) /\ (dom f1) is Element of K19(X)
(dom Y) /\ (dom f1) is Element of K19(X)
((dom Y) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(((dom Y) /\ (dom f1)) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(dom C) /\ (dom f1) is Element of K19(X)
((dom Y) /\ (dom f1)) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
dom (Y (#) f1) is Element of K19(X)
(dom (Y (#) f1)) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
dom (C (#) f1) is Element of K19(X)
(dom (Y (#) f1)) /\ (dom (C (#) f1)) is Element of K19(X)
dom ((Y (#) f1) + (C (#) f1)) is Element of K19(X)
f2 is Element of X
((Y + C) (#) f1) /. f2 is complex Element of COMPLEX
(Y + C) /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
((Y + C) /. f2) * (f1 /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) + (C /. f2) is complex Element of COMPLEX
((Y /. f2) + (C /. f2)) * (f1 /. f2) is complex Element of COMPLEX
(Y /. f2) * (f1 /. f2) is complex Element of COMPLEX
(C /. f2) * (f1 /. f2) is complex Element of COMPLEX
((Y /. f2) * (f1 /. f2)) + ((C /. f2) * (f1 /. f2)) is complex Element of COMPLEX
(Y (#) f1) /. f2 is complex Element of COMPLEX
((Y (#) f1) /. f2) + ((C /. f2) * (f1 /. f2)) is complex Element of COMPLEX
(C (#) f1) /. f2 is complex Element of COMPLEX
((Y (#) f1) /. f2) + ((C (#) f1) /. f2) is complex Element of COMPLEX
((Y (#) f1) + (C (#) f1)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C + f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (C + f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) C) + (Y (#) f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is complex Element of COMPLEX
f1 (#) (Y (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(f1 (#) Y) (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (f1 (#) (Y (#) C)) is Element of K19(X)
K19(X) is set
dom (Y (#) C) is Element of K19(X)
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
dom (f1 (#) Y) is Element of K19(X)
(dom (f1 (#) Y)) /\ (dom C) is Element of K19(X)
dom ((f1 (#) Y) (#) C) is Element of K19(X)
f2 is Element of X
(f1 (#) (Y (#) C)) /. f2 is complex Element of COMPLEX
(Y (#) C) /. f2 is complex Element of COMPLEX
f1 * ((Y (#) C) /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) * (C /. f2) is complex Element of COMPLEX
f1 * ((Y /. f2) * (C /. f2)) is complex Element of COMPLEX
f1 * (Y /. f2) is complex Element of COMPLEX
(f1 * (Y /. f2)) * (C /. f2) is complex Element of COMPLEX
(f1 (#) Y) /. f2 is complex Element of COMPLEX
((f1 (#) Y) /. f2) * (C /. f2) is complex Element of COMPLEX
((f1 (#) Y) (#) C) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is complex Element of COMPLEX
f1 (#) (Y (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (f1 (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (f1 (#) (Y (#) C)) is Element of K19(X)
K19(X) is set
dom (Y (#) C) is Element of K19(X)
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
dom (f1 (#) C) is Element of K19(X)
(dom Y) /\ (dom (f1 (#) C)) is Element of K19(X)
dom (Y (#) (f1 (#) C)) is Element of K19(X)
f2 is Element of X
(f1 (#) (Y (#) C)) /. f2 is complex Element of COMPLEX
(Y (#) C) /. f2 is complex Element of COMPLEX
f1 * ((Y (#) C) /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) * (C /. f2) is complex Element of COMPLEX
f1 * ((Y /. f2) * (C /. f2)) is complex Element of COMPLEX
f1 * (C /. f2) is complex Element of COMPLEX
(Y /. f2) * (f1 * (C /. f2)) is complex Element of COMPLEX
(f1 (#) C) /. f2 is complex Element of COMPLEX
(Y /. f2) * ((f1 (#) C) /. f2) is complex Element of COMPLEX
(Y (#) (f1 (#) C)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y + (- C) is V1() Function-like set
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y - C) (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) f1) - (C (#) f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (C (#) f1) is V1() Function-like V38() set
(- 1) (#) (C (#) f1) is V1() Function-like set
(Y (#) f1) + (- (C (#) f1)) is V1() Function-like set
dom ((Y - C) (#) f1) is Element of K19(X)
K19(X) is set
dom (Y - C) is Element of K19(X)
dom f1 is Element of K19(X)
(dom (Y - C)) /\ (dom f1) is Element of K19(X)
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
(dom f1) /\ (dom f1) is Element of K19(X)
((dom Y) /\ (dom C)) /\ ((dom f1) /\ (dom f1)) is Element of K19(X)
((dom Y) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(((dom Y) /\ (dom C)) /\ (dom f1)) /\ (dom f1) is Element of K19(X)
(dom Y) /\ (dom f1) is Element of K19(X)
((dom Y) /\ (dom f1)) /\ (dom C) is Element of K19(X)
(((dom Y) /\ (dom f1)) /\ (dom C)) /\ (dom f1) is Element of K19(X)
(dom C) /\ (dom f1) is Element of K19(X)
((dom Y) /\ (dom f1)) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
dom (Y (#) f1) is Element of K19(X)
(dom (Y (#) f1)) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
dom (C (#) f1) is Element of K19(X)
(dom (Y (#) f1)) /\ (dom (C (#) f1)) is Element of K19(X)
dom ((Y (#) f1) - (C (#) f1)) is Element of K19(X)
f2 is Element of X
((Y - C) (#) f1) /. f2 is complex Element of COMPLEX
(Y - C) /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
((Y - C) /. f2) * (f1 /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) - (C /. f2) is complex Element of COMPLEX
((Y /. f2) - (C /. f2)) * (f1 /. f2) is complex Element of COMPLEX
(Y /. f2) * (f1 /. f2) is complex Element of COMPLEX
(C /. f2) * (f1 /. f2) is complex Element of COMPLEX
((Y /. f2) * (f1 /. f2)) - ((C /. f2) * (f1 /. f2)) is complex Element of COMPLEX
(Y (#) f1) /. f2 is complex Element of COMPLEX
((Y (#) f1) /. f2) - ((C /. f2) * (f1 /. f2)) is complex Element of COMPLEX
(C (#) f1) /. f2 is complex Element of COMPLEX
((Y (#) f1) /. f2) - ((C (#) f1) /. f2) is complex Element of COMPLEX
((Y (#) f1) - (C (#) f1)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) C) - (Y (#) f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (Y (#) f1) is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) (Y (#) f1) is V1() Function-like set
(Y (#) C) + (- (Y (#) f1)) is V1() Function-like set
C - f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- f1 is V1() Function-like V38() set
(- 1) (#) f1 is V1() Function-like set
C + (- f1) is V1() Function-like set
Y (#) (C - f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is complex Element of COMPLEX
f1 (#) (Y + C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(f1 (#) Y) + (f1 (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (f1 (#) (Y + C)) is Element of K19(X)
K19(X) is set
dom (Y + C) is Element of K19(X)
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
dom (f1 (#) C) is Element of K19(X)
(dom Y) /\ (dom (f1 (#) C)) is Element of K19(X)
dom (f1 (#) Y) is Element of K19(X)
(dom (f1 (#) Y)) /\ (dom (f1 (#) C)) is Element of K19(X)
dom ((f1 (#) Y) + (f1 (#) C)) is Element of K19(X)
f2 is Element of X
(f1 (#) (Y + C)) /. f2 is complex Element of COMPLEX
(Y + C) /. f2 is complex Element of COMPLEX
f1 * ((Y + C) /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) + (C /. f2) is complex Element of COMPLEX
f1 * ((Y /. f2) + (C /. f2)) is complex Element of COMPLEX
f1 * (Y /. f2) is complex Element of COMPLEX
f1 * (C /. f2) is complex Element of COMPLEX
(f1 * (Y /. f2)) + (f1 * (C /. f2)) is complex Element of COMPLEX
(f1 (#) Y) /. f2 is complex Element of COMPLEX
((f1 (#) Y) /. f2) + (f1 * (C /. f2)) is complex Element of COMPLEX
(f1 (#) C) /. f2 is complex Element of COMPLEX
((f1 (#) Y) /. f2) + ((f1 (#) C) /. f2) is complex Element of COMPLEX
((f1 (#) Y) + (f1 (#) C)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is complex Element of COMPLEX
f1 is complex Element of COMPLEX
C * f1 is complex Element of COMPLEX
(C * f1) (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) (f1 (#) Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((C * f1) (#) Y) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
dom (f1 (#) Y) is Element of K19(X)
dom (C (#) (f1 (#) Y)) is Element of K19(X)
f2 is Element of X
((C * f1) (#) Y) /. f2 is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
(C * f1) * (Y /. f2) is complex Element of COMPLEX
f1 * (Y /. f2) is complex Element of COMPLEX
C * (f1 * (Y /. f2)) is complex Element of COMPLEX
(f1 (#) Y) /. f2 is complex Element of COMPLEX
C * ((f1 (#) Y) /. f2) is complex Element of COMPLEX
(C (#) (f1 (#) Y)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y + (- C) is V1() Function-like set
f1 is complex Element of COMPLEX
f1 (#) (Y - C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(f1 (#) Y) - (f1 (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (f1 (#) C) is V1() Function-like V38() set
(- 1) (#) (f1 (#) C) is V1() Function-like set
(f1 (#) Y) + (- (f1 (#) C)) is V1() Function-like set
dom (f1 (#) (Y - C)) is Element of K19(X)
K19(X) is set
dom (Y - C) is Element of K19(X)
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
dom (f1 (#) C) is Element of K19(X)
(dom Y) /\ (dom (f1 (#) C)) is Element of K19(X)
dom (f1 (#) Y) is Element of K19(X)
(dom (f1 (#) Y)) /\ (dom (f1 (#) C)) is Element of K19(X)
dom ((f1 (#) Y) - (f1 (#) C)) is Element of K19(X)
f2 is Element of X
(f1 (#) (Y - C)) /. f2 is complex Element of COMPLEX
(Y - C) /. f2 is complex Element of COMPLEX
f1 * ((Y - C) /. f2) is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
(Y /. f2) - (C /. f2) is complex Element of COMPLEX
f1 * ((Y /. f2) - (C /. f2)) is complex Element of COMPLEX
f1 * (Y /. f2) is complex Element of COMPLEX
f1 * (C /. f2) is complex Element of COMPLEX
(f1 * (Y /. f2)) - (f1 * (C /. f2)) is complex Element of COMPLEX
(f1 (#) Y) /. f2 is complex Element of COMPLEX
((f1 (#) Y) /. f2) - (f1 * (C /. f2)) is complex Element of COMPLEX
(f1 (#) C) /. f2 is complex Element of COMPLEX
((f1 (#) Y) /. f2) - ((f1 (#) C) /. f2) is complex Element of COMPLEX
((f1 (#) Y) - (f1 (#) C)) /. f2 is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y + (- C) is V1() Function-like set
C - Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- Y is V1() Function-like V38() set
(- 1) (#) Y is V1() Function-like set
C + (- Y) is V1() Function-like set
(- 1r) (#) (C - Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y - C) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom Y is Element of K19(X)
(dom C) /\ (dom Y) is Element of K19(X)
dom (C - Y) is Element of K19(X)
dom ((- 1r) (#) (C - Y)) is Element of K19(X)
f1 is Element of X
(Y - C) /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
(Y /. f1) - (C /. f1) is complex Element of COMPLEX
(C /. f1) - (Y /. f1) is complex Element of COMPLEX
(- 1) * ((C /. f1) - (Y /. f1)) is set
(C - Y) /. f1 is complex Element of COMPLEX
(- 1r) * ((C - Y) /. f1) is complex Element of COMPLEX
((- 1r) (#) (C - Y)) /. f1 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y + (- C) is V1() Function-like set
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C + f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - (C + f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (C + f1) is V1() Function-like V38() set
(- 1) (#) (C + f1) is V1() Function-like set
Y + (- (C + f1)) is V1() Function-like set
(Y - C) - f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- f1 is V1() Function-like V38() set
(- 1) (#) f1 is V1() Function-like set
(Y - C) + (- f1) is V1() Function-like set
dom (Y - (C + f1)) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
dom (C + f1) is Element of K19(X)
(dom Y) /\ (dom (C + f1)) is Element of K19(X)
dom C is Element of K19(X)
dom f1 is Element of K19(X)
(dom C) /\ (dom f1) is Element of K19(X)
(dom Y) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
((dom Y) /\ (dom C)) /\ (dom f1) is Element of K19(X)
dom (Y - C) is Element of K19(X)
(dom (Y - C)) /\ (dom f1) is Element of K19(X)
dom ((Y - C) - f1) is Element of K19(X)
f2 is Element of X
(Y - (C + f1)) /. f2 is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
(C + f1) /. f2 is complex Element of COMPLEX
(Y /. f2) - ((C + f1) /. f2) is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) + (f1 /. f2) is complex Element of COMPLEX
(Y /. f2) - ((C /. f2) + (f1 /. f2)) is complex Element of COMPLEX
(Y /. f2) - (C /. f2) is complex Element of COMPLEX
((Y /. f2) - (C /. f2)) - (f1 /. f2) is complex Element of COMPLEX
(Y - C) /. f2 is complex Element of COMPLEX
((Y - C) /. f2) - (f1 /. f2) is complex Element of COMPLEX
((Y - C) - f1) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
1r (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is Element of X
dom (1r (#) Y) is Element of K19(X)
K19(X) is set
(1r (#) Y) /. C is complex Element of COMPLEX
Y /. C is complex Element of COMPLEX
1r * (Y /. C) is complex Element of COMPLEX
dom Y is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y + (- C) is V1() Function-like set
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C - f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- f1 is V1() Function-like V38() set
(- 1) (#) f1 is V1() Function-like set
C + (- f1) is V1() Function-like set
Y - (C - f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (C - f1) is V1() Function-like V38() set
(- 1) (#) (C - f1) is V1() Function-like set
Y + (- (C - f1)) is V1() Function-like set
(Y - C) + f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y - (C - f1)) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
dom (C - f1) is Element of K19(X)
(dom Y) /\ (dom (C - f1)) is Element of K19(X)
dom C is Element of K19(X)
dom f1 is Element of K19(X)
(dom C) /\ (dom f1) is Element of K19(X)
(dom Y) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
((dom Y) /\ (dom C)) /\ (dom f1) is Element of K19(X)
dom (Y - C) is Element of K19(X)
(dom (Y - C)) /\ (dom f1) is Element of K19(X)
dom ((Y - C) + f1) is Element of K19(X)
f2 is Element of X
(Y - (C - f1)) /. f2 is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
(C - f1) /. f2 is complex Element of COMPLEX
(Y /. f2) - ((C - f1) /. f2) is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) - (f1 /. f2) is complex Element of COMPLEX
(Y /. f2) - ((C /. f2) - (f1 /. f2)) is complex Element of COMPLEX
(Y /. f2) - (C /. f2) is complex Element of COMPLEX
((Y /. f2) - (C /. f2)) + (f1 /. f2) is complex Element of COMPLEX
(Y - C) /. f2 is complex Element of COMPLEX
((Y - C) /. f2) + (f1 /. f2) is complex Element of COMPLEX
((Y - C) + f1) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C - f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- f1 is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) f1 is V1() Function-like set
C + (- f1) is V1() Function-like set
Y + (C - f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y + C) - f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y + C) + (- f1) is V1() Function-like set
dom (Y + (C - f1)) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
dom (C - f1) is Element of K19(X)
(dom Y) /\ (dom (C - f1)) is Element of K19(X)
dom C is Element of K19(X)
dom f1 is Element of K19(X)
(dom C) /\ (dom f1) is Element of K19(X)
(dom Y) /\ ((dom C) /\ (dom f1)) is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
((dom Y) /\ (dom C)) /\ (dom f1) is Element of K19(X)
dom (Y + C) is Element of K19(X)
(dom (Y + C)) /\ (dom f1) is Element of K19(X)
dom ((Y + C) - f1) is Element of K19(X)
f2 is Element of X
(Y + (C - f1)) /. f2 is complex Element of COMPLEX
Y /. f2 is complex Element of COMPLEX
(C - f1) /. f2 is complex Element of COMPLEX
(Y /. f2) + ((C - f1) /. f2) is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) - (f1 /. f2) is complex Element of COMPLEX
(Y /. f2) + ((C /. f2) - (f1 /. f2)) is complex Element of COMPLEX
(Y /. f2) + (C /. f2) is complex Element of COMPLEX
((Y /. f2) + (C /. f2)) - (f1 /. f2) is complex Element of COMPLEX
(Y + C) /. f2 is complex Element of COMPLEX
((Y + C) /. f2) - (f1 /. f2) is complex Element of COMPLEX
((Y + C) - f1) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.(Y (#) C).| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.C.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.Y.| (#) |.C.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
dom |.(Y (#) C).| is Element of K19(X)
K19(X) is set
dom (Y (#) C) is Element of K19(X)
dom Y is Element of K19(X)
dom C is Element of K19(X)
(dom Y) /\ (dom C) is Element of K19(X)
dom |.C.| is Element of K19(X)
(dom Y) /\ (dom |.C.|) is Element of K19(X)
dom |.Y.| is Element of K19(X)
(dom |.Y.|) /\ (dom |.C.|) is Element of K19(X)
dom (|.Y.| (#) |.C.|) is Element of K19(X)
f1 is Element of X
Y . f1 is complex set
Y /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
C . f1 is complex set
|.(Y (#) C).| . f1 is ext-real complex real set
(Y (#) C) . f1 is complex set
|.((Y (#) C) . f1).| is ext-real complex real Element of REAL
(Y (#) C) /. f1 is complex Element of COMPLEX
|.((Y (#) C) /. f1).| is ext-real complex real Element of REAL
(Y /. f1) * (C /. f1) is complex Element of COMPLEX
|.((Y /. f1) * (C /. f1)).| is ext-real complex real Element of REAL
|.(Y /. f1).| is ext-real complex real Element of REAL
|.(C /. f1).| is ext-real complex real Element of REAL
|.(Y /. f1).| * |.(C /. f1).| is ext-real complex real set
|.Y.| . f1 is ext-real complex real set
(|.Y.| . f1) * |.(C /. f1).| is ext-real complex real set
|.C.| . f1 is ext-real complex real set
(|.Y.| . f1) * (|.C.| . f1) is ext-real complex real set
(|.Y.| (#) |.C.|) . f1 is ext-real complex real set
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
C is complex Element of COMPLEX
C (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.(C (#) Y).| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.C.| is ext-real complex real Element of REAL
|.C.| (#) |.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
dom Y is Element of K19(X)
K19(X) is set
dom |.Y.| is Element of K19(X)
dom |.(C (#) Y).| is Element of K19(X)
dom (C (#) Y) is Element of K19(X)
dom (|.C.| (#) |.Y.|) is Element of K19(X)
f1 is Element of X
|.(C (#) Y).| . f1 is ext-real complex real set
(C (#) Y) . f1 is complex set
|.((C (#) Y) . f1).| is ext-real complex real Element of REAL
(C (#) Y) /. f1 is complex Element of COMPLEX
|.((C (#) Y) /. f1).| is ext-real complex real Element of REAL
Y /. f1 is complex Element of COMPLEX
C * (Y /. f1) is complex Element of COMPLEX
|.(C * (Y /. f1)).| is ext-real complex real Element of REAL
|.(Y /. f1).| is ext-real complex real Element of REAL
|.C.| * |.(Y /. f1).| is ext-real complex real set
Y . f1 is complex set
|.(Y . f1).| is ext-real complex real Element of REAL
|.C.| * |.(Y . f1).| is ext-real complex real set
|.Y.| . f1 is ext-real complex real set
|.C.| * (|.Y.| . f1) is ext-real complex real set
(|.C.| (#) |.Y.|) . f1 is ext-real complex real set
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) Y is V1() Function-like set
(- 1r) (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y - (- C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (- C) is V1() Function-like V38() set
(- 1) (#) (- C) is V1() Function-like set
Y + (- (- C)) is V1() Function-like set
Y + C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(X,Y)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,Y) is Element of K19(X)
K19(X) is set
Y | (dom (X,Y)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,(X,Y)) is Element of K19(X)
dom (Y | (dom (X,Y))) is Element of K19(X)
C is Element of X
dom Y is Element of K19(X)
(dom Y) /\ (dom (X,Y)) is Element of K19(X)
(X,(X,Y)) /. C is complex Element of COMPLEX
(X,Y) /. C is complex Element of COMPLEX
((X,Y) /. C) " is complex Element of COMPLEX
Y /. C is complex Element of COMPLEX
(Y /. C) " is complex Element of COMPLEX
((Y /. C) ") " is complex Element of COMPLEX
(Y | (dom (X,Y))) /. C is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(Y (#) C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,(Y (#) C)) is Element of K19(X)
K19(X) is set
dom (Y (#) C) is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
(Y (#) C) " {0c} is Element of K19(X)
(dom (Y (#) C)) \ ((Y (#) C) " {0c}) is Element of K19(X)
dom Y is Element of K19(X)
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
dom C is Element of K19(X)
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
((dom Y) \ (Y " {0c})) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
dom (X,Y) is Element of K19(X)
(dom (X,Y)) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
dom (X,C) is Element of K19(X)
(dom (X,Y)) /\ (dom (X,C)) is Element of K19(X)
dom ((X,Y) (#) (X,C)) is Element of K19(X)
f1 is Element of X
(X,(Y (#) C)) /. f1 is complex Element of COMPLEX
(Y (#) C) /. f1 is complex Element of COMPLEX
((Y (#) C) /. f1) " is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
(Y /. f1) * (C /. f1) is complex Element of COMPLEX
((Y /. f1) * (C /. f1)) " is complex Element of COMPLEX
(Y /. f1) " is complex Element of COMPLEX
(C /. f1) " is complex Element of COMPLEX
((Y /. f1) ") * ((C /. f1) ") is complex Element of COMPLEX
(X,Y) /. f1 is complex Element of COMPLEX
((X,Y) /. f1) * ((C /. f1) ") is complex Element of COMPLEX
(X,C) /. f1 is complex Element of COMPLEX
((X,Y) /. f1) * ((X,C) /. f1) is complex Element of COMPLEX
((X,Y) (#) (X,C)) /. f1 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is complex Element of COMPLEX
C (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(C (#) Y)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C " is complex Element of COMPLEX
(C ") (#) (X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,(C (#) Y)) is Element of K19(X)
K19(X) is set
dom (C (#) Y) is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
(C (#) Y) " {0c} is Element of K19(X)
(dom (C (#) Y)) \ ((C (#) Y) " {0c}) is Element of K19(X)
Y " {0c} is Element of K19(X)
(dom (C (#) Y)) \ (Y " {0c}) is Element of K19(X)
dom Y is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
dom (X,Y) is Element of K19(X)
dom ((C ") (#) (X,Y)) is Element of K19(X)
f1 is Element of X
(X,(C (#) Y)) /. f1 is complex Element of COMPLEX
(C (#) Y) /. f1 is complex Element of COMPLEX
((C (#) Y) /. f1) " is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C * (Y /. f1) is complex Element of COMPLEX
(C * (Y /. f1)) " is complex Element of COMPLEX
(Y /. f1) " is complex Element of COMPLEX
(C ") * ((Y /. f1) ") is complex Element of COMPLEX
(X,Y) /. f1 is complex Element of COMPLEX
(C ") * ((X,Y) /. f1) is complex Element of COMPLEX
((C ") (#) (X,Y)) /. f1 is complex Element of COMPLEX
(- 1r) " is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) Y is V1() Function-like set
(X,(- Y)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(- 1r) (#) (X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
|.Y.| ^ is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.(X,Y).| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
dom (|.Y.| ^) is Element of K19(X)
K19(X) is set
dom |.Y.| is Element of K19(X)
|.Y.| " {0} is Element of K19(X)
(dom |.Y.|) \ (|.Y.| " {0}) is Element of K19(X)
dom Y is Element of K19(X)
(dom Y) \ (|.Y.| " {0}) is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
dom (X,Y) is Element of K19(X)
dom |.(X,Y).| is Element of K19(X)
C is Element of X
(|.Y.| ^) . C is ext-real complex real set
|.Y.| . C is ext-real complex real set
(|.Y.| . C) " is ext-real complex real set
Y . C is complex set
|.(Y . C).| is ext-real complex real Element of REAL
|.(Y . C).| " is ext-real complex real set
Y /. C is complex Element of COMPLEX
|.(Y /. C).| is ext-real complex real Element of REAL
|.(Y /. C).| " is ext-real complex real set
|.1r.| / |.(Y /. C).| is ext-real complex real Element of COMPLEX
1r / (Y /. C) is complex Element of COMPLEX
|.(1r / (Y /. C)).| is ext-real complex real Element of REAL
(Y /. C) " is complex Element of COMPLEX
|.((Y /. C) ").| is ext-real complex real Element of REAL
(X,Y) /. C is complex Element of COMPLEX
|.((X,Y) /. C).| is ext-real complex real Element of REAL
(X,Y) . C is complex set
|.((X,Y) . C).| is ext-real complex real Element of REAL
|.(X,Y).| . C is ext-real complex real set
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is Element of X
dom (X,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)
0c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
(dom Y) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
dom (X,C) is Element of K19(X)
(dom Y) /\ (dom (X,C)) is Element of K19(X)
dom (Y (#) (X,C)) is Element of K19(X)
(X,Y,C) /. f1 is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
(C /. f1) " is complex Element of COMPLEX
(Y /. f1) * ((C /. f1) ") is complex Element of COMPLEX
(X,C) /. f1 is complex Element of COMPLEX
(Y /. f1) * ((X,C) /. f1) is complex Element of COMPLEX
(Y (#) (X,C)) /. f1 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is complex Element of COMPLEX
f1 (#) (X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(f1 (#) Y),C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) (Y (#) (X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(f1 (#) Y) (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,C) is Element of K19(X)
K19(X) is set
Y | (dom (X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((X,Y,C) (#) C) is Element of K19(X)
dom (X,Y,C) is Element of K19(X)
dom C is Element of K19(X)
(dom (X,Y,C)) /\ (dom C) is Element of K19(X)
dom Y is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
(dom Y) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
((dom Y) /\ ((dom C) \ (C " {0c}))) /\ (dom C) is Element of K19(X)
((dom C) \ (C " {0c})) /\ (dom C) is Element of K19(X)
(dom Y) /\ (((dom C) \ (C " {0c})) /\ (dom C)) is Element of K19(X)
(dom (X,C)) /\ (dom C) is Element of K19(X)
(dom Y) /\ ((dom (X,C)) /\ (dom C)) is Element of K19(X)
(dom Y) /\ (dom (X,C)) is Element of K19(X)
dom (Y | (dom (X,C))) is Element of K19(X)
f1 is Element of X
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y (#) (X,C)) is Element of K19(X)
C /. f1 is complex Element of COMPLEX
((X,Y,C) (#) C) /. f1 is complex Element of COMPLEX
(X,Y,C) /. f1 is complex Element of COMPLEX
((X,Y,C) /. f1) * (C /. f1) is complex Element of COMPLEX
(Y (#) (X,C)) /. f1 is complex Element of COMPLEX
((Y (#) (X,C)) /. f1) * (C /. f1) is complex Element of COMPLEX
Y /. f1 is complex Element of COMPLEX
(X,C) /. f1 is complex Element of COMPLEX
(Y /. f1) * ((X,C) /. f1) is complex Element of COMPLEX
((Y /. f1) * ((X,C) /. f1)) * (C /. f1) is complex Element of COMPLEX
(C /. f1) " is complex Element of COMPLEX
(Y /. f1) * ((C /. f1) ") is complex Element of COMPLEX
((Y /. f1) * ((C /. f1) ")) * (C /. f1) is complex Element of COMPLEX
((C /. f1) ") * (C /. f1) is complex Element of COMPLEX
(Y /. f1) * (((C /. f1) ") * (C /. f1)) is complex Element of COMPLEX
(Y /. f1) * 1r is complex Element of COMPLEX
(Y | (dom (X,C))) /. f1 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) (#) (X,f1,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(Y (#) f1),(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
c is Element of X
dom ((X,Y,C) (#) (X,f1,f2)) is Element of K19(X)
K19(X) is set
dom (X,Y,C) is Element of K19(X)
dom (X,f1,f2) is Element of K19(X)
(dom (X,Y,C)) /\ (dom (X,f1,f2)) is Element of K19(X)
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y (#) (X,C)) is Element of K19(X)
(dom (Y (#) (X,C))) /\ (dom (X,f1,f2)) is Element of K19(X)
dom Y is Element of K19(X)
dom (X,C) is Element of K19(X)
(dom Y) /\ (dom (X,C)) is Element of K19(X)
(X,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) (X,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (f1 (#) (X,f2)) is Element of K19(X)
(dom (Y (#) (X,C))) /\ (dom (f1 (#) (X,f2))) is Element of K19(X)
dom f1 is Element of K19(X)
dom (X,f2) is Element of K19(X)
(dom f1) /\ (dom (X,f2)) is Element of K19(X)
(dom Y) /\ (dom f1) is Element of K19(X)
dom (Y (#) f1) is Element of K19(X)
(dom (X,C)) /\ (dom (X,f2)) is Element of K19(X)
(X,C) (#) (X,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((X,C) (#) (X,f2)) is Element of K19(X)
(X,(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,(C (#) f2)) is Element of K19(X)
(dom (Y (#) f1)) /\ (dom (X,(C (#) f2))) is Element of K19(X)
(Y (#) f1) (#) (X,(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((Y (#) f1) (#) (X,(C (#) f2))) is Element of K19(X)
((X,Y,C) (#) (X,f1,f2)) /. c is complex Element of COMPLEX
(X,Y,C) /. c is complex Element of COMPLEX
(X,f1,f2) /. c is complex Element of COMPLEX
((X,Y,C) /. c) * ((X,f1,f2) /. c) is complex Element of COMPLEX
(Y (#) (X,C)) /. c is complex Element of COMPLEX
((Y (#) (X,C)) /. c) * ((X,f1,f2) /. c) is complex Element of COMPLEX
(f1 (#) (X,f2)) /. c is complex Element of COMPLEX
((Y (#) (X,C)) /. c) * ((f1 (#) (X,f2)) /. c) is complex Element of COMPLEX
Y /. c is complex Element of COMPLEX
(X,C) /. c is complex Element of COMPLEX
(Y /. c) * ((X,C) /. c) is complex Element of COMPLEX
((Y /. c) * ((X,C) /. c)) * ((f1 (#) (X,f2)) /. c) is complex Element of COMPLEX
f1 /. c is complex Element of COMPLEX
(X,f2) /. c is complex Element of COMPLEX
(f1 /. c) * ((X,f2) /. c) is complex Element of COMPLEX
((Y /. c) * ((X,C) /. c)) * ((f1 /. c) * ((X,f2) /. c)) is complex Element of COMPLEX
((X,C) /. c) * ((X,f2) /. c) is complex Element of COMPLEX
(f1 /. c) * (((X,C) /. c) * ((X,f2) /. c)) is complex Element of COMPLEX
(Y /. c) * ((f1 /. c) * (((X,C) /. c) * ((X,f2) /. c))) is complex Element of COMPLEX
((X,C) (#) (X,f2)) /. c is complex Element of COMPLEX
(f1 /. c) * (((X,C) (#) (X,f2)) /. c) is complex Element of COMPLEX
(Y /. c) * ((f1 /. c) * (((X,C) (#) (X,f2)) /. c)) is complex Element of COMPLEX
(Y /. c) * (f1 /. c) is complex Element of COMPLEX
((Y /. c) * (f1 /. c)) * (((X,C) (#) (X,f2)) /. c) is complex Element of COMPLEX
(X,(C (#) f2)) /. c is complex Element of COMPLEX
((Y /. c) * (f1 /. c)) * ((X,(C (#) f2)) /. c) is complex Element of COMPLEX
(Y (#) f1) /. c is complex Element of COMPLEX
((Y (#) f1) /. c) * ((X,(C (#) f2)) /. c) is complex Element of COMPLEX
((Y (#) f1) (#) (X,(C (#) f2))) /. c is complex Element of COMPLEX
(X,(Y (#) f1),(C (#) f2)) /. c is complex Element of COMPLEX
dom C is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
(dom Y) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
((dom Y) /\ ((dom C) \ (C " {0c}))) /\ (dom (X,f1,f2)) is Element of K19(X)
dom f2 is Element of K19(X)
f2 " {0c} is Element of K19(X)
(dom f2) \ (f2 " {0c}) is Element of K19(X)
(dom f1) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
((dom Y) /\ ((dom C) \ (C " {0c}))) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
((dom C) \ (C " {0c})) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom Y) /\ (((dom C) \ (C " {0c})) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
(dom f1) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom Y) /\ ((dom f1) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
((dom Y) /\ (dom f1)) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom (Y (#) f1)) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
dom (C (#) f2) is Element of K19(X)
(C (#) f2) " {0c} is Element of K19(X)
(dom (C (#) f2)) \ ((C (#) f2) " {0c}) is Element of K19(X)
(dom (Y (#) f1)) /\ ((dom (C (#) f2)) \ ((C (#) f2) " {0c})) is Element of K19(X)
dom (X,(Y (#) f1),(C (#) f2)) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(X,Y,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,C) is Element of K19(X)
K19(X) is set
C | (dom (X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(C | (dom (X,C))),Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(Y (#) (X,C))) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) (#) (X,(X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(C | (dom (X,C))) (#) (X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(Y (#) C),f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) (X,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (C (#) (X,f1)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) C) (#) (X,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,(X,C,f1)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,f1) is Element of K19(X)
K19(X) is set
f1 | (dom (X,f1)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (f1 | (dom (X,f1))) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(Y (#) (f1 | (dom (X,f1)))),C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(X,C,f1)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,(X,C,f1)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(f1 | (dom (X,f1))),C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,(f1 | (dom (X,f1))),C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) Y is V1() Function-like set
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(- 1) (#) (X,Y,C) is V1() Function-like set
(X,(- Y),C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(- 1) (#) C is V1() Function-like set
(X,Y,(- C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(- 1r) (#) (X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(- C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,(- C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(- 1r) (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) ((- 1r) (#) (X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (Y (#) (X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(- 1) (#) (Y (#) (X,C)) is V1() Function-like set
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) + (X,f1,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(Y + f1),C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) - (X,f1,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (X,f1,C) is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) (X,f1,C) is V1() Function-like set
(X,Y,C) + (- (X,f1,C)) is V1() Function-like set
Y - f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- f1 is V1() Function-like V38() set
(- 1) (#) f1 is V1() Function-like set
Y + (- f1) is V1() Function-like set
(X,(Y - f1),C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) (X,C)) + (X,f1,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) (X,C)) + (f1 (#) (X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y + f1) (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) (X,C)) - (X,f1,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) (X,C)) + (- (X,f1,C)) is V1() Function-like set
(Y (#) (X,C)) - (f1 (#) (X,C)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (f1 (#) (X,C)) is V1() Function-like V38() set
(- 1) (#) (f1 (#) (X,C)) is V1() Function-like set
(Y (#) (X,C)) + (- (f1 (#) (X,C))) is V1() Function-like set
(Y - f1) (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) + (X,f1,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) f2) + (f1 (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,((Y (#) f2) + (f1 (#) C)),(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,C) is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
c is Element of X
dom ((X,Y,C) + (X,f1,f2)) is Element of K19(X)
dom (X,Y,C) is Element of K19(X)
dom (X,f1,f2) is Element of K19(X)
(dom (X,Y,C)) /\ (dom (X,f1,f2)) is Element of K19(X)
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (Y (#) (X,C)) is Element of K19(X)
(dom (Y (#) (X,C))) /\ (dom (X,f1,f2)) is Element of K19(X)
dom Y is Element of K19(X)
(dom Y) /\ (dom (X,C)) is Element of K19(X)
C /. c is complex Element of COMPLEX
0c is complex Element of COMPLEX
(X,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) (X,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (f1 (#) (X,f2)) is Element of K19(X)
(dom (Y (#) (X,C))) /\ (dom (f1 (#) (X,f2))) is Element of K19(X)
dom f1 is Element of K19(X)
dom (X,f2) is Element of K19(X)
(dom f1) /\ (dom (X,f2)) is Element of K19(X)
f2 /. c is complex Element of COMPLEX
(dom f1) /\ (dom C) is Element of K19(X)
dom (f1 (#) C) is Element of K19(X)
dom f2 is Element of K19(X)
(dom C) /\ (dom f2) is Element of K19(X)
dom (C (#) f2) is Element of K19(X)
(dom Y) /\ (dom f2) is Element of K19(X)
dom (Y (#) f2) is Element of K19(X)
(dom (Y (#) f2)) /\ (dom (f1 (#) C)) is Element of K19(X)
dom ((Y (#) f2) + (f1 (#) C)) is Element of K19(X)
(dom (X,C)) /\ (dom (X,f2)) is Element of K19(X)
(X,C) (#) (X,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom ((X,C) (#) (X,f2)) is Element of K19(X)
(X,(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,(C (#) f2)) is Element of K19(X)
(dom ((Y (#) f2) + (f1 (#) C))) /\ (dom (X,(C (#) f2))) is Element of K19(X)
((Y (#) f2) + (f1 (#) C)) (#) (X,(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (((Y (#) f2) + (f1 (#) C)) (#) (X,(C (#) f2))) is Element of K19(X)
dom (X,((Y (#) f2) + (f1 (#) C)),(C (#) f2)) is Element of K19(X)
((X,Y,C) + (X,f1,f2)) /. c is complex Element of COMPLEX
(X,Y,C) /. c is complex Element of COMPLEX
(X,f1,f2) /. c is complex Element of COMPLEX
((X,Y,C) /. c) + ((X,f1,f2) /. c) is complex Element of COMPLEX
Y /. c is complex Element of COMPLEX
(C /. c) " is complex Element of COMPLEX
(Y /. c) * ((C /. c) ") is complex Element of COMPLEX
((Y /. c) * ((C /. c) ")) + ((X,f1,f2) /. c) is complex Element of COMPLEX
1r * ((C /. c) ") is complex Element of COMPLEX
(Y /. c) * (1r * ((C /. c) ")) is complex Element of COMPLEX
f1 /. c is complex Element of COMPLEX
(f1 /. c) * 1r is complex Element of COMPLEX
(f2 /. c) " is complex Element of COMPLEX
((f1 /. c) * 1r) * ((f2 /. c) ") is complex Element of COMPLEX
((Y /. c) * (1r * ((C /. c) "))) + (((f1 /. c) * 1r) * ((f2 /. c) ")) is complex Element of COMPLEX
(f2 /. c) * ((f2 /. c) ") is complex Element of COMPLEX
((f2 /. c) * ((f2 /. c) ")) * ((C /. c) ") is complex Element of COMPLEX
(Y /. c) * (((f2 /. c) * ((f2 /. c) ")) * ((C /. c) ")) is complex Element of COMPLEX
1r * ((f2 /. c) ") is complex Element of COMPLEX
(f1 /. c) * (1r * ((f2 /. c) ")) is complex Element of COMPLEX
((Y /. c) * (((f2 /. c) * ((f2 /. c) ")) * ((C /. c) "))) + ((f1 /. c) * (1r * ((f2 /. c) "))) is complex Element of COMPLEX
((f2 /. c) ") * ((C /. c) ") is complex Element of COMPLEX
(f2 /. c) * (((f2 /. c) ") * ((C /. c) ")) is complex Element of COMPLEX
(Y /. c) * ((f2 /. c) * (((f2 /. c) ") * ((C /. c) "))) is complex Element of COMPLEX
(C /. c) * ((C /. c) ") is complex Element of COMPLEX
((C /. c) * ((C /. c) ")) * ((f2 /. c) ") is complex Element of COMPLEX
(f1 /. c) * (((C /. c) * ((C /. c) ")) * ((f2 /. c) ")) is complex Element of COMPLEX
((Y /. c) * ((f2 /. c) * (((f2 /. c) ") * ((C /. c) ")))) + ((f1 /. c) * (((C /. c) * ((C /. c) ")) * ((f2 /. c) "))) is complex Element of COMPLEX
(f2 /. c) * (C /. c) is complex Element of COMPLEX
((f2 /. c) * (C /. c)) " is complex Element of COMPLEX
(f2 /. c) * (((f2 /. c) * (C /. c)) ") is complex Element of COMPLEX
(Y /. c) * ((f2 /. c) * (((f2 /. c) * (C /. c)) ")) is complex Element of COMPLEX
((C /. c) ") * ((f2 /. c) ") is complex Element of COMPLEX
(C /. c) * (((C /. c) ") * ((f2 /. c) ")) is complex Element of COMPLEX
(f1 /. c) * ((C /. c) * (((C /. c) ") * ((f2 /. c) "))) is complex Element of COMPLEX
((Y /. c) * ((f2 /. c) * (((f2 /. c) * (C /. c)) "))) + ((f1 /. c) * ((C /. c) * (((C /. c) ") * ((f2 /. c) ")))) is complex Element of COMPLEX
(C /. c) * (f2 /. c) is complex Element of COMPLEX
((C /. c) * (f2 /. c)) " is complex Element of COMPLEX
(f2 /. c) * (((C /. c) * (f2 /. c)) ") is complex Element of COMPLEX
(Y /. c) * ((f2 /. c) * (((C /. c) * (f2 /. c)) ")) is complex Element of COMPLEX
(C /. c) * (((C /. c) * (f2 /. c)) ") is complex Element of COMPLEX
(f1 /. c) * ((C /. c) * (((C /. c) * (f2 /. c)) ")) is complex Element of COMPLEX
((Y /. c) * ((f2 /. c) * (((C /. c) * (f2 /. c)) "))) + ((f1 /. c) * ((C /. c) * (((C /. c) * (f2 /. c)) "))) is complex Element of COMPLEX
(C (#) f2) /. c is complex Element of COMPLEX
((C (#) f2) /. c) " is complex Element of COMPLEX
(f2 /. c) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
(Y /. c) * ((f2 /. c) * (((C (#) f2) /. c) ")) is complex Element of COMPLEX
((Y /. c) * ((f2 /. c) * (((C (#) f2) /. c) "))) + ((f1 /. c) * ((C /. c) * (((C /. c) * (f2 /. c)) "))) is complex Element of COMPLEX
(Y /. c) * (f2 /. c) is complex Element of COMPLEX
((Y /. c) * (f2 /. c)) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
(C /. c) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
(f1 /. c) * ((C /. c) * (((C (#) f2) /. c) ")) is complex Element of COMPLEX
(((Y /. c) * (f2 /. c)) * (((C (#) f2) /. c) ")) + ((f1 /. c) * ((C /. c) * (((C (#) f2) /. c) "))) is complex Element of COMPLEX
(Y (#) f2) /. c is complex Element of COMPLEX
((Y (#) f2) /. c) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
(f1 /. c) * (C /. c) is complex Element of COMPLEX
((f1 /. c) * (C /. c)) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
(((Y (#) f2) /. c) * (((C (#) f2) /. c) ")) + (((f1 /. c) * (C /. c)) * (((C (#) f2) /. c) ")) is complex Element of COMPLEX
(f1 (#) C) /. c is complex Element of COMPLEX
((f1 (#) C) /. c) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
(((Y (#) f2) /. c) * (((C (#) f2) /. c) ")) + (((f1 (#) C) /. c) * (((C (#) f2) /. c) ")) is complex Element of COMPLEX
((Y (#) f2) /. c) + ((f1 (#) C) /. c) is complex Element of COMPLEX
(((Y (#) f2) /. c) + ((f1 (#) C) /. c)) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
((Y (#) f2) + (f1 (#) C)) /. c is complex Element of COMPLEX
(((Y (#) f2) + (f1 (#) C)) /. c) * (((C (#) f2) /. c) ") is complex Element of COMPLEX
(X,((Y (#) f2) + (f1 (#) C)),(C (#) f2)) /. c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(X)
(dom C) \ (C " {0c}) is Element of K19(X)
(dom Y) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
((dom Y) /\ ((dom C) \ (C " {0c}))) /\ (dom (X,f1,f2)) is Element of K19(X)
f2 " {0c} is Element of K19(X)
(dom f2) \ (f2 " {0c}) is Element of K19(X)
(dom f1) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
((dom Y) /\ ((dom C) \ (C " {0c}))) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom C) /\ ((dom C) \ (C " {0c})) is Element of K19(X)
(dom Y) /\ ((dom C) /\ ((dom C) \ (C " {0c}))) is Element of K19(X)
((dom Y) /\ ((dom C) /\ ((dom C) \ (C " {0c})))) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
((dom C) /\ ((dom C) \ (C " {0c}))) /\ (dom Y) is Element of K19(X)
(dom f2) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
((dom f2) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1) is Element of K19(X)
(((dom C) /\ ((dom C) \ (C " {0c}))) /\ (dom Y)) /\ (((dom f2) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1)) is Element of K19(X)
(dom Y) /\ (((dom f2) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1)) is Element of K19(X)
((dom C) /\ ((dom C) \ (C " {0c}))) /\ ((dom Y) /\ (((dom f2) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1))) is Element of K19(X)
(dom Y) /\ ((dom f2) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
((dom Y) /\ ((dom f2) /\ ((dom f2) \ (f2 " {0c})))) /\ (dom f1) is Element of K19(X)
((dom C) /\ ((dom C) \ (C " {0c}))) /\ (((dom Y) /\ ((dom f2) /\ ((dom f2) \ (f2 " {0c})))) /\ (dom f1)) is Element of K19(X)
((dom Y) /\ (dom f2)) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
(((dom Y) /\ (dom f2)) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1) is Element of K19(X)
((dom C) /\ ((dom C) \ (C " {0c}))) /\ ((((dom Y) /\ (dom f2)) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1)) is Element of K19(X)
(dom (Y (#) f2)) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
((dom (Y (#) f2)) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1) is Element of K19(X)
((dom C) /\ ((dom C) \ (C " {0c}))) /\ (((dom (Y (#) f2)) /\ ((dom f2) \ (f2 " {0c}))) /\ (dom f1)) is Element of K19(X)
(dom (Y (#) f2)) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
((dom C) /\ ((dom C) \ (C " {0c}))) /\ ((dom (Y (#) f2)) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
((dom C) \ (C " {0c})) /\ (dom C) is Element of K19(X)
(((dom C) \ (C " {0c})) /\ (dom C)) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom (Y (#) f2)) /\ ((((dom C) \ (C " {0c})) /\ (dom C)) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
(dom C) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
((dom C) \ (C " {0c})) /\ ((dom C) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
(dom (Y (#) f2)) /\ (((dom C) \ (C " {0c})) /\ ((dom C) /\ ((dom f1) /\ ((dom f2) \ (f2 " {0c}))))) is Element of K19(X)
((dom f1) /\ (dom C)) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
((dom C) \ (C " {0c})) /\ (((dom f1) /\ (dom C)) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom (Y (#) f2)) /\ (((dom C) \ (C " {0c})) /\ (((dom f1) /\ (dom C)) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
(dom (f1 (#) C)) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
((dom C) \ (C " {0c})) /\ ((dom (f1 (#) C)) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom (Y (#) f2)) /\ (((dom C) \ (C " {0c})) /\ ((dom (f1 (#) C)) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c})) is Element of K19(X)
(dom (f1 (#) C)) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom (Y (#) f2)) /\ ((dom (f1 (#) C)) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c})))) is Element of K19(X)
((dom (Y (#) f2)) /\ (dom (f1 (#) C))) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(dom ((Y (#) f2) + (f1 (#) C))) /\ (((dom C) \ (C " {0c})) /\ ((dom f2) \ (f2 " {0c}))) is Element of K19(X)
(C (#) f2) " {0c} is Element of K19(X)
(dom (C (#) f2)) \ ((C (#) f2) " {0c}) is Element of K19(X)
(dom ((Y (#) f2) + (f1 (#) C))) /\ ((dom (C (#) f2)) \ ((C (#) f2) " {0c})) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(X,Y,C),(X,f1,f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom (X,f2) is Element of K19(X)
K19(X) is set
f2 | (dom (X,f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (f2 | (dom (X,f2))) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(Y (#) (f2 | (dom (X,f2)))),(C (#) f1)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(X,f1,f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) (#) (X,(X,f1,f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,(f2 | (dom (X,f2))),f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) (#) (X,(f2 | (dom (X,f2))),f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f1 (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) - (X,f1,f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (X,f1,f2) is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) (X,f1,f2) is V1() Function-like set
(X,Y,C) + (- (X,f1,f2)) is V1() Function-like set
Y (#) f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) f2) - (f1 (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- (f1 (#) C) is V1() Function-like V38() set
(- 1) (#) (f1 (#) C) is V1() Function-like set
(Y (#) f2) + (- (f1 (#) C)) is V1() Function-like set
C (#) f2 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,((Y (#) f2) - (f1 (#) C)),(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(- 1r) (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,((- 1r) (#) f1),f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) + (X,((- 1r) (#) f1),f2) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
((- 1r) (#) f1) (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(Y (#) f2) + (((- 1r) (#) f1) (#) C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,((Y (#) f2) + (((- 1r) (#) f1) (#) C)),(C (#) f2)) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.(X,Y,C).| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.C.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.Y.| / |.C.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.(Y (#) (X,C)).| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.(X,C).| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.Y.| (#) |.(X,C).| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.C.| ^ is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
|.Y.| (#) (|.C.| ^) is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C + f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C + f1) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) + (f1 | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) + f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C + (f1 | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f2 is Element of Y
dom ((C + f1) | X) is Element of K19(Y)
K19(Y) is set
dom (C + f1) is Element of K19(Y)
(dom (C + f1)) /\ X is Element of K19(Y)
dom C is Element of K19(Y)
dom f1 is Element of K19(Y)
(dom C) /\ (dom f1) is Element of K19(Y)
(dom f1) /\ X is Element of K19(Y)
dom (f1 | X) is Element of K19(Y)
(dom C) /\ X is Element of K19(Y)
dom (C | X) is Element of K19(Y)
(dom (C | X)) /\ (dom (f1 | X)) is Element of K19(Y)
dom ((C | X) + (f1 | X)) is Element of K19(Y)
((C + f1) | X) /. f2 is complex Element of COMPLEX
(C + f1) /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) + (f1 /. f2) is complex Element of COMPLEX
(C | X) /. f2 is complex Element of COMPLEX
((C | X) /. f2) + (f1 /. f2) is complex Element of COMPLEX
(f1 | X) /. f2 is complex Element of COMPLEX
((C | X) /. f2) + ((f1 | X) /. f2) is complex Element of COMPLEX
((C | X) + (f1 | X)) /. f2 is complex Element of COMPLEX
X /\ X is set
((dom C) /\ (dom f1)) /\ (X /\ X) is Element of K19(Y)
(dom f1) /\ (X /\ X) is Element of K19(Y)
(dom C) /\ ((dom f1) /\ (X /\ X)) is Element of K19(Y)
((dom f1) /\ X) /\ X is Element of K19(Y)
(dom C) /\ (((dom f1) /\ X) /\ X) is Element of K19(Y)
X /\ (dom (f1 | X)) is Element of K19(Y)
(dom C) /\ (X /\ (dom (f1 | X))) is Element of K19(Y)
((dom C) /\ X) /\ (dom (f1 | X)) is Element of K19(Y)
f2 is Element of Y
(dom (C | X)) /\ (dom f1) is Element of K19(Y)
dom ((C | X) + f1) is Element of K19(Y)
((C + f1) | X) /. f2 is complex Element of COMPLEX
(C + f1) /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) + (f1 /. f2) is complex Element of COMPLEX
(C | X) /. f2 is complex Element of COMPLEX
((C | X) /. f2) + (f1 /. f2) is complex Element of COMPLEX
((C | X) + f1) /. f2 is complex Element of COMPLEX
((dom C) /\ (dom f1)) /\ X is Element of K19(Y)
((dom C) /\ X) /\ (dom f1) is Element of K19(Y)
f2 is Element of Y
(dom C) /\ (dom (f1 | X)) is Element of K19(Y)
dom (C + (f1 | X)) is Element of K19(Y)
((C + f1) | X) /. f2 is complex Element of COMPLEX
(C + f1) /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) + (f1 /. f2) is complex Element of COMPLEX
(f1 | X) /. f2 is complex Element of COMPLEX
(C /. f2) + ((f1 | X) /. f2) is complex Element of COMPLEX
(C + (f1 | X)) /. f2 is complex Element of COMPLEX
(dom C) /\ ((dom f1) /\ X) is Element of K19(Y)
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C (#) f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C (#) f1) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) (#) (f1 | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) (#) f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C (#) (f1 | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f2 is Element of Y
dom ((C (#) f1) | X) is Element of K19(Y)
K19(Y) is set
dom (C (#) f1) is Element of K19(Y)
(dom (C (#) f1)) /\ X is Element of K19(Y)
dom C is Element of K19(Y)
dom f1 is Element of K19(Y)
(dom C) /\ (dom f1) is Element of K19(Y)
(dom f1) /\ X is Element of K19(Y)
dom (f1 | X) is Element of K19(Y)
(dom C) /\ X is Element of K19(Y)
dom (C | X) is Element of K19(Y)
(dom (C | X)) /\ (dom (f1 | X)) is Element of K19(Y)
dom ((C | X) (#) (f1 | X)) is Element of K19(Y)
((C (#) f1) | X) /. f2 is complex Element of COMPLEX
(C (#) f1) /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) * (f1 /. f2) is complex Element of COMPLEX
(C | X) /. f2 is complex Element of COMPLEX
((C | X) /. f2) * (f1 /. f2) is complex Element of COMPLEX
(f1 | X) /. f2 is complex Element of COMPLEX
((C | X) /. f2) * ((f1 | X) /. f2) is complex Element of COMPLEX
((C | X) (#) (f1 | X)) /. f2 is complex Element of COMPLEX
X /\ X is set
((dom C) /\ (dom f1)) /\ (X /\ X) is Element of K19(Y)
(dom f1) /\ (X /\ X) is Element of K19(Y)
(dom C) /\ ((dom f1) /\ (X /\ X)) is Element of K19(Y)
((dom f1) /\ X) /\ X is Element of K19(Y)
(dom C) /\ (((dom f1) /\ X) /\ X) is Element of K19(Y)
X /\ (dom (f1 | X)) is Element of K19(Y)
(dom C) /\ (X /\ (dom (f1 | X))) is Element of K19(Y)
((dom C) /\ X) /\ (dom (f1 | X)) is Element of K19(Y)
f2 is Element of Y
(dom (C | X)) /\ (dom f1) is Element of K19(Y)
dom ((C | X) (#) f1) is Element of K19(Y)
((C (#) f1) | X) /. f2 is complex Element of COMPLEX
(C (#) f1) /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) * (f1 /. f2) is complex Element of COMPLEX
(C | X) /. f2 is complex Element of COMPLEX
((C | X) /. f2) * (f1 /. f2) is complex Element of COMPLEX
((C | X) (#) f1) /. f2 is complex Element of COMPLEX
((dom C) /\ (dom f1)) /\ X is Element of K19(Y)
((dom C) /\ X) /\ (dom f1) is Element of K19(Y)
f2 is Element of Y
(dom C) /\ (dom (f1 | X)) is Element of K19(Y)
dom (C (#) (f1 | X)) is Element of K19(Y)
((C (#) f1) | X) /. f2 is complex Element of COMPLEX
(C (#) f1) /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 /. f2 is complex Element of COMPLEX
(C /. f2) * (f1 /. f2) is complex Element of COMPLEX
(f1 | X) /. f2 is complex Element of COMPLEX
(C /. f2) * ((f1 | X) /. f2) is complex Element of COMPLEX
(C (#) (f1 | X)) /. f2 is complex Element of COMPLEX
(dom C) /\ ((dom f1) /\ X) is Element of K19(Y)
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
(- C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- (C | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(- 1) (#) (C | X) is V1() Function-like set
(Y,C) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,(C | X)) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
|.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V38() V39() V40() set
K19(K20(Y,REAL)) is set
|.C.| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
|.(C | X).| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
dom ((Y,C) | X) is Element of K19(Y)
K19(Y) is set
dom (Y,C) is Element of K19(Y)
(dom (Y,C)) /\ X is Element of K19(Y)
dom C is Element of K19(Y)
0c is complex Element of COMPLEX
{0c} is V48() set
C " {0c} is Element of K19(Y)
(dom C) \ (C " {0c}) is Element of K19(Y)
((dom C) \ (C " {0c})) /\ X is Element of K19(Y)
(dom C) /\ X is Element of K19(Y)
(C " {0c}) /\ X is Element of K19(Y)
((dom C) /\ X) \ ((C " {0c}) /\ X) is Element of K19(Y)
dom (C | X) is Element of K19(Y)
X /\ (C " {0c}) is Element of K19(Y)
(dom (C | X)) \ (X /\ (C " {0c})) is Element of K19(Y)
(C | X) " {0c} is Element of K19(Y)
(dom (C | X)) \ ((C | X) " {0c}) is Element of K19(Y)
dom (Y,(C | X)) is Element of K19(Y)
f1 is Element of Y
dom ((- C) | X) is Element of K19(Y)
dom (- C) is Element of K19(Y)
(dom (- C)) /\ X is Element of K19(Y)
dom (- (C | X)) is Element of K19(Y)
((- C) | X) /. f1 is complex Element of COMPLEX
(- C) /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
- (C /. f1) is complex Element of COMPLEX
(C | X) /. f1 is complex Element of COMPLEX
- ((C | X) /. f1) is complex Element of COMPLEX
(- (C | X)) /. f1 is complex Element of COMPLEX
f1 is Element of Y
((Y,C) | X) /. f1 is complex Element of COMPLEX
(Y,C) /. f1 is complex Element of COMPLEX
C /. f1 is complex Element of COMPLEX
(C /. f1) " is complex Element of COMPLEX
(C | X) /. f1 is complex Element of COMPLEX
((C | X) /. f1) " is complex Element of COMPLEX
(Y,(C | X)) /. f1 is complex Element of COMPLEX
dom (|.C.| | X) is Element of K19(Y)
dom |.C.| is Element of K19(Y)
(dom |.C.|) /\ X is Element of K19(Y)
dom |.(C | X).| is Element of K19(Y)
f1 is Element of Y
(|.C.| | X) . f1 is ext-real complex real set
|.C.| . f1 is ext-real complex real set
C . f1 is complex set
|.(C . f1).| is ext-real complex real Element of REAL
C /. f1 is complex Element of COMPLEX
|.(C /. f1).| is ext-real complex real Element of REAL
(C | X) /. f1 is complex Element of COMPLEX
|.((C | X) /. f1).| is ext-real complex real Element of REAL
(C | X) . f1 is complex set
|.((C | X) . f1).| is ext-real complex real Element of REAL
|.(C | X).| . f1 is ext-real complex real set
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C - f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- f1 is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) f1 is V1() Function-like set
C + (- f1) is V1() Function-like set
(C - f1) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) - (f1 | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- (f1 | X) is V1() Function-like V38() set
(- 1) (#) (f1 | X) is V1() Function-like set
(C | X) + (- (f1 | X)) is V1() Function-like set
(C | X) - f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) + (- f1) is V1() Function-like set
C - (f1 | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C + (- (f1 | X)) is V1() Function-like set
- f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(- f1) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) + ((- f1) | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) + (- f1) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C + ((- f1) | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,C,f1) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,C,f1) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,(C | X),(f1 | X)) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,(C | X),f1) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,C,(f1 | X)) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,f1) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C (#) (Y,f1) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C (#) (Y,f1)) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,f1) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) (#) ((Y,f1) | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(Y,(f1 | X)) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) (#) (Y,(f1 | X)) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(C | X) (#) (Y,f1) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C (#) ((Y,f1) | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C (#) (Y,(f1 | X)) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 is complex Element of COMPLEX
f1 (#) C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(f1 (#) C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 (#) (C | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f2 is Element of Y
dom ((f1 (#) C) | X) is Element of K19(Y)
K19(Y) is set
dom (f1 (#) C) is Element of K19(Y)
(dom (f1 (#) C)) /\ X is Element of K19(Y)
dom C is Element of K19(Y)
(dom C) /\ X is Element of K19(Y)
dom (C | X) is Element of K19(Y)
dom (f1 (#) (C | X)) is Element of K19(Y)
((f1 (#) C) | X) /. f2 is complex Element of COMPLEX
(f1 (#) C) /. f2 is complex Element of COMPLEX
C /. f2 is complex Element of COMPLEX
f1 * (C /. f2) is complex Element of COMPLEX
(C | X) /. f2 is complex Element of COMPLEX
f1 * ((C | X) /. f2) is complex Element of COMPLEX
(f1 (#) (C | X)) /. f2 is complex Element of COMPLEX
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y + C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y - C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
Y + (- C) is V1() Function-like set
Y (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (Y + C) is Element of K19(X)
X /\ X is set
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 is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (Y - C) is Element of K19(X)
X /\ X is set
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 is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (Y (#) C) is Element of K19(X)
X /\ X is set
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,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is complex Element of COMPLEX
C (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
dom Y is Element of K19(X)
K19(X) is set
dom (C (#) Y) is Element of K19(X)
dom (C (#) Y) is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) Y is V1() Function-like set
(- 1r) (#) Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
dom Y is Element of K19(X)
K19(X) is set
dom |.Y.| is Element of K19(X)
dom |.Y.| is Element of K19(X)
K19(X) is set
dom Y is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,Y) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y " {0} is Element of K19(X)
K19(X) is set
dom (X,Y) is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
Y " {0c} is Element of K19(X)
dom Y is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
(dom Y) \ {} is Element of K19(X)
dom (X,Y) is Element of K19(X)
dom Y is Element of K19(X)
0c is complex Element of COMPLEX
{0c} is V48() set
Y " {0c} is Element of K19(X)
(dom Y) \ (Y " {0c}) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C " {0} is Element of K19(X)
K19(X) is set
(X,Y,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
Y (#) (X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is Element of X
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C /. Y is complex Element of COMPLEX
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C + f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(C + f1) /. Y is complex Element of COMPLEX
f1 /. Y is complex Element of COMPLEX
(C /. Y) + (f1 /. Y) is complex Element of COMPLEX
C - f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- f1 is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) f1 is V1() Function-like set
C + (- f1) is V1() Function-like set
(C - f1) /. Y is complex Element of COMPLEX
(C /. Y) - (f1 /. Y) is complex Element of COMPLEX
C (#) f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(C (#) f1) /. Y is complex Element of COMPLEX
(C /. Y) * (f1 /. Y) is complex Element of COMPLEX
dom (C + f1) is Element of K19(X)
K19(X) is set
dom (C - f1) is Element of K19(X)
dom (C (#) f1) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is Element of X
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C /. Y is complex Element of COMPLEX
f1 is complex Element of COMPLEX
f1 (#) C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(f1 (#) C) /. Y is complex Element of COMPLEX
f1 * (C /. Y) is complex Element of COMPLEX
dom (f1 (#) C) is Element of K19(X)
K19(X) is set
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is Element of X
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
(- C) /. Y is complex Element of COMPLEX
C /. Y is complex Element of COMPLEX
- (C /. Y) is complex Element of COMPLEX
|.C.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
|.C.| . Y is ext-real complex real set
|.(C /. Y).| is ext-real complex real Element of REAL
dom |.C.| is Element of K19(X)
K19(X) is set
dom C is Element of K19(X)
dom (- C) is Element of K19(X)
C . Y is complex set
|.(C . Y).| is ext-real complex real Element of REAL
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is Element of X
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C) /. Y is complex Element of COMPLEX
C /. Y is complex Element of COMPLEX
(C /. Y) " is complex Element of COMPLEX
dom (X,C) is Element of K19(X)
K19(X) is set
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is Element of X
C is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
C /. Y is complex Element of COMPLEX
f1 is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C,f1) is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
(X,C,f1) /. Y is complex Element of COMPLEX
f1 /. Y is complex Element of COMPLEX
(f1 /. Y) " is complex Element of COMPLEX
(C /. Y) * ((f1 /. Y) ") is complex Element of COMPLEX
0c is complex Element of COMPLEX
{0c} is V48() set
f1 " {0c} is Element of K19(X)
K19(X) is set
dom (X,C,f1) is Element of K19(X)
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
dom Y is Element of K19(X)
K19(X) is set
dom |.Y.| is Element of K19(X)
C is ext-real complex real set
K104(Y) is set
f1 is set
Y . f1 is complex set
abs (Y . f1) is ext-real complex real Element of REAL
|.Y.| . f1 is ext-real complex real set
abs (|.Y.| . f1) is ext-real complex real Element of REAL
|.(Y . f1).| is ext-real complex real Element of REAL
abs |.(Y . f1).| is ext-real complex real Element of REAL
C is ext-real complex real set
f2 is set
f1 is ext-real complex real set
Y . f2 is complex set
|.(Y . f2).| is ext-real complex real Element of REAL
abs |.(Y . f2).| is ext-real complex real Element of REAL
|.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 set
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
dom C is Element of K19(Y)
K19(Y) is set
X /\ (dom C) is Element of K19(Y)
|.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V38() V39() V40() set
K19(K20(Y,REAL)) is set
dom |.C.| is Element of K19(Y)
|.C.| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
dom (|.C.| | X) is Element of K19(Y)
X /\ (dom |.C.|) is Element of K19(Y)
|.(C | X).| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
f1 is ext-real complex real set
f2 is Element of Y
C . f2 is complex set
C /. f2 is complex Element of COMPLEX
(|.C.| | X) . f2 is ext-real complex real set
abs ((|.C.| | X) . f2) is ext-real complex real Element of REAL
|.C.| . f2 is ext-real complex real set
abs (|.C.| . f2) is ext-real complex real Element of REAL
|.(C . f2).| is ext-real complex real Element of REAL
abs |.(C . f2).| is ext-real complex real Element of REAL
|.(C /. f2).| is ext-real complex real Element of REAL
f1 is ext-real complex real set
f2 is set
(|.C.| | X) . f2 is ext-real complex real set
abs ((|.C.| | X) . f2) is ext-real complex real Element of REAL
|.C.| . f2 is ext-real complex real set
abs (|.C.| . f2) is ext-real complex real Element of REAL
C . f2 is complex set
|.(C . f2).| is ext-real complex real Element of REAL
abs |.(C . f2).| is ext-real complex real Element of REAL
C /. f2 is complex Element of COMPLEX
|.(C /. f2).| is ext-real complex real Element of REAL
abs |.(C /. f2).| is ext-real complex real Element of REAL
X is set
Y is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | X is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
|.f1.| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
K20(C,REAL) is V38() V39() V40() set
K19(K20(C,REAL)) is set
|.f1.| | Y is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.(f1 | Y).| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.f1.| | X is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.(f1 | X).| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
dom C is Element of K19(Y)
K19(Y) is set
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
X /\ (dom C) is Element of K19(Y)
f1 is Element of Y
C /. f1 is complex Element of COMPLEX
|.(C /. f1).| is ext-real complex real Element of REAL
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 is complex Element of COMPLEX
f1 (#) C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(f1 (#) C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
|.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V38() V39() V40() set
K19(K20(Y,REAL)) is set
|.C.| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
|.(C | X).| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
|.f1.| is ext-real complex real Element of REAL
|.f1.| (#) |.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
(|.f1.| (#) |.C.|) | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
|.(f1 (#) C).| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
|.(f1 (#) C).| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
|.((f1 (#) C) | X).| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
|.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V38() V39() V40() set
K19(K20(Y,REAL)) is set
|.C.| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
f1 is ext-real natural complex real V36() V37() V48() V49() V50() V51() V52() V53() Element of NAT
f2 is set
C /. f2 is complex Element of COMPLEX
|.(C /. f2).| is ext-real complex real Element of REAL
dom |.C.| is Element of K19(Y)
K19(Y) is set
X /\ (dom |.C.|) is Element of K19(Y)
dom C is Element of K19(Y)
C . f2 is complex set
|.C.| . f2 is ext-real complex real set
f1 is ext-real natural complex real V36() V37() V48() V49() V50() V51() V52() V53() Element of NAT
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
|.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V38() V39() V40() set
K19(K20(Y,REAL)) is set
|.C.| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
- C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
(- C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
|.(C | X).| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
(- 1r) (#) (C | X) is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(- 1r) (#) C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
((- 1r) (#) C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | X is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 + f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(f1 + f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
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 set
dom f2 is Element of K19(C)
Y /\ (dom f2) is Element of K19(C)
cr2 is ext-real complex real set
dom (f1 + f2) is Element of K19(C)
(X /\ Y) /\ (dom (f1 + f2)) is Element of K19(C)
c + cr2 is ext-real complex real set
c is ext-real complex real set
c is Element of C
(f1 + f2) /. c is complex Element of COMPLEX
|.((f1 + f2) /. c).| is ext-real complex real Element of REAL
f1 /. c is complex Element of COMPLEX
f2 /. c is complex Element of COMPLEX
(f1 /. c) + (f2 /. c) is complex Element of COMPLEX
|.((f1 /. c) + (f2 /. c)).| is ext-real complex real Element of REAL
|.(f1 /. c).| is ext-real complex real Element of REAL
|.(f2 /. c).| is ext-real complex real Element of REAL
|.(f1 /. c).| + |.(f2 /. c).| is ext-real complex real set
(dom f1) /\ (dom f2) is Element of K19(C)
c is ext-real complex real set
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | X is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 (#) f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(f1 (#) f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 - f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
- f2 is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) f2 is V1() Function-like set
f1 + (- f2) is V1() Function-like set
(f1 - f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
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 set
dom f2 is Element of K19(C)
Y /\ (dom f2) is Element of K19(C)
cr2 is ext-real complex real set
c * cr2 is ext-real complex real set
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 /. c is complex Element of COMPLEX
|.(f1 /. c).| is ext-real complex real Element of REAL
f2 /. c is complex Element of COMPLEX
|.(f2 /. c).| is ext-real complex real Element of REAL
|.(f1 /. c).| * |.(f2 /. c).| is ext-real complex real set
c is ext-real complex real set
(f1 /. c) * (f2 /. c) is complex Element of COMPLEX
|.((f1 /. c) * (f2 /. c)).| is ext-real complex real Element of REAL
(f1 (#) f2) /. c is complex Element of COMPLEX
|.((f1 (#) f2) /. c).| is ext-real complex real Element of REAL
c is ext-real complex real set
- f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(- f2) | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
X is set
Y is set
X \/ Y is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | X is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | (X \/ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
|.f1.| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
K20(C,REAL) is V38() V39() V40() set
K19(K20(C,REAL)) is set
|.f1.| | Y is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.(f1 | Y).| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.f1.| | X is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.(f1 | X).| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.f1.| | (X \/ Y) is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
|.(f1 | (X \/ Y)).| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | X is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 + f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(f1 + f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 - f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
- f2 is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) f2 is V1() Function-like set
f1 + (- f2) is V1() Function-like set
(f1 - f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 (#) f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(f1 (#) f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
dom f1 is Element of K19(C)
K19(C) is set
X /\ (dom f1) is Element of K19(C)
c is complex Element of COMPLEX
dom f2 is Element of K19(C)
Y /\ (dom f2) is Element of K19(C)
cr2 is complex Element of COMPLEX
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 complex Element of COMPLEX
f1 /. c is complex Element of COMPLEX
f2 /. c is complex Element of COMPLEX
(f1 /. c) + (f2 /. c) is complex Element of COMPLEX
c + (f2 /. c) is complex Element of COMPLEX
c + cr2 is complex Element of COMPLEX
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 complex Element of COMPLEX
f1 /. c is complex Element of COMPLEX
f2 /. c is complex Element of COMPLEX
(f1 /. c) - (f2 /. c) is complex Element of COMPLEX
c - (f2 /. c) is complex Element of COMPLEX
c - cr2 is complex Element of COMPLEX
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 complex Element of COMPLEX
f1 /. c is complex Element of COMPLEX
f2 /. c is complex Element of COMPLEX
(f1 /. c) * (f2 /. c) is complex Element of COMPLEX
c * (f2 /. c) is complex Element of COMPLEX
c * cr2 is complex Element of COMPLEX
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
f1 is complex Element of COMPLEX
f1 (#) C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(f1 (#) C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
dom C is Element of K19(Y)
K19(Y) is set
X /\ (dom C) is Element of K19(Y)
f2 is complex Element of COMPLEX
c is Element of Y
dom (f1 (#) C) is Element of K19(Y)
X /\ (dom (f1 (#) C)) is Element of K19(Y)
(f1 (#) C) /. c is complex Element of COMPLEX
C /. c is complex Element of COMPLEX
f1 * (C /. c) is complex Element of COMPLEX
f1 * f2 is complex Element of COMPLEX
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
|.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V38() V39() V40() set
K19(K20(Y,REAL)) is set
|.C.| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
- C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
(- C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
dom C is Element of K19(Y)
K19(Y) is set
X /\ (dom C) is Element of K19(Y)
f1 is complex Element of COMPLEX
f2 is Element of Y
dom |.C.| is Element of K19(Y)
X /\ (dom |.C.|) is Element of K19(Y)
C . f2 is complex set
C /. f2 is complex Element of COMPLEX
|.C.| . f2 is ext-real complex real set
|.(C /. f2).| is ext-real complex real Element of REAL
|.f1.| is ext-real complex real Element of REAL
- f1 is complex Element of COMPLEX
c is Element of Y
dom (- C) is Element of K19(Y)
X /\ (dom (- C)) is Element of K19(Y)
C /. c is complex Element of COMPLEX
- (C /. c) is complex Element of COMPLEX
f2 is complex Element of COMPLEX
(- C) /. c is complex Element of COMPLEX
f2 is complex Element of COMPLEX
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
dom C is Element of K19(Y)
K19(Y) is set
X /\ (dom C) is Element of K19(Y)
f1 is complex Element of COMPLEX
|.f1.| is ext-real complex real Element of REAL
c is Element of Y
C /. c is complex Element of COMPLEX
|.(C /. c).| is ext-real complex real Element of REAL
f2 is ext-real complex real Element of REAL
f2 is ext-real complex real Element of REAL
X is set
Y is non empty set
K20(Y,COMPLEX) is V38() set
K19(K20(Y,COMPLEX)) is set
C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
C | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
- 1 is ext-real complex real set
(- 1) (#) C is V1() Function-like set
(- C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
|.C.| is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
K20(Y,REAL) is V38() V39() V40() set
K19(K20(Y,REAL)) is set
|.C.| | X is V1() V4(Y) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(Y,REAL))
f1 is complex Element of COMPLEX
f1 (#) C is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
(f1 (#) C) | X is V1() V4(Y) V5( COMPLEX ) Function-like V38() Element of K19(K20(Y,COMPLEX))
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | X is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 + f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(f1 + f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
X is set
Y is set
X /\ Y is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 | X is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 - f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
- f2 is V1() Function-like V38() set
- 1 is ext-real complex real set
(- 1) (#) f2 is V1() Function-like set
f1 + (- f2) is V1() Function-like set
(f1 - f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f2 - f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
- f1 is V1() Function-like V38() set
(- 1) (#) f1 is V1() Function-like set
f2 + (- f1) is V1() Function-like set
(f2 - f1) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
f1 (#) f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(f1 (#) f2) | (X /\ Y) is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
- f2 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
(- f2) | Y is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
X is non empty set
K20(X,COMPLEX) is V38() set
K19(K20(X,COMPLEX)) is set
C is non empty set
K20(C,COMPLEX) is V38() set
K19(K20(C,COMPLEX)) is set
Y is V1() V4(X) V5( COMPLEX ) Function-like V38() Element of K19(K20(X,COMPLEX))
|.Y.| is V1() V4(X) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(X,REAL))
K20(X,REAL) is V38() V39() V40() set
K19(K20(X,REAL)) is set
f1 is V1() V4(C) V5( COMPLEX ) Function-like V38() Element of K19(K20(C,COMPLEX))
|.f1.| is V1() V4(C) V5( REAL ) Function-like V38() V39() V40() Element of K19(K20(C,REAL))
K20(C,REAL) is V38() V39() V40() set
K19(K20(C,REAL)) is set