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