:: INTEGR1C semantic presentation

REAL is non empty V39() V57() V58() V59() V63() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V58() set
[:NAT,ExtREAL:] is non empty Relation-like ext-real-valued set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
[:REAL,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() set
bool omega is non empty set
COMPLEX is non empty V39() V57() V63() set
RAT is non empty V39() V57() V58() V59() V60() V63() set
INT is non empty V39() V57() V58() V59() V60() V61() V63() set
bool NAT is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
{{},1} is non empty V57() V58() V59() V60() V61() V62() set
[:NAT,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
[:NAT,COMPLEX:] is non empty Relation-like complex-valued set
bool [:NAT,COMPLEX:] is non empty set
[:COMPLEX,COMPLEX:] is non empty Relation-like complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty set
K416() is L6()
the U1 of K416() is set
[:1,1:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
[:2,2:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is non empty set
K444() is V126() L7()
R^1 is V98() L6()
bool (bool REAL) is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative V37() V38() complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() Element of NAT
the U1 of R^1 is set
|.0.| is complex real ext-real V38() Element of REAL
<i> is complex Element of COMPLEX
sin is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of bool [:REAL,REAL:]
dom sin is non empty V57() V58() V59() Element of bool REAL
cos is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of bool [:REAL,REAL:]
dom cos is non empty V57() V58() V59() Element of bool REAL
bool the U1 of R^1 is non empty set
[:[:REAL,REAL:],COMPLEX:] is non empty Relation-like complex-valued set
bool [:[:REAL,REAL:],COMPLEX:] is non empty set
f is complex real ext-real Element of REAL
C is complex real ext-real Element of REAL
C * <i> is complex set
f + (C * <i>) is complex set
f is non empty Relation-like [:REAL,REAL:] -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of bool [:[:REAL,REAL:],COMPLEX:]
C is Element of [:REAL,REAL:]
C `1 is set
C `2 is set
C1 is complex real ext-real Element of REAL
C2 is complex real ext-real Element of REAL
f . ((C `1),(C `2)) is set
C2 * <i> is complex set
C1 + (C2 * <i>) is complex set
C is non empty Relation-like [:REAL,REAL:] -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of bool [:[:REAL,REAL:],COMPLEX:]
C1 is Element of [:REAL,REAL:]
C1 `1 is set
C1 `2 is set
C2 is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
[C2,a] is V24() set
C . [C2,a] is complex set
a * <i> is complex set
C2 + (a * <i>) is complex set
[C2,a] `1 is set
[C2,a] `2 is set
f . (C2,a) is complex Element of COMPLEX
C2 is complex real ext-real Element of REAL
C1 is Element of [:REAL,REAL:]
C1 `1 is set
a is complex real ext-real Element of REAL
C1 `2 is set
[C2,a] is V24() set
C . [C2,a] is complex set
a * <i> is complex set
C2 + (a * <i>) is complex set
f is non empty Relation-like [:REAL,REAL:] -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of bool [:[:REAL,REAL:],COMPLEX:]
C is non empty Relation-like [:REAL,REAL:] -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of bool [:[:REAL,REAL:],COMPLEX:]
C1 is set
f . C1 is complex set
C . C1 is complex set
C2 is set
a is set
[C2,a] is V24() set
C1 `1 is set
b is complex real ext-real Element of REAL
C1 `2 is set
d is complex real ext-real Element of REAL
d * <i> is complex set
b + (d * <i>) is complex set
() is non empty Relation-like [:REAL,REAL:] -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of bool [:[:REAL,REAL:],COMPLEX:]
C1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<:C1,C2:> is Relation-like Function-like set
b is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
Re b is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
[:COMPLEX,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty set
(Re b) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:C1,C2:> (#) ((Re b) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im b is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im b) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:C1,C2:> (#) ((Im b) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
f is complex real ext-real Element of REAL
C is complex real ext-real Element of REAL
a is V57() V58() V59() Element of bool REAL
C1 `| a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C2 `| a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
proj1 <:C1,C2:> is set
dom C1 is V57() V58() V59() Element of bool REAL
dom C2 is V57() V58() V59() Element of bool REAL
(dom C1) /\ (dom C2) is V57() V58() V59() Element of bool REAL
proj2 <:C1,C2:> is set
rng C1 is V57() V58() V59() Element of bool REAL
rng C2 is V57() V58() V59() Element of bool REAL
[:(rng C1),(rng C2):] is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
[:REAL,[:REAL,REAL:]:] is non empty Relation-like set
bool [:REAL,[:REAL,REAL:]:] is non empty set
d is Relation-like REAL -defined [:REAL,REAL:] -valued Function-like Element of bool [:REAL,[:REAL,REAL:]:]
((Re b) * ()) * d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((Im b) * ()) * d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (b0 (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (b0 (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(a0 (#) (C1 `| a)) + (- (b0 (#) (C2 `| a))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
b0 (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
(integral (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),f,C)) * <i> is complex set
(integral (((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))),f,C)) + ((integral (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),f,C)) * <i>) is complex set
b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
d is complex set
b0 (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (C1 `| a)) - (x (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (x (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (x (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(b0 (#) (C1 `| a)) + (- (x (#) (C2 `| a))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((b0 (#) (C1 `| a)) - (x (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
x (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x (#) (C1 `| a)) + (b0 (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((x (#) (C1 `| a)) + (b0 (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
(integral (((x (#) (C1 `| a)) + (b0 (#) (C2 `| a))),f,C)) * <i> is complex set
(integral (((b0 (#) (C1 `| a)) - (x (#) (C2 `| a))),f,C)) + ((integral (((x (#) (C1 `| a)) + (b0 (#) (C2 `| a))),f,C)) * <i>) is complex set
y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 is complex set
y (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(y (#) (C1 `| a)) - (Z (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (Z (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (Z (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(y (#) (C1 `| a)) + (- (Z (#) (C2 `| a))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((y (#) (C1 `| a)) - (Z (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
Z (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(Z (#) (C1 `| a)) + (y (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((Z (#) (C1 `| a)) + (y (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
(integral (((Z (#) (C1 `| a)) + (y (#) (C2 `| a))),f,C)) * <i> is complex set
(integral (((y (#) (C1 `| a)) - (Z (#) (C2 `| a))),f,C)) + ((integral (((Z (#) (C1 `| a)) + (y (#) (C2 `| a))),f,C)) * <i>) is complex set
[:REAL,COMPLEX:] is non empty Relation-like complex-valued set
bool [:REAL,COMPLEX:] is non empty set
5 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
- 5 is non empty complex real ext-real non positive negative Element of REAL
].(- 5),5.[ is V57() V58() V59() Element of bool REAL
<i> (#) sin is non empty Relation-like REAL -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of bool [:REAL,COMPLEX:]
cos + (<i> (#) sin) is non empty Relation-like REAL -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of bool [:REAL,COMPLEX:]
[.1,2.] is V57() V58() V59() Element of bool REAL
(cos + (<i> (#) sin)) | [.1,2.] is Relation-like REAL -defined [.1,2.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
b is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
dom (cos + (<i> (#) sin)) is non empty V57() V58() V59() Element of bool REAL
dom b is V57() V58() V59() Element of bool REAL
(dom (cos + (<i> (#) sin))) /\ [.1,2.] is V57() V58() V59() Element of bool REAL
sin | REAL is Relation-like REAL -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
sin | ].(- 5),5.[ is Relation-like REAL -defined ].(- 5),5.[ -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- sin is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) sin is Relation-like REAL -defined Function-like total complex-valued ext-real-valued real-valued set
(- sin) | ].(- 5),5.[ is Relation-like REAL -defined ].(- 5),5.[ -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (sin | ].(- 5),5.[) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(- 1) (#) (sin | ].(- 5),5.[) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
dom (- (sin | ].(- 5),5.[)) is V57() V58() V59() Element of bool REAL
dom ((- sin) | ].(- 5),5.[) is V57() V58() V59() Element of bool REAL
dom (- sin) is non empty V57() V58() V59() Element of bool REAL
(dom (- sin)) /\ ].(- 5),5.[ is V57() V58() V59() Element of bool REAL
REAL /\ ].(- 5),5.[ is V57() V58() V59() Element of bool REAL
d is complex real ext-real Element of REAL
(- (sin | ].(- 5),5.[)) . d is complex real ext-real Element of REAL
diff (cos,d) is complex real ext-real Element of REAL
((- sin) | ].(- 5),5.[) . d is complex real ext-real Element of REAL
(- sin) . d is complex real ext-real Element of REAL
sin . d is complex real ext-real Element of REAL
- (sin . d) is complex real ext-real Element of REAL
(sin | ].(- 5),5.[) . d is complex real ext-real Element of REAL
- ((sin | ].(- 5),5.[) . d) is complex real ext-real Element of REAL
cos `| ].(- 5),5.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
cos | REAL is Relation-like REAL -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
cos | ].(- 5),5.[ is Relation-like REAL -defined ].(- 5),5.[ -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (cos | ].(- 5),5.[) is V57() V58() V59() Element of bool REAL
(dom cos) /\ ].(- 5),5.[ is V57() V58() V59() Element of bool REAL
d is complex real ext-real Element of REAL
(cos | ].(- 5),5.[) . d is complex real ext-real Element of REAL
diff (sin,d) is complex real ext-real Element of REAL
cos . d is complex real ext-real Element of REAL
sin `| ].(- 5),5.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
f is complex real ext-real Element of REAL
C is complex real ext-real Element of REAL
[.f,C.] is V57() V58() V59() Element of bool REAL
C1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom C1 is V57() V58() V59() Element of bool REAL
C2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom C2 is V57() V58() V59() Element of bool REAL
<i> (#) C2 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
C1 + (<i> (#) C2) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(C1 + (<i> (#) C2)) | [.f,C.] is Relation-like REAL -defined [.f,C.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
rng ((C1 + (<i> (#) C2)) | [.f,C.]) is V57() Element of bool COMPLEX
bool COMPLEX is non empty set
a is V57() V58() V59() Element of bool REAL
b is V57() V58() V59() Element of bool REAL
d is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
dom d is V57() Element of bool COMPLEX
(f,C,C1,C2,a,d) is complex set
(f,C,C1,C2,b,d) is complex set
<:C1,C2:> is Relation-like Function-like set
Re d is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re d) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:C1,C2:> (#) ((Re d) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im d is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im d) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:C1,C2:> (#) ((Im d) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
C1 `| a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C2 `| a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (b0 (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (b0 (#) (C2 `| a)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(a0 (#) (C1 `| a)) + (- (b0 (#) (C2 `| a))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
b0 (#) (C1 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 (#) (C2 `| a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),f,C) is complex real ext-real Element of REAL
(integral (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),f,C)) * <i> is complex set
(integral (((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))),f,C)) + ((integral (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),f,C)) * <i>) is complex set
C1 `| b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C2 `| b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (C1 `| b) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (C2 `| b) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x (#) (C1 `| b)) - (y (#) (C2 `| b)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (y (#) (C2 `| b)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (y (#) (C2 `| b)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(x (#) (C1 `| b)) + (- (y (#) (C2 `| b))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((x (#) (C1 `| b)) - (y (#) (C2 `| b))),f,C) is complex real ext-real Element of REAL
y (#) (C1 `| b) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (C2 `| b) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(y (#) (C1 `| b)) + (x (#) (C2 `| b)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((y (#) (C1 `| b)) + (x (#) (C2 `| b))),f,C) is complex real ext-real Element of REAL
(integral (((y (#) (C1 `| b)) + (x (#) (C2 `| b))),f,C)) * <i> is complex set
(integral (((x (#) (C1 `| b)) - (y (#) (C2 `| b))),f,C)) + ((integral (((y (#) (C1 `| b)) + (x (#) (C2 `| b))),f,C)) * <i>) is complex set
Z is non empty V57() V58() V59() closed_interval interval Element of bool REAL
((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))) | Z is Relation-like REAL -defined Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((x (#) (C1 `| b)) - (y (#) (C2 `| b))) | Z is Relation-like REAL -defined Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))) is V57() V58() V59() Element of bool REAL
dom (a0 (#) (C1 `| a)) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (C2 `| a)) is V57() V58() V59() Element of bool REAL
(dom (a0 (#) (C1 `| a))) /\ (dom (b0 (#) (C2 `| a))) is V57() V58() V59() Element of bool REAL
dom a0 is V57() V58() V59() Element of bool REAL
dom (C1 `| a) is V57() V58() V59() Element of bool REAL
(dom a0) /\ (dom (C1 `| a)) is V57() V58() V59() Element of bool REAL
((dom a0) /\ (dom (C1 `| a))) /\ (dom (b0 (#) (C2 `| a))) is V57() V58() V59() Element of bool REAL
dom b0 is V57() V58() V59() Element of bool REAL
dom (C2 `| a) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (C2 `| a)) is V57() V58() V59() Element of bool REAL
((dom a0) /\ (dom (C1 `| a))) /\ ((dom b0) /\ (dom (C2 `| a))) is V57() V58() V59() Element of bool REAL
(dom a0) /\ a is V57() V58() V59() Element of bool REAL
((dom a0) /\ a) /\ ((dom b0) /\ (dom (C2 `| a))) is V57() V58() V59() Element of bool REAL
(dom b0) /\ a is V57() V58() V59() Element of bool REAL
((dom a0) /\ a) /\ ((dom b0) /\ a) is V57() V58() V59() Element of bool REAL
a /\ ((dom b0) /\ a) is V57() V58() V59() Element of bool REAL
(dom a0) /\ (a /\ ((dom b0) /\ a)) is V57() V58() V59() Element of bool REAL
a /\ a is V57() V58() V59() Element of bool REAL
(a /\ a) /\ (dom b0) is V57() V58() V59() Element of bool REAL
(dom a0) /\ ((a /\ a) /\ (dom b0)) is V57() V58() V59() Element of bool REAL
(dom a0) /\ (dom b0) is V57() V58() V59() Element of bool REAL
((dom a0) /\ (dom b0)) /\ a is V57() V58() V59() Element of bool REAL
dom ((x (#) (C1 `| b)) - (y (#) (C2 `| b))) is V57() V58() V59() Element of bool REAL
dom (x (#) (C1 `| b)) is V57() V58() V59() Element of bool REAL
dom (y (#) (C2 `| b)) is V57() V58() V59() Element of bool REAL
(dom (x (#) (C1 `| b))) /\ (dom (y (#) (C2 `| b))) is V57() V58() V59() Element of bool REAL
dom x is V57() V58() V59() Element of bool REAL
dom (C1 `| b) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (C1 `| b)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (C1 `| b))) /\ (dom (y (#) (C2 `| b))) is V57() V58() V59() Element of bool REAL
dom y is V57() V58() V59() Element of bool REAL
dom (C2 `| b) is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (C2 `| b)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (C1 `| b))) /\ ((dom y) /\ (dom (C2 `| b))) is V57() V58() V59() Element of bool REAL
(dom x) /\ b is V57() V58() V59() Element of bool REAL
((dom x) /\ b) /\ ((dom y) /\ (dom (C2 `| b))) is V57() V58() V59() Element of bool REAL
(dom y) /\ b is V57() V58() V59() Element of bool REAL
((dom x) /\ b) /\ ((dom y) /\ b) is V57() V58() V59() Element of bool REAL
b /\ ((dom y) /\ b) is V57() V58() V59() Element of bool REAL
(dom x) /\ (b /\ ((dom y) /\ b)) is V57() V58() V59() Element of bool REAL
b /\ b is V57() V58() V59() Element of bool REAL
(b /\ b) /\ (dom y) is V57() V58() V59() Element of bool REAL
(dom x) /\ ((b /\ b) /\ (dom y)) is V57() V58() V59() Element of bool REAL
((dom a0) /\ (dom b0)) /\ b is V57() V58() V59() Element of bool REAL
dom (((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))) | Z) is V57() V58() V59() Element of bool Z
bool Z is non empty set
(dom ((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a)))) /\ Z is V57() V58() V59() Element of bool REAL
a /\ Z is V57() V58() V59() Element of bool REAL
((dom a0) /\ (dom b0)) /\ (a /\ Z) is V57() V58() V59() Element of bool REAL
((dom a0) /\ (dom b0)) /\ Z is V57() V58() V59() Element of bool REAL
dom (((x (#) (C1 `| b)) - (y (#) (C2 `| b))) | Z) is V57() V58() V59() Element of bool Z
(dom ((x (#) (C1 `| b)) - (y (#) (C2 `| b)))) /\ Z is V57() V58() V59() Element of bool REAL
b /\ Z is V57() V58() V59() Element of bool REAL
((dom a0) /\ (dom b0)) /\ (b /\ Z) is V57() V58() V59() Element of bool REAL
u0 is set
(((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))) | Z) . u0 is complex real ext-real Element of REAL
(((x (#) (C1 `| b)) - (y (#) (C2 `| b))) | Z) . u0 is complex real ext-real Element of REAL
v0 is complex real ext-real Element of REAL
(((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))) | Z) . v0 is complex real ext-real Element of REAL
((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))) . v0 is complex real ext-real Element of REAL
(a0 (#) (C1 `| a)) . v0 is complex real ext-real Element of REAL
(b0 (#) (C2 `| a)) . v0 is complex real ext-real Element of REAL
((a0 (#) (C1 `| a)) . v0) - ((b0 (#) (C2 `| a)) . v0) is complex real ext-real Element of REAL
a0 . v0 is complex real ext-real Element of REAL
(C1 `| a) . v0 is complex real ext-real Element of REAL
(a0 . v0) * ((C1 `| a) . v0) is complex real ext-real Element of REAL
((a0 . v0) * ((C1 `| a) . v0)) - ((b0 (#) (C2 `| a)) . v0) is complex real ext-real Element of REAL
b0 . v0 is complex real ext-real Element of REAL
(C2 `| a) . v0 is complex real ext-real Element of REAL
(b0 . v0) * ((C2 `| a) . v0) is complex real ext-real Element of REAL
((a0 . v0) * ((C1 `| a) . v0)) - ((b0 . v0) * ((C2 `| a) . v0)) is complex real ext-real Element of REAL
diff (C1,v0) is complex real ext-real Element of REAL
(a0 . v0) * (diff (C1,v0)) is complex real ext-real Element of REAL
((a0 . v0) * (diff (C1,v0))) - ((b0 . v0) * ((C2 `| a) . v0)) is complex real ext-real Element of REAL
(((x (#) (C1 `| b)) - (y (#) (C2 `| b))) | Z) . v0 is complex real ext-real Element of REAL
((x (#) (C1 `| b)) - (y (#) (C2 `| b))) . v0 is complex real ext-real Element of REAL
(x (#) (C1 `| b)) . v0 is complex real ext-real Element of REAL
(y (#) (C2 `| b)) . v0 is complex real ext-real Element of REAL
((x (#) (C1 `| b)) . v0) - ((y (#) (C2 `| b)) . v0) is complex real ext-real Element of REAL
x . v0 is complex real ext-real Element of REAL
(C1 `| b) . v0 is complex real ext-real Element of REAL
(x . v0) * ((C1 `| b) . v0) is complex real ext-real Element of REAL
((x . v0) * ((C1 `| b) . v0)) - ((y (#) (C2 `| b)) . v0) is complex real ext-real Element of REAL
y . v0 is complex real ext-real Element of REAL
(C2 `| b) . v0 is complex real ext-real Element of REAL
(y . v0) * ((C2 `| b) . v0) is complex real ext-real Element of REAL
((x . v0) * ((C1 `| b) . v0)) - ((y . v0) * ((C2 `| b) . v0)) is complex real ext-real Element of REAL
(x . v0) * (diff (C1,v0)) is complex real ext-real Element of REAL
((x . v0) * (diff (C1,v0))) - ((y . v0) * ((C2 `| b) . v0)) is complex real ext-real Element of REAL
diff (C2,v0) is complex real ext-real Element of REAL
(b0 . v0) * (diff (C2,v0)) is complex real ext-real Element of REAL
((a0 . v0) * (diff (C1,v0))) - ((b0 . v0) * (diff (C2,v0))) is complex real ext-real Element of REAL
integral (((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))),Z) is complex real ext-real Element of REAL
K298(((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))),Z) is Relation-like Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:Z,REAL:]
[:Z,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:Z,REAL:] is non empty set
K659(Z,K298(((a0 (#) (C1 `| a)) - (b0 (#) (C2 `| a))),Z)) is complex real ext-real Element of REAL
integral (((x (#) (C1 `| b)) - (y (#) (C2 `| b))),Z) is complex real ext-real Element of REAL
K298(((x (#) (C1 `| b)) - (y (#) (C2 `| b))),Z) is Relation-like Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:Z,REAL:]
K659(Z,K298(((x (#) (C1 `| b)) - (y (#) (C2 `| b))),Z)) is complex real ext-real Element of REAL
((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))) | Z is Relation-like REAL -defined Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((y (#) (C1 `| b)) + (x (#) (C2 `| b))) | Z is Relation-like REAL -defined Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (C1 `| a)) is V57() V58() V59() Element of bool REAL
dom (a0 (#) (C2 `| a)) is V57() V58() V59() Element of bool REAL
(dom (b0 (#) (C1 `| a))) /\ (dom (a0 (#) (C2 `| a))) is V57() V58() V59() Element of bool REAL
dom b0 is V57() V58() V59() Element of bool REAL
dom (C1 `| a) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (C1 `| a)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (C1 `| a))) /\ (dom (a0 (#) (C2 `| a))) is V57() V58() V59() Element of bool REAL
dom a0 is V57() V58() V59() Element of bool REAL
dom (C2 `| a) is V57() V58() V59() Element of bool REAL
(dom a0) /\ (dom (C2 `| a)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (C1 `| a))) /\ ((dom a0) /\ (dom (C2 `| a))) is V57() V58() V59() Element of bool REAL
(dom b0) /\ a is V57() V58() V59() Element of bool REAL
((dom b0) /\ a) /\ ((dom a0) /\ (dom (C2 `| a))) is V57() V58() V59() Element of bool REAL
(dom a0) /\ a is V57() V58() V59() Element of bool REAL
((dom b0) /\ a) /\ ((dom a0) /\ a) is V57() V58() V59() Element of bool REAL
a /\ ((dom a0) /\ a) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (a /\ ((dom a0) /\ a)) is V57() V58() V59() Element of bool REAL
a /\ a is V57() V58() V59() Element of bool REAL
(a /\ a) /\ (dom a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ ((a /\ a) /\ (dom a0)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom a0) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom a0)) /\ a is V57() V58() V59() Element of bool REAL
dom ((y (#) (C1 `| b)) + (x (#) (C2 `| b))) is V57() V58() V59() Element of bool REAL
dom (y (#) (C1 `| b)) is V57() V58() V59() Element of bool REAL
dom (x (#) (C2 `| b)) is V57() V58() V59() Element of bool REAL
(dom (y (#) (C1 `| b))) /\ (dom (x (#) (C2 `| b))) is V57() V58() V59() Element of bool REAL
dom y is V57() V58() V59() Element of bool REAL
dom (C1 `| b) is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (C1 `| b)) is V57() V58() V59() Element of bool REAL
((dom y) /\ (dom (C1 `| b))) /\ (dom (x (#) (C2 `| b))) is V57() V58() V59() Element of bool REAL
dom x is V57() V58() V59() Element of bool REAL
dom (C2 `| b) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (C2 `| b)) is V57() V58() V59() Element of bool REAL
((dom y) /\ (dom (C1 `| b))) /\ ((dom x) /\ (dom (C2 `| b))) is V57() V58() V59() Element of bool REAL
(dom y) /\ b is V57() V58() V59() Element of bool REAL
((dom y) /\ b) /\ ((dom x) /\ (dom (C2 `| b))) is V57() V58() V59() Element of bool REAL
(dom x) /\ b is V57() V58() V59() Element of bool REAL
((dom y) /\ b) /\ ((dom x) /\ b) is V57() V58() V59() Element of bool REAL
b /\ ((dom x) /\ b) is V57() V58() V59() Element of bool REAL
(dom y) /\ (b /\ ((dom x) /\ b)) is V57() V58() V59() Element of bool REAL
b /\ b is V57() V58() V59() Element of bool REAL
(b /\ b) /\ (dom x) is V57() V58() V59() Element of bool REAL
(dom y) /\ ((b /\ b) /\ (dom x)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom a0)) /\ b is V57() V58() V59() Element of bool REAL
dom (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))) | Z) is V57() V58() V59() Element of bool Z
bool Z is non empty set
(dom ((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a)))) /\ Z is V57() V58() V59() Element of bool REAL
a /\ Z is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom a0)) /\ (a /\ Z) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom a0)) /\ Z is V57() V58() V59() Element of bool REAL
dom (((y (#) (C1 `| b)) + (x (#) (C2 `| b))) | Z) is V57() V58() V59() Element of bool Z
(dom ((y (#) (C1 `| b)) + (x (#) (C2 `| b)))) /\ Z is V57() V58() V59() Element of bool REAL
b /\ Z is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom a0)) /\ (b /\ Z) is V57() V58() V59() Element of bool REAL
u0 is set
(((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))) | Z) . u0 is complex real ext-real Element of REAL
(((y (#) (C1 `| b)) + (x (#) (C2 `| b))) | Z) . u0 is complex real ext-real Element of REAL
v0 is complex real ext-real Element of REAL
(((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))) | Z) . v0 is complex real ext-real Element of REAL
((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))) . v0 is complex real ext-real Element of REAL
(b0 (#) (C1 `| a)) . v0 is complex real ext-real Element of REAL
(a0 (#) (C2 `| a)) . v0 is complex real ext-real Element of REAL
((b0 (#) (C1 `| a)) . v0) + ((a0 (#) (C2 `| a)) . v0) is complex real ext-real Element of REAL
b0 . v0 is complex real ext-real Element of REAL
(C1 `| a) . v0 is complex real ext-real Element of REAL
(b0 . v0) * ((C1 `| a) . v0) is complex real ext-real Element of REAL
((b0 . v0) * ((C1 `| a) . v0)) + ((a0 (#) (C2 `| a)) . v0) is complex real ext-real Element of REAL
a0 . v0 is complex real ext-real Element of REAL
(C2 `| a) . v0 is complex real ext-real Element of REAL
(a0 . v0) * ((C2 `| a) . v0) is complex real ext-real Element of REAL
((b0 . v0) * ((C1 `| a) . v0)) + ((a0 . v0) * ((C2 `| a) . v0)) is complex real ext-real Element of REAL
diff (C1,v0) is complex real ext-real Element of REAL
(b0 . v0) * (diff (C1,v0)) is complex real ext-real Element of REAL
((b0 . v0) * (diff (C1,v0))) + ((a0 . v0) * ((C2 `| a) . v0)) is complex real ext-real Element of REAL
diff (C2,v0) is complex real ext-real Element of REAL
(a0 . v0) * (diff (C2,v0)) is complex real ext-real Element of REAL
((b0 . v0) * (diff (C1,v0))) + ((a0 . v0) * (diff (C2,v0))) is complex real ext-real Element of REAL
(((y (#) (C1 `| b)) + (x (#) (C2 `| b))) | Z) . v0 is complex real ext-real Element of REAL
((y (#) (C1 `| b)) + (x (#) (C2 `| b))) . v0 is complex real ext-real Element of REAL
(y (#) (C1 `| b)) . v0 is complex real ext-real Element of REAL
(x (#) (C2 `| b)) . v0 is complex real ext-real Element of REAL
((y (#) (C1 `| b)) . v0) + ((x (#) (C2 `| b)) . v0) is complex real ext-real Element of REAL
y . v0 is complex real ext-real Element of REAL
(C1 `| b) . v0 is complex real ext-real Element of REAL
(y . v0) * ((C1 `| b) . v0) is complex real ext-real Element of REAL
((y . v0) * ((C1 `| b) . v0)) + ((x (#) (C2 `| b)) . v0) is complex real ext-real Element of REAL
x . v0 is complex real ext-real Element of REAL
(C2 `| b) . v0 is complex real ext-real Element of REAL
(x . v0) * ((C2 `| b) . v0) is complex real ext-real Element of REAL
((y . v0) * ((C1 `| b) . v0)) + ((x . v0) * ((C2 `| b) . v0)) is complex real ext-real Element of REAL
(y . v0) * (diff (C1,v0)) is complex real ext-real Element of REAL
((y . v0) * (diff (C1,v0))) + ((x . v0) * ((C2 `| b) . v0)) is complex real ext-real Element of REAL
integral (((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),Z) is complex real ext-real Element of REAL
K298(((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),Z) is Relation-like Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:Z,REAL:]
K659(Z,K298(((b0 (#) (C1 `| a)) + (a0 (#) (C2 `| a))),Z)) is complex real ext-real Element of REAL
integral (((y (#) (C1 `| b)) + (x (#) (C2 `| b))),Z) is complex real ext-real Element of REAL
K298(((y (#) (C1 `| b)) + (x (#) (C2 `| b))),Z) is Relation-like Z -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:Z,REAL:]
K659(Z,K298(((y (#) (C1 `| b)) + (x (#) (C2 `| b))),Z)) is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
C is complex real ext-real Element of REAL
[.f,C.] is V57() V58() V59() Element of bool REAL
C1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom C1 is V57() V58() V59() Element of bool REAL
C2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom C2 is V57() V58() V59() Element of bool REAL
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom a is V57() V58() V59() Element of bool REAL
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V57() V58() V59() Element of bool REAL
C1 | [.f,C.] is Relation-like REAL -defined [.f,C.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a | [.f,C.] is Relation-like REAL -defined [.f,C.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C2 | [.f,C.] is Relation-like REAL -defined [.f,C.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b | [.f,C.] is Relation-like REAL -defined [.f,C.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) C2 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
C1 + (<i> (#) C2) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(C1 + (<i> (#) C2)) | [.f,C.] is Relation-like REAL -defined [.f,C.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
rng ((C1 + (<i> (#) C2)) | [.f,C.]) is V57() Element of bool COMPLEX
bool COMPLEX is non empty set
<i> (#) b is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
a + (<i> (#) b) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(a + (<i> (#) b)) | [.f,C.] is Relation-like REAL -defined [.f,C.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
rng ((a + (<i> (#) b)) | [.f,C.]) is V57() Element of bool COMPLEX
d is V57() V58() V59() Element of bool REAL
a0 is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
dom a0 is V57() Element of bool COMPLEX
(f,C,C1,C2,d,a0) is complex set
(f,C,a,b,d,a0) is complex set
<:C1,C2:> is Relation-like Function-like set
Re a0 is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re a0) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:C1,C2:> (#) ((Re a0) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im a0 is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im a0) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:C1,C2:> (#) ((Im a0) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
C1 `| d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C2 `| d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (C1 `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (C2 `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (C1 `| d)) - (x (#) (C2 `| d)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (x (#) (C2 `| d)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (x (#) (C2 `| d)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(b0 (#) (C1 `| d)) + (- (x (#) (C2 `| d))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),f,C) is complex real ext-real Element of REAL
x (#) (C1 `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (C2 `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x (#) (C1 `| d)) + (b0 (#) (C2 `| d)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),f,C) is complex real ext-real Element of REAL
(integral (((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),f,C)) * <i> is complex set
(integral (((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),f,C)) + ((integral (((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),f,C)) * <i>) is complex set
<:a,b:> is Relation-like Function-like set
<:a,b:> (#) ((Re a0) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
<:a,b:> (#) ((Im a0) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
a `| d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b `| d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (a `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z (#) (b `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(y (#) (a `| d)) - (Z (#) (b `| d)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (Z (#) (b `| d)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (Z (#) (b `| d)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(y (#) (a `| d)) + (- (Z (#) (b `| d))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((y (#) (a `| d)) - (Z (#) (b `| d))),f,C) is complex real ext-real Element of REAL
Z (#) (a `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (b `| d) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(Z (#) (a `| d)) + (y (#) (b `| d)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((Z (#) (a `| d)) + (y (#) (b `| d))),f,C) is complex real ext-real Element of REAL
(integral (((Z (#) (a `| d)) + (y (#) (b `| d))),f,C)) * <i> is complex set
(integral (((y (#) (a `| d)) - (Z (#) (b `| d))),f,C)) + ((integral (((Z (#) (a `| d)) + (y (#) (b `| d))),f,C)) * <i>) is complex set
C - f is complex real ext-real Element of REAL
f - C is complex real ext-real Element of REAL
f + (C - f) is complex real ext-real Element of REAL
C + (f - C) is complex real ext-real Element of REAL
u0 is non empty V57() V58() V59() closed_interval interval Element of bool REAL
b0 | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (b0 | u0) is V57() V58() V59() Element of bool u0
bool u0 is non empty set
dom (y | u0) is V57() V58() V59() Element of bool u0
v0 is set
dom b0 is V57() V58() V59() Element of bool REAL
(dom b0) /\ u0 is V57() V58() V59() Element of bool REAL
proj1 <:C1,C2:> is set
<:C1,C2:> . v0 is set
dom ((Re a0) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C1 . v0 is complex real ext-real Element of REAL
C2 . v0 is complex real ext-real Element of REAL
[(C1 . v0),(C2 . v0)] is V24() set
C1 | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C1 | u0) . v0 is complex real ext-real Element of REAL
[((C1 | u0) . v0),(C2 . v0)] is V24() set
a | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a | u0) . v0 is complex real ext-real Element of REAL
b | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b | u0) . v0 is complex real ext-real Element of REAL
[((a | u0) . v0),((b | u0) . v0)] is V24() set
b . v0 is complex real ext-real Element of REAL
[((a | u0) . v0),(b . v0)] is V24() set
a . v0 is complex real ext-real Element of REAL
[(a . v0),(b . v0)] is V24() set
(dom a) /\ (dom b) is V57() V58() V59() Element of bool REAL
proj1 <:a,b:> is set
<:a,b:> . v0 is set
dom y is V57() V58() V59() Element of bool REAL
(dom y) /\ u0 is V57() V58() V59() Element of bool REAL
v0 is set
dom y is V57() V58() V59() Element of bool REAL
(dom y) /\ u0 is V57() V58() V59() Element of bool REAL
proj1 <:a,b:> is set
<:a,b:> . v0 is set
dom ((Re a0) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a . v0 is complex real ext-real Element of REAL
b . v0 is complex real ext-real Element of REAL
[(a . v0),(b . v0)] is V24() set
a | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a | u0) . v0 is complex real ext-real Element of REAL
[((a | u0) . v0),(b . v0)] is V24() set
C1 | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C1 | u0) . v0 is complex real ext-real Element of REAL
C2 | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C2 | u0) . v0 is complex real ext-real Element of REAL
[((C1 | u0) . v0),((C2 | u0) . v0)] is V24() set
C2 . v0 is complex real ext-real Element of REAL
[((C1 | u0) . v0),(C2 . v0)] is V24() set
C1 . v0 is complex real ext-real Element of REAL
[(C1 . v0),(C2 . v0)] is V24() set
(dom C1) /\ (dom C2) is V57() V58() V59() Element of bool REAL
proj1 <:C1,C2:> is set
<:C1,C2:> . v0 is set
dom b0 is V57() V58() V59() Element of bool REAL
(dom b0) /\ u0 is V57() V58() V59() Element of bool REAL
v0 is set
(b0 | u0) . v0 is complex real ext-real Element of REAL
(y | u0) . v0 is complex real ext-real Element of REAL
dom b0 is V57() V58() V59() Element of bool REAL
(dom b0) /\ u0 is V57() V58() V59() Element of bool REAL
(dom C1) /\ (dom C2) is V57() V58() V59() Element of bool REAL
a1 is complex real ext-real Element of REAL
proj1 <:C1,C2:> is set
b0 . a1 is complex real ext-real Element of REAL
<:C1,C2:> . a1 is set
((Re a0) * ()) . (<:C1,C2:> . a1) is complex real ext-real Element of REAL
(dom a) /\ (dom b) is V57() V58() V59() Element of bool REAL
proj1 <:a,b:> is set
y . a1 is complex real ext-real Element of REAL
<:a,b:> . a1 is set
((Re a0) * ()) . (<:a,b:> . a1) is complex real ext-real Element of REAL
a . a1 is complex real ext-real Element of REAL
b . a1 is complex real ext-real Element of REAL
[(a . a1),(b . a1)] is V24() set
((Re a0) * ()) . [(a . a1),(b . a1)] is complex real ext-real Element of REAL
C1 . a1 is complex real ext-real Element of REAL
(C1 | [.f,C.]) . a1 is complex real ext-real Element of REAL
C2 . a1 is complex real ext-real Element of REAL
(C2 | [.f,C.]) . a1 is complex real ext-real Element of REAL
(b0 | u0) . a1 is complex real ext-real Element of REAL
(y | u0) . a1 is complex real ext-real Element of REAL
(C1 `| d) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a `| d) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((C1 `| d) | u0) is V57() V58() V59() Element of bool u0
bool u0 is non empty set
dom (C1 `| d) is V57() V58() V59() Element of bool REAL
(dom (C1 `| d)) /\ u0 is V57() V58() V59() Element of bool REAL
d /\ u0 is V57() V58() V59() Element of bool REAL
dom ((a `| d) | u0) is V57() V58() V59() Element of bool u0
dom (a `| d) is V57() V58() V59() Element of bool REAL
(dom (a `| d)) /\ u0 is V57() V58() V59() Element of bool REAL
v0 is set
((C1 `| d) | u0) . v0 is complex real ext-real Element of REAL
((a `| d) | u0) . v0 is complex real ext-real Element of REAL
a1 is complex real ext-real Element of REAL
((a `| d) | u0) . a1 is complex real ext-real Element of REAL
(a `| d) . a1 is complex real ext-real Element of REAL
(C1 `| d) . a1 is complex real ext-real Element of REAL
diff (C1,a1) is complex real ext-real Element of REAL
diff (a,a1) is complex real ext-real Element of REAL
].f,C.[ is V57() V58() V59() Element of bool REAL
{ b₁ where b₁ is complex real ext-real Element of REAL : ( f <= b₁ & b₁ <= C ) } is set
a1 - f is complex real ext-real Element of REAL
f - a1 is complex real ext-real Element of REAL
f + (a1 - f) is complex real ext-real Element of REAL
a1 + (f - a1) is complex real ext-real Element of REAL
b1 is complex real ext-real Element of REAL
a1 - C is complex real ext-real Element of REAL
C - a1 is complex real ext-real Element of REAL
C + (a1 - C) is complex real ext-real Element of REAL
a1 + (C - a1) is complex real ext-real Element of REAL
b1 is complex real ext-real Element of REAL
{ b₁ where b₁ is complex real ext-real Element of REAL : ( not b₁ <= f & not C <= b₁ ) } is set
Rdiff (C1,a1) is complex real ext-real Element of REAL
Rdiff (a,a1) is complex real ext-real Element of REAL
C1 - a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- a is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) a is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
C1 + (- a) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(Rdiff (C1,a1)) - (Rdiff (a,a1)) is complex real ext-real Element of REAL
Rdiff ((C1 - a),a1) is complex real ext-real Element of REAL
{a1} is non empty V57() V58() V59() set
dom (C1 - a) is V57() V58() V59() Element of bool REAL
b1 is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of bool [:NAT,REAL:]
b1 " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
x1 is non empty Relation-like NAT -defined REAL -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng x1 is non empty V57() V58() V59() Element of bool REAL
b1 + x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng (b1 + x1) is non empty V57() V58() V59() Element of bool REAL
(C1 - a) /* (b1 + x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(C1 - a) /* x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- ((C1 - a) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) ((C1 - a) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((C1 - a) /* (b1 + x1)) + (- ((C1 - a) /* x1)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim ((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) is complex real ext-real Element of REAL
lim b1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() Element of REAL
(C - a1) / 2 is complex real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
Z1 is complex real ext-real set
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2 is complex real ext-real Element of REAL
b1 . a2 is complex real ext-real Element of REAL
(b1 . a2) - 0 is complex real ext-real Element of REAL
abs ((b1 . a2) - 0) is complex real ext-real Element of REAL
f + 0 is complex real ext-real Element of REAL
a1 + (b1 . a2) is complex real ext-real Element of REAL
a1 + ((C - a1) / 2) is complex real ext-real Element of REAL
(a1 + (b1 . a2)) + 0 is complex real ext-real Element of REAL
C - ((C - a1) / 2) is complex real ext-real Element of REAL
(C - ((C - a1) / 2)) + ((C - a1) / 2) is complex real ext-real Element of REAL
(dom C1) /\ (dom a) is V57() V58() V59() Element of bool REAL
lim x1 is complex real ext-real Element of REAL
x1 . a2 is complex real ext-real Element of REAL
(b1 + x1) . a2 is complex real ext-real Element of REAL
(b1 . a2) + (x1 . a2) is complex real ext-real Element of REAL
(b1 . a2) + a1 is complex real ext-real Element of REAL
b2 is set
(b1 ") . a2 is complex real ext-real Element of REAL
(((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1)) . a2 is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1)) . a2) is complex real ext-real Element of REAL
((C1 - a) /* (b1 + x1)) . a2 is complex real ext-real Element of REAL
((C1 - a) /* x1) . a2 is complex real ext-real Element of REAL
(((C1 - a) /* (b1 + x1)) . a2) - (((C1 - a) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C1 - a) /* (b1 + x1)) . a2) - (((C1 - a) /* x1) . a2)) is complex real ext-real Element of REAL
(C1 - a) . ((b1 + x1) . a2) is complex real ext-real Element of REAL
((C1 - a) . ((b1 + x1) . a2)) - (((C1 - a) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C1 - a) . ((b1 + x1) . a2)) - (((C1 - a) /* x1) . a2)) is complex real ext-real Element of REAL
(C1 - a) . (x1 . a2) is complex real ext-real Element of REAL
((C1 - a) . ((b1 + x1) . a2)) - ((C1 - a) . (x1 . a2)) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C1 - a) . ((b1 + x1) . a2)) - ((C1 - a) . (x1 . a2))) is complex real ext-real Element of REAL
(C1 - a) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C1 - a) . a1 is complex real ext-real Element of REAL
((C1 - a) . ((b1 . a2) + a1)) - ((C1 - a) . a1) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C1 - a) . ((b1 . a2) + a1)) - ((C1 - a) . a1)) is complex real ext-real Element of REAL
C1 . ((b1 . a2) + a1) is complex real ext-real Element of REAL
a . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C1 . ((b1 . a2) + a1)) - (a . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(C1 | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C1 | [.f,C.]) . ((b1 . a2) + a1)) - (a . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(a | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C1 | [.f,C.]) . ((b1 . a2) + a1)) - ((a | [.f,C.]) . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
C1 . a1 is complex real ext-real Element of REAL
a . a1 is complex real ext-real Element of REAL
(C1 . a1) - (a . a1) is complex real ext-real Element of REAL
(C1 | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C1 | [.f,C.]) . a1) - (a . a1) is complex real ext-real Element of REAL
(a | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C1 | [.f,C.]) . a1) - ((a | [.f,C.]) . a1) is complex real ext-real Element of REAL
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2 is complex real ext-real Element of REAL
(((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2) - 0 is complex real ext-real Element of REAL
abs ((((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2) - 0) is complex real ext-real Element of REAL
b1 is set
y1 is complex real ext-real Element of REAL
x1 is complex real ext-real Element of REAL
y1 is complex real ext-real Element of REAL
C1 | ].f,C.[ is Relation-like REAL -defined ].f,C.[ -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C1 | ].f,C.[) `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C1 `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C1 `| ].f,C.[) . a1 is complex real ext-real Element of REAL
a | ].f,C.[ is Relation-like REAL -defined ].f,C.[ -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a | ].f,C.[) `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a `| ].f,C.[) . a1 is complex real ext-real Element of REAL
dom (C1 | ].f,C.[) is V57() V58() V59() Element of bool REAL
(dom C1) /\ ].f,C.[ is V57() V58() V59() Element of bool REAL
(dom a) /\ ].f,C.[ is V57() V58() V59() Element of bool REAL
dom (a | ].f,C.[) is V57() V58() V59() Element of bool REAL
b1 is set
(C1 | ].f,C.[) . b1 is complex real ext-real Element of REAL
(a | ].f,C.[) . b1 is complex real ext-real Element of REAL
C1 . b1 is complex real ext-real Element of REAL
(C1 | [.f,C.]) . b1 is complex real ext-real Element of REAL
a . b1 is complex real ext-real Element of REAL
Ldiff (C1,a1) is complex real ext-real Element of REAL
Ldiff (a,a1) is complex real ext-real Element of REAL
C1 - a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- a is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) a is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
C1 + (- a) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(Ldiff (C1,a1)) - (Ldiff (a,a1)) is complex real ext-real Element of REAL
Ldiff ((C1 - a),a1) is complex real ext-real Element of REAL
{a1} is non empty V57() V58() V59() set
dom (C1 - a) is V57() V58() V59() Element of bool REAL
b1 is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of bool [:NAT,REAL:]
b1 " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
x1 is non empty Relation-like NAT -defined REAL -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng x1 is non empty V57() V58() V59() Element of bool REAL
b1 + x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng (b1 + x1) is non empty V57() V58() V59() Element of bool REAL
(C1 - a) /* (b1 + x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(C1 - a) /* x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- ((C1 - a) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) ((C1 - a) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((C1 - a) /* (b1 + x1)) + (- ((C1 - a) /* x1)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim ((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) is complex real ext-real Element of REAL
lim b1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() Element of REAL
(a1 - f) / 2 is complex real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
Z1 is complex real ext-real set
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2 is complex real ext-real Element of REAL
b1 . a2 is complex real ext-real Element of REAL
(b1 . a2) - 0 is complex real ext-real Element of REAL
abs ((b1 . a2) - 0) is complex real ext-real Element of REAL
- (b1 . a2) is complex real ext-real Element of REAL
a1 + (b1 . a2) is complex real ext-real Element of REAL
C + 0 is complex real ext-real Element of REAL
a1 - ((a1 - f) / 2) is complex real ext-real Element of REAL
a1 - (- (b1 . a2)) is complex real ext-real Element of REAL
f + ((a1 - f) / 2) is complex real ext-real Element of REAL
(f + ((a1 - f) / 2)) - ((a1 - f) / 2) is complex real ext-real Element of REAL
(a1 + (b1 . a2)) - 0 is complex real ext-real Element of REAL
(dom C1) /\ (dom a) is V57() V58() V59() Element of bool REAL
lim x1 is complex real ext-real Element of REAL
(b1 + x1) . a2 is complex real ext-real Element of REAL
x1 . a2 is complex real ext-real Element of REAL
(b1 . a2) + (x1 . a2) is complex real ext-real Element of REAL
(b1 . a2) + a1 is complex real ext-real Element of REAL
b2 is set
(b1 ") . a2 is complex real ext-real Element of REAL
(((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1)) . a2 is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1)) . a2) is complex real ext-real Element of REAL
((C1 - a) /* (b1 + x1)) . a2 is complex real ext-real Element of REAL
((C1 - a) /* x1) . a2 is complex real ext-real Element of REAL
(((C1 - a) /* (b1 + x1)) . a2) - (((C1 - a) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C1 - a) /* (b1 + x1)) . a2) - (((C1 - a) /* x1) . a2)) is complex real ext-real Element of REAL
(C1 - a) . ((b1 + x1) . a2) is complex real ext-real Element of REAL
((C1 - a) . ((b1 + x1) . a2)) - (((C1 - a) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C1 - a) . ((b1 + x1) . a2)) - (((C1 - a) /* x1) . a2)) is complex real ext-real Element of REAL
(C1 - a) . (x1 . a2) is complex real ext-real Element of REAL
((C1 - a) . ((b1 + x1) . a2)) - ((C1 - a) . (x1 . a2)) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C1 - a) . ((b1 + x1) . a2)) - ((C1 - a) . (x1 . a2))) is complex real ext-real Element of REAL
(C1 - a) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C1 - a) . a1 is complex real ext-real Element of REAL
((C1 - a) . ((b1 . a2) + a1)) - ((C1 - a) . a1) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C1 - a) . ((b1 . a2) + a1)) - ((C1 - a) . a1)) is complex real ext-real Element of REAL
C1 . ((b1 . a2) + a1) is complex real ext-real Element of REAL
a . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C1 . ((b1 . a2) + a1)) - (a . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(C1 | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C1 | [.f,C.]) . ((b1 . a2) + a1)) - (a . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(a | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C1 | [.f,C.]) . ((b1 . a2) + a1)) - ((a | [.f,C.]) . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
C1 . a1 is complex real ext-real Element of REAL
a . a1 is complex real ext-real Element of REAL
(C1 . a1) - (a . a1) is complex real ext-real Element of REAL
(C1 | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C1 | [.f,C.]) . a1) - (a . a1) is complex real ext-real Element of REAL
(a | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C1 | [.f,C.]) . a1) - ((a | [.f,C.]) . a1) is complex real ext-real Element of REAL
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2 is complex real ext-real Element of REAL
(((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2) - 0 is complex real ext-real Element of REAL
abs ((((b1 ") (#) (((C1 - a) /* (b1 + x1)) - ((C1 - a) /* x1))) . a2) - 0) is complex real ext-real Element of REAL
x | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (x | u0) is V57() V58() V59() Element of bool u0
bool u0 is non empty set
dom (Z | u0) is V57() V58() V59() Element of bool u0
v0 is set
dom x is V57() V58() V59() Element of bool REAL
(dom x) /\ u0 is V57() V58() V59() Element of bool REAL
proj1 <:C1,C2:> is set
<:C1,C2:> . v0 is set
dom ((Im a0) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C1 . v0 is complex real ext-real Element of REAL
C2 . v0 is complex real ext-real Element of REAL
[(C1 . v0),(C2 . v0)] is V24() set
C1 | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C1 | u0) . v0 is complex real ext-real Element of REAL
[((C1 | u0) . v0),(C2 . v0)] is V24() set
a | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a | u0) . v0 is complex real ext-real Element of REAL
b | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b | u0) . v0 is complex real ext-real Element of REAL
[((a | u0) . v0),((b | u0) . v0)] is V24() set
b . v0 is complex real ext-real Element of REAL
[((a | u0) . v0),(b . v0)] is V24() set
a . v0 is complex real ext-real Element of REAL
[(a . v0),(b . v0)] is V24() set
(dom a) /\ (dom b) is V57() V58() V59() Element of bool REAL
proj1 <:a,b:> is set
<:a,b:> . v0 is set
dom Z is V57() V58() V59() Element of bool REAL
(dom Z) /\ u0 is V57() V58() V59() Element of bool REAL
v0 is set
dom Z is V57() V58() V59() Element of bool REAL
(dom Z) /\ u0 is V57() V58() V59() Element of bool REAL
proj1 <:a,b:> is set
<:a,b:> . v0 is set
dom ((Im a0) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a . v0 is complex real ext-real Element of REAL
b . v0 is complex real ext-real Element of REAL
[(a . v0),(b . v0)] is V24() set
a | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a | u0) . v0 is complex real ext-real Element of REAL
[((a | u0) . v0),(b . v0)] is V24() set
C1 | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C1 | u0) . v0 is complex real ext-real Element of REAL
C2 | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C2 | u0) . v0 is complex real ext-real Element of REAL
[((C1 | u0) . v0),((C2 | u0) . v0)] is V24() set
C2 . v0 is complex real ext-real Element of REAL
[((C1 | u0) . v0),(C2 . v0)] is V24() set
C1 . v0 is complex real ext-real Element of REAL
[(C1 . v0),(C2 . v0)] is V24() set
(dom C1) /\ (dom C2) is V57() V58() V59() Element of bool REAL
proj1 <:C1,C2:> is set
<:C1,C2:> . v0 is set
dom x is V57() V58() V59() Element of bool REAL
(dom x) /\ u0 is V57() V58() V59() Element of bool REAL
v0 is set
(x | u0) . v0 is complex real ext-real Element of REAL
(Z | u0) . v0 is complex real ext-real Element of REAL
dom x is V57() V58() V59() Element of bool REAL
(dom x) /\ u0 is V57() V58() V59() Element of bool REAL
(dom C1) /\ (dom C2) is V57() V58() V59() Element of bool REAL
a1 is complex real ext-real Element of REAL
proj1 <:C1,C2:> is set
x . a1 is complex real ext-real Element of REAL
<:C1,C2:> . a1 is set
((Im a0) * ()) . (<:C1,C2:> . a1) is complex real ext-real Element of REAL
(dom a) /\ (dom b) is V57() V58() V59() Element of bool REAL
proj1 <:a,b:> is set
Z . a1 is complex real ext-real Element of REAL
<:a,b:> . a1 is set
((Im a0) * ()) . (<:a,b:> . a1) is complex real ext-real Element of REAL
a . a1 is complex real ext-real Element of REAL
b . a1 is complex real ext-real Element of REAL
[(a . a1),(b . a1)] is V24() set
((Im a0) * ()) . [(a . a1),(b . a1)] is complex real ext-real Element of REAL
C1 . a1 is complex real ext-real Element of REAL
(C1 | [.f,C.]) . a1 is complex real ext-real Element of REAL
C2 . a1 is complex real ext-real Element of REAL
(C2 | [.f,C.]) . a1 is complex real ext-real Element of REAL
(x | u0) . a1 is complex real ext-real Element of REAL
(Z | u0) . a1 is complex real ext-real Element of REAL
(C2 `| d) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b `| d) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((C2 `| d) | u0) is V57() V58() V59() Element of bool u0
bool u0 is non empty set
dom (C2 `| d) is V57() V58() V59() Element of bool REAL
(dom (C2 `| d)) /\ u0 is V57() V58() V59() Element of bool REAL
d /\ u0 is V57() V58() V59() Element of bool REAL
dom ((b `| d) | u0) is V57() V58() V59() Element of bool u0
dom (b `| d) is V57() V58() V59() Element of bool REAL
(dom (b `| d)) /\ u0 is V57() V58() V59() Element of bool REAL
v0 is set
((C2 `| d) | u0) . v0 is complex real ext-real Element of REAL
((b `| d) | u0) . v0 is complex real ext-real Element of REAL
a1 is complex real ext-real Element of REAL
((b `| d) | u0) . a1 is complex real ext-real Element of REAL
(b `| d) . a1 is complex real ext-real Element of REAL
(C2 `| d) . a1 is complex real ext-real Element of REAL
diff (C2,a1) is complex real ext-real Element of REAL
diff (b,a1) is complex real ext-real Element of REAL
].f,C.[ is V57() V58() V59() Element of bool REAL
{ b₁ where b₁ is complex real ext-real Element of REAL : ( f <= b₁ & b₁ <= C ) } is set
a1 - f is complex real ext-real Element of REAL
f - a1 is complex real ext-real Element of REAL
f + (a1 - f) is complex real ext-real Element of REAL
a1 + (f - a1) is complex real ext-real Element of REAL
b1 is complex real ext-real Element of REAL
a1 - C is complex real ext-real Element of REAL
C - a1 is complex real ext-real Element of REAL
C + (a1 - C) is complex real ext-real Element of REAL
a1 + (C - a1) is complex real ext-real Element of REAL
b1 is complex real ext-real Element of REAL
{ b₁ where b₁ is complex real ext-real Element of REAL : ( not b₁ <= f & not C <= b₁ ) } is set
Rdiff (C2,a1) is complex real ext-real Element of REAL
Rdiff (b,a1) is complex real ext-real Element of REAL
C2 - b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
C2 + (- b) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(Rdiff (C2,a1)) - (Rdiff (b,a1)) is complex real ext-real Element of REAL
Rdiff ((C2 - b),a1) is complex real ext-real Element of REAL
{a1} is non empty V57() V58() V59() set
dom (C2 - b) is V57() V58() V59() Element of bool REAL
b1 is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of bool [:NAT,REAL:]
b1 " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
x1 is non empty Relation-like NAT -defined REAL -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng x1 is non empty V57() V58() V59() Element of bool REAL
b1 + x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng (b1 + x1) is non empty V57() V58() V59() Element of bool REAL
(C2 - b) /* (b1 + x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(C2 - b) /* x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- ((C2 - b) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) ((C2 - b) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((C2 - b) /* (b1 + x1)) + (- ((C2 - b) /* x1)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim ((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) is complex real ext-real Element of REAL
lim b1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() Element of REAL
(C - a1) / 2 is complex real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
Z1 is complex real ext-real set
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2 is complex real ext-real Element of REAL
b1 . a2 is complex real ext-real Element of REAL
(b1 . a2) - 0 is complex real ext-real Element of REAL
abs ((b1 . a2) - 0) is complex real ext-real Element of REAL
f + 0 is complex real ext-real Element of REAL
a1 + (b1 . a2) is complex real ext-real Element of REAL
a1 + ((C - a1) / 2) is complex real ext-real Element of REAL
(a1 + (b1 . a2)) + 0 is complex real ext-real Element of REAL
C - ((C - a1) / 2) is complex real ext-real Element of REAL
(C - ((C - a1) / 2)) + ((C - a1) / 2) is complex real ext-real Element of REAL
(dom C2) /\ (dom b) is V57() V58() V59() Element of bool REAL
lim x1 is complex real ext-real Element of REAL
x1 . a2 is complex real ext-real Element of REAL
(b1 + x1) . a2 is complex real ext-real Element of REAL
(b1 . a2) + (x1 . a2) is complex real ext-real Element of REAL
(b1 . a2) + a1 is complex real ext-real Element of REAL
b2 is set
(b1 ") . a2 is complex real ext-real Element of REAL
(((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1)) . a2 is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1)) . a2) is complex real ext-real Element of REAL
((C2 - b) /* (b1 + x1)) . a2 is complex real ext-real Element of REAL
((C2 - b) /* x1) . a2 is complex real ext-real Element of REAL
(((C2 - b) /* (b1 + x1)) . a2) - (((C2 - b) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C2 - b) /* (b1 + x1)) . a2) - (((C2 - b) /* x1) . a2)) is complex real ext-real Element of REAL
(C2 - b) . ((b1 + x1) . a2) is complex real ext-real Element of REAL
((C2 - b) . ((b1 + x1) . a2)) - (((C2 - b) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C2 - b) . ((b1 + x1) . a2)) - (((C2 - b) /* x1) . a2)) is complex real ext-real Element of REAL
(C2 - b) . (x1 . a2) is complex real ext-real Element of REAL
((C2 - b) . ((b1 + x1) . a2)) - ((C2 - b) . (x1 . a2)) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C2 - b) . ((b1 + x1) . a2)) - ((C2 - b) . (x1 . a2))) is complex real ext-real Element of REAL
(C2 - b) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C2 - b) . a1 is complex real ext-real Element of REAL
((C2 - b) . ((b1 . a2) + a1)) - ((C2 - b) . a1) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C2 - b) . ((b1 . a2) + a1)) - ((C2 - b) . a1)) is complex real ext-real Element of REAL
C2 . ((b1 . a2) + a1) is complex real ext-real Element of REAL
b . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C2 . ((b1 . a2) + a1)) - (b . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(C2 | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C2 | [.f,C.]) . ((b1 . a2) + a1)) - (b . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(b | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C2 | [.f,C.]) . ((b1 . a2) + a1)) - ((b | [.f,C.]) . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
C2 . a1 is complex real ext-real Element of REAL
b . a1 is complex real ext-real Element of REAL
(C2 . a1) - (b . a1) is complex real ext-real Element of REAL
(C2 | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C2 | [.f,C.]) . a1) - (b . a1) is complex real ext-real Element of REAL
(b | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C2 | [.f,C.]) . a1) - ((b | [.f,C.]) . a1) is complex real ext-real Element of REAL
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2 is complex real ext-real Element of REAL
(((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2) - 0 is complex real ext-real Element of REAL
abs ((((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2) - 0) is complex real ext-real Element of REAL
b1 is set
y1 is complex real ext-real Element of REAL
x1 is complex real ext-real Element of REAL
y1 is complex real ext-real Element of REAL
C2 | ].f,C.[ is Relation-like REAL -defined ].f,C.[ -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C2 | ].f,C.[) `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C2 `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C2 `| ].f,C.[) . a1 is complex real ext-real Element of REAL
b | ].f,C.[ is Relation-like REAL -defined ].f,C.[ -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b | ].f,C.[) `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b `| ].f,C.[ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b `| ].f,C.[) . a1 is complex real ext-real Element of REAL
dom (C2 | ].f,C.[) is V57() V58() V59() Element of bool REAL
(dom C2) /\ ].f,C.[ is V57() V58() V59() Element of bool REAL
(dom b) /\ ].f,C.[ is V57() V58() V59() Element of bool REAL
dom (b | ].f,C.[) is V57() V58() V59() Element of bool REAL
b1 is set
(C2 | ].f,C.[) . b1 is complex real ext-real Element of REAL
(b | ].f,C.[) . b1 is complex real ext-real Element of REAL
C2 . b1 is complex real ext-real Element of REAL
(C2 | [.f,C.]) . b1 is complex real ext-real Element of REAL
b . b1 is complex real ext-real Element of REAL
Ldiff (C2,a1) is complex real ext-real Element of REAL
Ldiff (b,a1) is complex real ext-real Element of REAL
C2 - b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
C2 + (- b) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(Ldiff (C2,a1)) - (Ldiff (b,a1)) is complex real ext-real Element of REAL
Ldiff ((C2 - b),a1) is complex real ext-real Element of REAL
{a1} is non empty V57() V58() V59() set
dom (C2 - b) is V57() V58() V59() Element of bool REAL
b1 is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of bool [:NAT,REAL:]
b1 " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
x1 is non empty Relation-like NAT -defined REAL -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng x1 is non empty V57() V58() V59() Element of bool REAL
b1 + x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng (b1 + x1) is non empty V57() V58() V59() Element of bool REAL
(C2 - b) /* (b1 + x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(C2 - b) /* x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- ((C2 - b) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) ((C2 - b) /* x1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((C2 - b) /* (b1 + x1)) + (- ((C2 - b) /* x1)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim ((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) is complex real ext-real Element of REAL
lim b1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V57() V58() V59() V60() V61() V62() V63() Element of REAL
(a1 - f) / 2 is complex real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
Z1 is complex real ext-real set
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2 is complex real ext-real Element of REAL
b1 . a2 is complex real ext-real Element of REAL
(b1 . a2) - 0 is complex real ext-real Element of REAL
abs ((b1 . a2) - 0) is complex real ext-real Element of REAL
- (b1 . a2) is complex real ext-real Element of REAL
a1 + (b1 . a2) is complex real ext-real Element of REAL
C + 0 is complex real ext-real Element of REAL
a1 - ((a1 - f) / 2) is complex real ext-real Element of REAL
a1 - (- (b1 . a2)) is complex real ext-real Element of REAL
f + ((a1 - f) / 2) is complex real ext-real Element of REAL
(f + ((a1 - f) / 2)) - ((a1 - f) / 2) is complex real ext-real Element of REAL
(a1 + (b1 . a2)) - 0 is complex real ext-real Element of REAL
(dom C2) /\ (dom b) is V57() V58() V59() Element of bool REAL
lim x1 is complex real ext-real Element of REAL
(b1 + x1) . a2 is complex real ext-real Element of REAL
x1 . a2 is complex real ext-real Element of REAL
(b1 . a2) + (x1 . a2) is complex real ext-real Element of REAL
(b1 . a2) + a1 is complex real ext-real Element of REAL
b2 is set
(b1 ") . a2 is complex real ext-real Element of REAL
(((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1)) . a2 is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1)) . a2) is complex real ext-real Element of REAL
((C2 - b) /* (b1 + x1)) . a2 is complex real ext-real Element of REAL
((C2 - b) /* x1) . a2 is complex real ext-real Element of REAL
(((C2 - b) /* (b1 + x1)) . a2) - (((C2 - b) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * ((((C2 - b) /* (b1 + x1)) . a2) - (((C2 - b) /* x1) . a2)) is complex real ext-real Element of REAL
(C2 - b) . ((b1 + x1) . a2) is complex real ext-real Element of REAL
((C2 - b) . ((b1 + x1) . a2)) - (((C2 - b) /* x1) . a2) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C2 - b) . ((b1 + x1) . a2)) - (((C2 - b) /* x1) . a2)) is complex real ext-real Element of REAL
(C2 - b) . (x1 . a2) is complex real ext-real Element of REAL
((C2 - b) . ((b1 + x1) . a2)) - ((C2 - b) . (x1 . a2)) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C2 - b) . ((b1 + x1) . a2)) - ((C2 - b) . (x1 . a2))) is complex real ext-real Element of REAL
(C2 - b) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C2 - b) . a1 is complex real ext-real Element of REAL
((C2 - b) . ((b1 . a2) + a1)) - ((C2 - b) . a1) is complex real ext-real Element of REAL
((b1 ") . a2) * (((C2 - b) . ((b1 . a2) + a1)) - ((C2 - b) . a1)) is complex real ext-real Element of REAL
C2 . ((b1 . a2) + a1) is complex real ext-real Element of REAL
b . ((b1 . a2) + a1) is complex real ext-real Element of REAL
(C2 . ((b1 . a2) + a1)) - (b . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(C2 | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C2 | [.f,C.]) . ((b1 . a2) + a1)) - (b . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
(b | [.f,C.]) . ((b1 . a2) + a1) is complex real ext-real Element of REAL
((C2 | [.f,C.]) . ((b1 . a2) + a1)) - ((b | [.f,C.]) . ((b1 . a2) + a1)) is complex real ext-real Element of REAL
C2 . a1 is complex real ext-real Element of REAL
b . a1 is complex real ext-real Element of REAL
(C2 . a1) - (b . a1) is complex real ext-real Element of REAL
(C2 | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C2 | [.f,C.]) . a1) - (b . a1) is complex real ext-real Element of REAL
(b | [.f,C.]) . a1 is complex real ext-real Element of REAL
((C2 | [.f,C.]) . a1) - ((b | [.f,C.]) . a1) is complex real ext-real Element of REAL
a2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V37() V38() V57() V58() V59() V60() V61() V62() Element of NAT
((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2 is complex real ext-real Element of REAL
(((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2) - 0 is complex real ext-real Element of REAL
abs ((((b1 ") (#) (((C2 - b) /* (b1 + x1)) - ((C2 - b) /* x1))) . a2) - 0) is complex real ext-real Element of REAL
((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((y (#) (a `| d)) - (Z (#) (b `| d))) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (C1 `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x (#) (C2 `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((b0 (#) (C1 `| d)) | u0) - ((x (#) (C2 `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- ((x (#) (C2 `| d)) | u0) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) ((x (#) (C2 `| d)) | u0) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
((b0 (#) (C1 `| d)) | u0) + (- ((x (#) (C2 `| d)) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(b0 | u0) (#) ((C1 `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((b0 | u0) (#) ((C1 `| d) | u0)) - ((x (#) (C2 `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((b0 | u0) (#) ((C1 `| d) | u0)) + (- ((x (#) (C2 `| d)) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(x | u0) (#) ((C2 `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((b0 | u0) (#) ((C1 `| d) | u0)) - ((x | u0) (#) ((C2 `| d) | u0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- ((x | u0) (#) ((C2 `| d) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) ((x | u0) (#) ((C2 `| d) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
((b0 | u0) (#) ((C1 `| d) | u0)) + (- ((x | u0) (#) ((C2 `| d) | u0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(y (#) (a `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(Z (#) (b `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((y (#) (a `| d)) | u0) - ((Z (#) (b `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- ((Z (#) (b `| d)) | u0) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) ((Z (#) (b `| d)) | u0) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
((y (#) (a `| d)) | u0) + (- ((Z (#) (b `| d)) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(y | u0) (#) ((a `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((y | u0) (#) ((a `| d) | u0)) - ((Z (#) (b `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((y | u0) (#) ((a `| d) | u0)) + (- ((Z (#) (b `| d)) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(Z | u0) (#) ((b `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((y | u0) (#) ((a `| d) | u0)) - ((Z | u0) (#) ((b `| d) | u0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- ((Z | u0) (#) ((b `| d) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) ((Z | u0) (#) ((b `| d) | u0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
((y | u0) (#) ((a `| d) | u0)) + (- ((Z | u0) (#) ((b `| d) | u0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),u0) is complex real ext-real Element of REAL
K298(((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),u0) is Relation-like u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:u0,REAL:]
[:u0,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:u0,REAL:] is non empty set
K659(u0,K298(((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),u0)) is complex real ext-real Element of REAL
integral (((y (#) (a `| d)) - (Z (#) (b `| d))),u0) is complex real ext-real Element of REAL
K298(((y (#) (a `| d)) - (Z (#) (b `| d))),u0) is Relation-like u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:u0,REAL:]
K659(u0,K298(((y (#) (a `| d)) - (Z (#) (b `| d))),u0)) is complex real ext-real Element of REAL
((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((Z (#) (a `| d)) + (y (#) (b `| d))) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x (#) (C1 `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (C2 `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((x (#) (C1 `| d)) | u0) + ((b0 (#) (C2 `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x | u0) (#) ((C1 `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((x | u0) (#) ((C1 `| d) | u0)) + ((b0 (#) (C2 `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 | u0) (#) ((C2 `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((x | u0) (#) ((C1 `| d) | u0)) + ((b0 | u0) (#) ((C2 `| d) | u0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(Z (#) (a `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(y (#) (b `| d)) | u0 is Relation-like REAL -defined u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((Z (#) (a `| d)) | u0) + ((y (#) (b `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(Z | u0) (#) ((a `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((Z | u0) (#) ((a `| d) | u0)) + ((y (#) (b `| d)) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(y | u0) (#) ((b `| d) | u0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((Z | u0) (#) ((a `| d) | u0)) + ((y | u0) (#) ((b `| d) | u0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),u0) is complex real ext-real Element of REAL
K298(((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),u0) is Relation-like u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:u0,REAL:]
K659(u0,K298(((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),u0)) is complex real ext-real Element of REAL
integral (((Z (#) (a `| d)) + (y (#) (b `| d))),u0) is complex real ext-real Element of REAL
K298(((Z (#) (a `| d)) + (y (#) (b `| d))),u0) is Relation-like u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:u0,REAL:]
K659(u0,K298(((Z (#) (a `| d)) + (y (#) (b `| d))),u0)) is complex real ext-real Element of REAL
[.C,f.] is V57() V58() V59() Element of bool REAL
v0 is non empty V57() V58() V59() closed_interval interval Element of bool REAL
integral (((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),v0) is complex real ext-real Element of REAL
K298(((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),v0) is Relation-like v0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:v0,REAL:]
[:v0,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:v0,REAL:] is non empty set
K659(v0,K298(((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),v0)) is complex real ext-real Element of REAL
- (integral (((b0 (#) (C1 `| d)) - (x (#) (C2 `| d))),v0)) is complex real ext-real Element of REAL
integral (((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),v0) is complex real ext-real Element of REAL
K298(((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),v0) is Relation-like v0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:v0,REAL:]
K659(v0,K298(((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),v0)) is complex real ext-real Element of REAL
- (integral (((x (#) (C1 `| d)) + (b0 (#) (C2 `| d))),v0)) is complex real ext-real Element of REAL
integral (((y (#) (a `| d)) - (Z (#) (b `| d))),v0) is complex real ext-real Element of REAL
K298(((y (#) (a `| d)) - (Z (#) (b `| d))),v0) is Relation-like v0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:v0,REAL:]
K659(v0,K298(((y (#) (a `| d)) - (Z (#) (b `| d))),v0)) is complex real ext-real Element of REAL
- (integral (((y (#) (a `| d)) - (Z (#) (b `| d))),f,C)) is complex real ext-real Element of REAL
u0 is non empty V57() V58() V59() closed_interval interval Element of bool REAL
integral (((Z (#) (a `| d)) + (y (#) (b `| d))),u0) is complex real ext-real Element of REAL
K298(((Z (#) (a `| d)) + (y (#) (b `| d))),u0) is Relation-like u0 -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:u0,REAL:]
[:u0,REAL:] is non empty Relation-like complex-valued ext-real-valued real-valued set
bool [:u0,REAL:] is non empty set
K659(u0,K298(((Z (#) (a `| d)) + (y (#) (b `| d))),u0)) is complex real ext-real Element of REAL
- (integral (((Z (#) (a `| d)) + (y (#) (b `| d))),f,C)) is complex real ext-real Element of REAL
C is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued () Element of bool [:REAL,COMPLEX:]
rng C is V57() Element of bool COMPLEX
bool COMPLEX is non empty set
f is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
dom f is V57() Element of bool COMPLEX
dom C is V57() V58() V59() Element of bool REAL
C1 is complex real ext-real Element of REAL
C2 is complex real ext-real Element of REAL
[.C1,C2.] is V57() V58() V59() Element of bool REAL
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom a is V57() V58() V59() Element of bool REAL
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V57() V58() V59() Element of bool REAL
d is V57() V58() V59() Element of bool REAL
a `| d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b `| d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) b is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
a + (<i> (#) b) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(a + (<i> (#) b)) | [.C1,C2.] is Relation-like REAL -defined [.C1,C2.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(C1,C2,a,b,d,f) is complex set
C1 is complex set
C2 is complex set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
[.a,b.] is V57() V58() V59() Element of bool REAL
d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom d is V57() V58() V59() Element of bool REAL
a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom a0 is V57() V58() V59() Element of bool REAL
b0 is V57() V58() V59() Element of bool REAL
d `| b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 `| b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) a0 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
d + (<i> (#) a0) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(d + (<i> (#) a0)) | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(a,b,d,a0,b0,f) is complex set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
[.a,b.] is V57() V58() V59() Element of bool REAL
d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom d is V57() V58() V59() Element of bool REAL
a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom a0 is V57() V58() V59() Element of bool REAL
b0 is V57() V58() V59() Element of bool REAL
d `| b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a0 `| b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) a0 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
d + (<i> (#) a0) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(d + (<i> (#) a0)) | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(a,b,d,a0,b0,f) is complex set
x is complex real ext-real Element of REAL
y is complex real ext-real Element of REAL
[.x,y.] is V57() V58() V59() Element of bool REAL
Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom Z is V57() V58() V59() Element of bool REAL
u0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom u0 is V57() V58() V59() Element of bool REAL
v0 is V57() V58() V59() Element of bool REAL
Z `| v0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 `| v0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) u0 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
Z + (<i> (#) u0) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(Z + (<i> (#) u0)) | [.x,y.] is Relation-like REAL -defined [.x,y.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(x,y,Z,u0,v0,f) is complex set
x is complex real ext-real Element of REAL
y is complex real ext-real Element of REAL
[.x,y.] is V57() V58() V59() Element of bool REAL
Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom Z is V57() V58() V59() Element of bool REAL
u0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom u0 is V57() V58() V59() Element of bool REAL
v0 is V57() V58() V59() Element of bool REAL
Z `| v0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 `| v0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) u0 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
Z + (<i> (#) u0) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(Z + (<i> (#) u0)) | [.x,y.] is Relation-like REAL -defined [.x,y.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(x,y,Z,u0,v0,f) is complex set
b0 /\ v0 is V57() V58() V59() Element of bool REAL
b1 is Element of bool the U1 of R^1
x1 is Element of bool the U1 of R^1
b1 /\ x1 is Element of bool the U1 of R^1
a1 is V57() V58() V59() Element of bool REAL
d | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z | [.x,y.] is Relation-like REAL -defined [.x,y.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is set
d . y1 is complex real ext-real Element of REAL
Z . y1 is complex real ext-real Element of REAL
dom (<i> (#) a0) is V57() V58() V59() Element of bool REAL
dom (d + (<i> (#) a0)) is V57() V58() V59() Element of bool REAL
(dom d) /\ (dom (<i> (#) a0)) is V57() V58() V59() Element of bool REAL
((d + (<i> (#) a0)) | [.a,b.]) . y1 is complex set
(d + (<i> (#) a0)) . y1 is complex set
(<i> (#) a0) . y1 is complex set
(d . y1) + ((<i> (#) a0) . y1) is complex set
a0 . y1 is complex real ext-real Element of REAL
<i> * (a0 . y1) is complex set
(d . y1) + (<i> * (a0 . y1)) is complex set
dom (<i> (#) u0) is V57() V58() V59() Element of bool REAL
dom (Z + (<i> (#) u0)) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (<i> (#) u0)) is V57() V58() V59() Element of bool REAL
((Z + (<i> (#) u0)) | [.x,y.]) . y1 is complex set
(Z + (<i> (#) u0)) . y1 is complex set
(<i> (#) u0) . y1 is complex set
(Z . y1) + ((<i> (#) u0) . y1) is complex set
u0 . y1 is complex real ext-real Element of REAL
<i> * (u0 . y1) is complex set
(Z . y1) + (<i> * (u0 . y1)) is complex set
a0 | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 | [.x,y.] is Relation-like REAL -defined [.x,y.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is set
a0 . y1 is complex real ext-real Element of REAL
u0 . y1 is complex real ext-real Element of REAL
dom (<i> (#) a0) is V57() V58() V59() Element of bool REAL
dom (d + (<i> (#) a0)) is V57() V58() V59() Element of bool REAL
(dom d) /\ (dom (<i> (#) a0)) is V57() V58() V59() Element of bool REAL
((d + (<i> (#) a0)) | [.a,b.]) . y1 is complex set
(d + (<i> (#) a0)) . y1 is complex set
d . y1 is complex real ext-real Element of REAL
(<i> (#) a0) . y1 is complex set
(d . y1) + ((<i> (#) a0) . y1) is complex set
<i> * (a0 . y1) is complex set
(d . y1) + (<i> * (a0 . y1)) is complex set
dom (<i> (#) u0) is V57() V58() V59() Element of bool REAL
dom (Z + (<i> (#) u0)) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (<i> (#) u0)) is V57() V58() V59() Element of bool REAL
((Z + (<i> (#) u0)) | [.x,y.]) . y1 is complex set
(Z + (<i> (#) u0)) . y1 is complex set
Z . y1 is complex real ext-real Element of REAL
(<i> (#) u0) . y1 is complex set
(Z . y1) + ((<i> (#) u0) . y1) is complex set
<i> * (u0 . y1) is complex set
(Z . y1) + (<i> * (u0 . y1)) is complex set
(a,b,d,a0,a1,f) is complex set
(x,y,Z,u0,a1,f) is complex set
f is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
dom f is V57() Element of bool COMPLEX
C is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
dom C is V57() Element of bool COMPLEX
f + C is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
C1 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued () Element of bool [:REAL,COMPLEX:]
rng C1 is V57() Element of bool COMPLEX
((f + C),C1) is complex set
(f,C1) is complex set
(C,C1) is complex set
(f,C1) + (C,C1) is complex set
dom C1 is V57() V58() V59() Element of bool REAL
C2 is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
[.C2,a.] is V57() V58() V59() Element of bool REAL
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V57() V58() V59() Element of bool REAL
d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom d is V57() V58() V59() Element of bool REAL
a0 is V57() V58() V59() Element of bool REAL
b `| a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
d `| a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) d is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
b + (<i> (#) d) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(b + (<i> (#) d)) | [.C2,a.] is Relation-like REAL -defined [.C2,a.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
<:b,d:> is Relation-like Function-like set
Re f is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re f) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Re f) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im f is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im f) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Im f) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
(C2,a,b,d,a0,f) is complex set
b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (b `| a0)) - (x (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (x (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (x (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(b0 (#) (b `| a0)) + (- (x (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
x (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x (#) (b `| a0)) + (b0 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) * <i> is complex set
(integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a)) + ((integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) * <i>) is complex set
Re C is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re C) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Re C) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im C is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im C) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Im C) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
(C2,a,b,d,a0,C) is complex set
y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(y (#) (b `| a0)) - (Z (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (Z (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (Z (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(y (#) (b `| a0)) + (- (Z (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((y (#) (b `| a0)) - (Z (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
Z (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(Z (#) (b `| a0)) + (y (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a)) * <i> is complex set
(integral (((y (#) (b `| a0)) - (Z (#) (d `| a0))),C2,a)) + ((integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a)) * <i>) is complex set
dom (f + C) is V57() Element of bool COMPLEX
(dom f) /\ (dom C) is V57() Element of bool COMPLEX
Re (f + C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re (f + C)) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Re (f + C)) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im (f + C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im (f + C)) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Im (f + C)) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
(C2,a,b,d,a0,(f + C)) is complex set
u0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
v0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
v0 (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u0 (#) (b `| a0)) - (v0 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (v0 (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (v0 (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(u0 (#) (b `| a0)) + (- (v0 (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((u0 (#) (b `| a0)) - (v0 (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
v0 (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(v0 (#) (b `| a0)) + (u0 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((v0 (#) (b `| a0)) + (u0 (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((v0 (#) (b `| a0)) + (u0 (#) (d `| a0))),C2,a)) * <i> is complex set
(integral (((u0 (#) (b `| a0)) - (v0 (#) (d `| a0))),C2,a)) + ((integral (((v0 (#) (b `| a0)) + (u0 (#) (d `| a0))),C2,a)) * <i>) is complex set
(b0 (#) (b `| a0)) + (y (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((b0 (#) (b `| a0)) + (y (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (y (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
(dom (b0 (#) (b `| a0))) /\ (dom (y (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom b0 is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (b `| a0))) /\ (dom (y (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom y is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (b `| a0))) /\ ((dom y) /\ (dom (b `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom y) /\ (dom (b `| a0))) is V57() V58() V59() Element of bool REAL
(dom b0) /\ ((dom (b `| a0)) /\ ((dom y) /\ (dom (b `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom (b `| a0)) /\ (dom (b `| a0))) /\ (dom y) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (((dom (b `| a0)) /\ (dom (b `| a0))) /\ (dom y)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom y) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom y)) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (u0 (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom u0 is V57() V58() V59() Element of bool REAL
(dom u0) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Re (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Re (f + C)) is V57() Element of bool COMPLEX
(Re f) + (Re C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Re f) + (Re C)) is V57() Element of bool COMPLEX
dom (Re f) is V57() Element of bool COMPLEX
dom (Re C) is V57() Element of bool COMPLEX
(dom (Re f)) /\ (dom (Re C)) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Re C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Re C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Re f) is V57() Element of bool COMPLEX
dom (Re C) is V57() Element of bool COMPLEX
(dom (Re f)) /\ (dom (Re C)) is V57() Element of bool COMPLEX
(Re f) + (Re C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Re f) + (Re C)) is V57() Element of bool COMPLEX
dom (Re (f + C)) is V57() Element of bool COMPLEX
dom ((Re (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
(u0 (#) (b `| a0)) . a1 is complex real ext-real Element of REAL
((b0 (#) (b `| a0)) + (y (#) (b `| a0))) . a1 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Re (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Re (f + C)) is V57() Element of bool COMPLEX
u0 . a1 is complex real ext-real Element of REAL
((Re (f + C)) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Re (f + C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(Re f) + (Re C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
((Re f) + (Re C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Re f) + (Re C)) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 . a1 is complex real ext-real Element of REAL
((Re f) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Re f) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Re C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y . a1 is complex real ext-real Element of REAL
((Re C) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Re C) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(b0 (#) (b `| a0)) . a1 is complex real ext-real Element of REAL
(b `| a0) . a1 is complex real ext-real Element of REAL
((Re f) . (() . (<:b,d:> . a1))) * ((b `| a0) . a1) is complex real ext-real Element of REAL
(y (#) (b `| a0)) . a1 is complex real ext-real Element of REAL
((Re C) . (() . (<:b,d:> . a1))) * ((b `| a0) . a1) is complex real ext-real Element of REAL
(u0 . a1) * ((b `| a0) . a1) is complex real ext-real Element of REAL
((Re f) . (() . (<:b,d:> . a1))) + ((Re C) . (() . (<:b,d:> . a1))) is complex real ext-real Element of REAL
(((Re f) . (() . (<:b,d:> . a1))) + ((Re C) . (() . (<:b,d:> . a1)))) * ((b `| a0) . a1) is complex real ext-real Element of REAL
((b0 (#) (b `| a0)) . a1) + ((y (#) (b `| a0)) . a1) is complex real ext-real Element of REAL
(x (#) (b `| a0)) + (Z (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((x (#) (b `| a0)) + (Z (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom (x (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (Z (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
(dom (x (#) (b `| a0))) /\ (dom (Z (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom x is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (b `| a0))) /\ (dom (Z (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom Z is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (b `| a0))) /\ ((dom Z) /\ (dom (b `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom Z) /\ (dom (b `| a0))) is V57() V58() V59() Element of bool REAL
(dom x) /\ ((dom (b `| a0)) /\ ((dom Z) /\ (dom (b `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom (b `| a0)) /\ (dom (b `| a0))) /\ (dom Z) is V57() V58() V59() Element of bool REAL
(dom x) /\ (((dom (b `| a0)) /\ (dom (b `| a0))) /\ (dom Z)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom Z) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom Z)) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (v0 (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom v0 is V57() V58() V59() Element of bool REAL
(dom v0) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Im (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Im (f + C)) is V57() Element of bool COMPLEX
(Im f) + (Im C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Im f) + (Im C)) is V57() Element of bool COMPLEX
dom (Im f) is V57() Element of bool COMPLEX
dom (Im C) is V57() Element of bool COMPLEX
(dom (Im f)) /\ (dom (Im C)) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Im C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Im C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Im f) is V57() Element of bool COMPLEX
dom (Im C) is V57() Element of bool COMPLEX
(dom (Im f)) /\ (dom (Im C)) is V57() Element of bool COMPLEX
(Im f) + (Im C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Im f) + (Im C)) is V57() Element of bool COMPLEX
dom (Im (f + C)) is V57() Element of bool COMPLEX
dom ((Im (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
(v0 (#) (b `| a0)) . a1 is complex real ext-real Element of REAL
((x (#) (b `| a0)) + (Z (#) (b `| a0))) . a1 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Im (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Im (f + C)) is V57() Element of bool COMPLEX
v0 . a1 is complex real ext-real Element of REAL
((Im (f + C)) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Im (f + C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(Im f) + (Im C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
((Im f) + (Im C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Im f) + (Im C)) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x . a1 is complex real ext-real Element of REAL
((Im f) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Im f) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Im C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z . a1 is complex real ext-real Element of REAL
((Im C) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Im C) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(x (#) (b `| a0)) . a1 is complex real ext-real Element of REAL
(b `| a0) . a1 is complex real ext-real Element of REAL
((Im f) . (() . (<:b,d:> . a1))) * ((b `| a0) . a1) is complex real ext-real Element of REAL
(Z (#) (b `| a0)) . a1 is complex real ext-real Element of REAL
((Im C) . (() . (<:b,d:> . a1))) * ((b `| a0) . a1) is complex real ext-real Element of REAL
(v0 . a1) * ((b `| a0) . a1) is complex real ext-real Element of REAL
((Im f) . (() . (<:b,d:> . a1))) + ((Im C) . (() . (<:b,d:> . a1))) is complex real ext-real Element of REAL
(((Im f) . (() . (<:b,d:> . a1))) + ((Im C) . (() . (<:b,d:> . a1)))) * ((b `| a0) . a1) is complex real ext-real Element of REAL
((x (#) (b `| a0)) . a1) + ((Z (#) (b `| a0)) . a1) is complex real ext-real Element of REAL
(b0 (#) (d `| a0)) + (y (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((b0 (#) (d `| a0)) + (y (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
dom (y (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (b0 (#) (d `| a0))) /\ (dom (y (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom b0 is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (d `| a0))) /\ (dom (y (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom y is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (d `| a0))) /\ ((dom y) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ ((dom y) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom b0) /\ ((dom (d `| a0)) /\ ((dom y) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom (d `| a0)) /\ (dom (d `| a0))) /\ (dom y) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (((dom (d `| a0)) /\ (dom (d `| a0))) /\ (dom y)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom y) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom y)) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
dom (u0 (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
dom u0 is V57() V58() V59() Element of bool REAL
(dom u0) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Re (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Re (f + C)) is V57() Element of bool COMPLEX
(Re f) + (Re C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Re f) + (Re C)) is V57() Element of bool COMPLEX
dom (Re f) is V57() Element of bool COMPLEX
dom (Re C) is V57() Element of bool COMPLEX
(dom (Re f)) /\ (dom (Re C)) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Re C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Re C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Re f) is V57() Element of bool COMPLEX
dom (Re C) is V57() Element of bool COMPLEX
(dom (Re f)) /\ (dom (Re C)) is V57() Element of bool COMPLEX
(Re f) + (Re C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Re f) + (Re C)) is V57() Element of bool COMPLEX
dom (Re (f + C)) is V57() Element of bool COMPLEX
dom ((Re (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
(u0 (#) (d `| a0)) . a1 is complex real ext-real Element of REAL
((b0 (#) (d `| a0)) + (y (#) (d `| a0))) . a1 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Re (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Re (f + C)) is V57() Element of bool COMPLEX
u0 . a1 is complex real ext-real Element of REAL
((Re (f + C)) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Re (f + C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(Re f) + (Re C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
((Re f) + (Re C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Re f) + (Re C)) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 . a1 is complex real ext-real Element of REAL
((Re f) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Re f) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Re C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y . a1 is complex real ext-real Element of REAL
((Re C) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Re C) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(b0 (#) (d `| a0)) . a1 is complex real ext-real Element of REAL
(d `| a0) . a1 is complex real ext-real Element of REAL
((Re f) . (() . (<:b,d:> . a1))) * ((d `| a0) . a1) is complex real ext-real Element of REAL
(y (#) (d `| a0)) . a1 is complex real ext-real Element of REAL
((Re C) . (() . (<:b,d:> . a1))) * ((d `| a0) . a1) is complex real ext-real Element of REAL
(u0 . a1) * ((d `| a0) . a1) is complex real ext-real Element of REAL
((Re f) . (() . (<:b,d:> . a1))) + ((Re C) . (() . (<:b,d:> . a1))) is complex real ext-real Element of REAL
(((Re f) . (() . (<:b,d:> . a1))) + ((Re C) . (() . (<:b,d:> . a1)))) * ((d `| a0) . a1) is complex real ext-real Element of REAL
((b0 (#) (d `| a0)) . a1) + ((y (#) (d `| a0)) . a1) is complex real ext-real Element of REAL
(x (#) (d `| a0)) + (Z (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((x (#) (d `| a0)) + (Z (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (x (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
dom (Z (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (x (#) (d `| a0))) /\ (dom (Z (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom x is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (d `| a0))) /\ (dom (Z (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom Z is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (d `| a0))) /\ ((dom Z) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ ((dom Z) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom x) /\ ((dom (d `| a0)) /\ ((dom Z) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom (d `| a0)) /\ (dom (d `| a0))) /\ (dom Z) is V57() V58() V59() Element of bool REAL
(dom x) /\ (((dom (d `| a0)) /\ (dom (d `| a0))) /\ (dom Z)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom Z) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom Z)) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
dom (v0 (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
dom v0 is V57() V58() V59() Element of bool REAL
(dom v0) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Im (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Im (f + C)) is V57() Element of bool COMPLEX
(Im f) + (Im C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Im f) + (Im C)) is V57() Element of bool COMPLEX
dom (Im f) is V57() Element of bool COMPLEX
dom (Im C) is V57() Element of bool COMPLEX
(dom (Im f)) /\ (dom (Im C)) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Im C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((Im C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Im f) is V57() Element of bool COMPLEX
dom (Im C) is V57() Element of bool COMPLEX
(dom (Im f)) /\ (dom (Im C)) is V57() Element of bool COMPLEX
(Im f) + (Im C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom ((Im f) + (Im C)) is V57() Element of bool COMPLEX
dom (Im (f + C)) is V57() Element of bool COMPLEX
dom ((Im (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a1 is set
(v0 (#) (d `| a0)) . a1 is complex real ext-real Element of REAL
((x (#) (d `| a0)) + (Z (#) (d `| a0))) . a1 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
dom ((Im (f + C)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . a1) is complex set
dom (Im (f + C)) is V57() Element of bool COMPLEX
v0 . a1 is complex real ext-real Element of REAL
((Im (f + C)) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Im (f + C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(Im f) + (Im C) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
((Im f) + (Im C)) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Im f) + (Im C)) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x . a1 is complex real ext-real Element of REAL
((Im f) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Im f) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
dom ((Im C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z . a1 is complex real ext-real Element of REAL
((Im C) * ()) . (<:b,d:> . a1) is complex real ext-real Element of REAL
(Im C) . (() . (<:b,d:> . a1)) is complex real ext-real Element of REAL
(x (#) (d `| a0)) . a1 is complex real ext-real Element of REAL
(d `| a0) . a1 is complex real ext-real Element of REAL
((Im f) . (() . (<:b,d:> . a1))) * ((d `| a0) . a1) is complex real ext-real Element of REAL
(Z (#) (d `| a0)) . a1 is complex real ext-real Element of REAL
((Im C) . (() . (<:b,d:> . a1))) * ((d `| a0) . a1) is complex real ext-real Element of REAL
(v0 . a1) * ((d `| a0) . a1) is complex real ext-real Element of REAL
((Im f) . (() . (<:b,d:> . a1))) + ((Im C) . (() . (<:b,d:> . a1))) is complex real ext-real Element of REAL
(((Im f) . (() . (<:b,d:> . a1))) + ((Im C) . (() . (<:b,d:> . a1)))) * ((d `| a0) . a1) is complex real ext-real Element of REAL
((x (#) (d `| a0)) . a1) + ((Z (#) (d `| a0)) . a1) is complex real ext-real Element of REAL
dom b0 is V57() V58() V59() Element of bool REAL
a1 is set
C1 . a1 is complex set
(dom b) /\ (dom d) is V57() V58() V59() Element of bool REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
b . a1 is complex real ext-real Element of REAL
d . a1 is complex real ext-real Element of REAL
[(b . a1),(d . a1)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) d) is V57() V58() V59() Element of bool REAL
(dom b) /\ (dom (<i> (#) d)) is V57() V58() V59() Element of bool REAL
dom (b + (<i> (#) d)) is V57() V58() V59() Element of bool REAL
[(b . a1),(d . a1)] `1 is set
[(b . a1),(d . a1)] `2 is set
(b + (<i> (#) d)) . a1 is complex set
(<i> (#) d) . a1 is complex set
(b . a1) + ((<i> (#) d) . a1) is complex set
<i> * (d . a1) is complex set
(b . a1) + (<i> * (d . a1)) is complex set
() . [(b . a1),(d . a1)] is complex set
() . (<:b,d:> . a1) is complex set
dom (Re f) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom x is V57() V58() V59() Element of bool REAL
a1 is set
C1 . a1 is complex set
(dom b) /\ (dom d) is V57() V58() V59() Element of bool REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
b . a1 is complex real ext-real Element of REAL
d . a1 is complex real ext-real Element of REAL
[(b . a1),(d . a1)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) d) is V57() V58() V59() Element of bool REAL
(dom b) /\ (dom (<i> (#) d)) is V57() V58() V59() Element of bool REAL
dom (b + (<i> (#) d)) is V57() V58() V59() Element of bool REAL
[(b . a1),(d . a1)] `1 is set
[(b . a1),(d . a1)] `2 is set
(b + (<i> (#) d)) . a1 is complex set
(<i> (#) d) . a1 is complex set
(b . a1) + ((<i> (#) d) . a1) is complex set
<i> * (d . a1) is complex set
(b . a1) + (<i> * (d . a1)) is complex set
() . [(b . a1),(d . a1)] is complex set
() . (<:b,d:> . a1) is complex set
dom (Im f) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom y is V57() V58() V59() Element of bool REAL
a1 is set
C1 . a1 is complex set
(dom b) /\ (dom d) is V57() V58() V59() Element of bool REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
b . a1 is complex real ext-real Element of REAL
d . a1 is complex real ext-real Element of REAL
[(b . a1),(d . a1)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) d) is V57() V58() V59() Element of bool REAL
(dom b) /\ (dom (<i> (#) d)) is V57() V58() V59() Element of bool REAL
dom (b + (<i> (#) d)) is V57() V58() V59() Element of bool REAL
[(b . a1),(d . a1)] `1 is set
[(b . a1),(d . a1)] `2 is set
(b + (<i> (#) d)) . a1 is complex set
(<i> (#) d) . a1 is complex set
(b . a1) + ((<i> (#) d) . a1) is complex set
<i> * (d . a1) is complex set
(b . a1) + (<i> * (d . a1)) is complex set
() . [(b . a1),(d . a1)] is complex set
() . (<:b,d:> . a1) is complex set
dom (Re C) is V57() Element of bool COMPLEX
dom ((Re C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom Z is V57() V58() V59() Element of bool REAL
a1 is set
C1 . a1 is complex set
(dom b) /\ (dom d) is V57() V58() V59() Element of bool REAL
proj1 <:b,d:> is set
<:b,d:> . a1 is set
b . a1 is complex real ext-real Element of REAL
d . a1 is complex real ext-real Element of REAL
[(b . a1),(d . a1)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) d) is V57() V58() V59() Element of bool REAL
(dom b) /\ (dom (<i> (#) d)) is V57() V58() V59() Element of bool REAL
dom (b + (<i> (#) d)) is V57() V58() V59() Element of bool REAL
[(b . a1),(d . a1)] `1 is set
[(b . a1),(d . a1)] `2 is set
(b + (<i> (#) d)) . a1 is complex set
(<i> (#) d) . a1 is complex set
(b . a1) + ((<i> (#) d) . a1) is complex set
<i> * (d . a1) is complex set
(b . a1) + (<i> * (d . a1)) is complex set
() . [(b . a1),(d . a1)] is complex set
() . (<:b,d:> . a1) is complex set
dom (Im C) is V57() Element of bool COMPLEX
dom ((Im C) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
['C2,a'] is non empty V57() V58() V59() closed_interval interval Element of bool REAL
dom ((b0 (#) (b `| a0)) - (x (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (x (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (b0 (#) (b `| a0))) /\ (dom (x (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (b `| a0))) /\ (dom (x (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (b `| a0))) /\ ((dom x) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom x) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom b0) /\ ((dom (b `| a0)) /\ ((dom x) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom x) is V57() V58() V59() Element of bool REAL
a0 /\ ((dom (d `| a0)) /\ (dom x)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (a0 /\ ((dom (d `| a0)) /\ (dom x))) is V57() V58() V59() Element of bool REAL
a0 /\ (dom x) is V57() V58() V59() Element of bool REAL
a0 /\ (a0 /\ (dom x)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (a0 /\ (a0 /\ (dom x))) is V57() V58() V59() Element of bool REAL
a0 /\ a0 is V57() V58() V59() Element of bool REAL
(a0 /\ a0) /\ (dom x) is V57() V58() V59() Element of bool REAL
(dom b0) /\ ((a0 /\ a0) /\ (dom x)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom x) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom x)) /\ a0 is V57() V58() V59() Element of bool REAL
dom ((y (#) (b `| a0)) - (Z (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (y (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (Z (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (y (#) (b `| a0))) /\ (dom (Z (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom y) /\ (dom (b `| a0))) /\ (dom (Z (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom y) /\ (dom (b `| a0))) /\ ((dom Z) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom Z) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom y) /\ ((dom (b `| a0)) /\ ((dom Z) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom Z) is V57() V58() V59() Element of bool REAL
a0 /\ ((dom (d `| a0)) /\ (dom Z)) is V57() V58() V59() Element of bool REAL
(dom y) /\ (a0 /\ ((dom (d `| a0)) /\ (dom Z))) is V57() V58() V59() Element of bool REAL
a0 /\ (dom Z) is V57() V58() V59() Element of bool REAL
a0 /\ (a0 /\ (dom Z)) is V57() V58() V59() Element of bool REAL
(dom y) /\ (a0 /\ (a0 /\ (dom Z))) is V57() V58() V59() Element of bool REAL
a0 /\ a0 is V57() V58() V59() Element of bool REAL
(a0 /\ a0) /\ (dom Z) is V57() V58() V59() Element of bool REAL
(dom y) /\ ((a0 /\ a0) /\ (dom Z)) is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom Z) is V57() V58() V59() Element of bool REAL
((dom y) /\ (dom Z)) /\ a0 is V57() V58() V59() Element of bool REAL
dom ((x (#) (b `| a0)) + (b0 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (x (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (x (#) (b `| a0))) /\ (dom (b0 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (b `| a0))) /\ (dom (b0 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (b `| a0))) /\ ((dom b0) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom b0) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom x) /\ ((dom (b `| a0)) /\ ((dom b0) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom b0) is V57() V58() V59() Element of bool REAL
a0 /\ ((dom (d `| a0)) /\ (dom b0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (a0 /\ ((dom (d `| a0)) /\ (dom b0))) is V57() V58() V59() Element of bool REAL
a0 /\ (dom b0) is V57() V58() V59() Element of bool REAL
a0 /\ (a0 /\ (dom b0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (a0 /\ (a0 /\ (dom b0))) is V57() V58() V59() Element of bool REAL
a0 /\ a0 is V57() V58() V59() Element of bool REAL
(a0 /\ a0) /\ (dom b0) is V57() V58() V59() Element of bool REAL
(dom x) /\ ((a0 /\ a0) /\ (dom b0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom b0) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom b0)) /\ a0 is V57() V58() V59() Element of bool REAL
dom ((Z (#) (b `| a0)) + (y (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (Z (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (y (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (Z (#) (b `| a0))) /\ (dom (y (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom Z) /\ (dom (b `| a0))) /\ (dom (y (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom Z) /\ (dom (b `| a0))) /\ ((dom y) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom y) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom Z) /\ ((dom (b `| a0)) /\ ((dom y) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom y) is V57() V58() V59() Element of bool REAL
a0 /\ ((dom (d `| a0)) /\ (dom y)) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (a0 /\ ((dom (d `| a0)) /\ (dom y))) is V57() V58() V59() Element of bool REAL
a0 /\ (dom y) is V57() V58() V59() Element of bool REAL
a0 /\ (a0 /\ (dom y)) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (a0 /\ (a0 /\ (dom y))) is V57() V58() V59() Element of bool REAL
a0 /\ a0 is V57() V58() V59() Element of bool REAL
(a0 /\ a0) /\ (dom y) is V57() V58() V59() Element of bool REAL
(dom Z) /\ ((a0 /\ a0) /\ (dom y)) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom y) is V57() V58() V59() Element of bool REAL
((dom Z) /\ (dom y)) /\ a0 is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom Z) is V57() V58() V59() Element of bool REAL
((b0 (#) (b `| a0)) - (x (#) (d `| a0))) | ['C2,a'] is Relation-like REAL -defined ['C2,a'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((y (#) (b `| a0)) - (Z (#) (d `| a0))) | ['C2,a'] is Relation-like REAL -defined ['C2,a'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((x (#) (b `| a0)) + (b0 (#) (d `| a0))) | ['C2,a'] is Relation-like REAL -defined ['C2,a'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((Z (#) (b `| a0)) + (y (#) (d `| a0))) | ['C2,a'] is Relation-like REAL -defined ['C2,a'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - ((x (#) (d `| a0)) + (Z (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- ((x (#) (d `| a0)) + (Z (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) ((x (#) (d `| a0)) + (Z (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
((b0 (#) (b `| a0)) + (y (#) (b `| a0))) + (- ((x (#) (d `| a0)) + (Z (#) (d `| a0)))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral ((((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - ((x (#) (d `| a0)) + (Z (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
((x (#) (b `| a0)) + (Z (#) (b `| a0))) + ((b0 (#) (d `| a0)) + (y (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral ((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + ((b0 (#) (d `| a0)) + (y (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
(integral ((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + ((b0 (#) (d `| a0)) + (y (#) (d `| a0)))),C2,a)) * <i> is complex set
(integral ((((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - ((x (#) (d `| a0)) + (Z (#) (d `| a0)))),C2,a)) + ((integral ((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + ((b0 (#) (d `| a0)) + (y (#) (d `| a0)))),C2,a)) * <i>) is complex set
((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - (x (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((b0 (#) (b `| a0)) + (y (#) (b `| a0))) + (- (x (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - (x (#) (d `| a0))) - (Z (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - (x (#) (d `| a0))) + (- (Z (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - (x (#) (d `| a0))) - (Z (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - (x (#) (d `| a0))) - (Z (#) (d `| a0))),C2,a)) + ((integral ((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + ((b0 (#) (d `| a0)) + (y (#) (d `| a0)))),C2,a)) * <i>) is complex set
((x (#) (b `| a0)) + (Z (#) (b `| a0))) + (b0 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(((x (#) (b `| a0)) + (Z (#) (b `| a0))) + (b0 (#) (d `| a0))) + (y (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + (b0 (#) (d `| a0))) + (y (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + (b0 (#) (d `| a0))) + (y (#) (d `| a0))),C2,a)) * <i> is complex set
(integral (((((b0 (#) (b `| a0)) + (y (#) (b `| a0))) - (x (#) (d `| a0))) - (Z (#) (d `| a0))),C2,a)) + ((integral (((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + (b0 (#) (d `| a0))) + (y (#) (d `| a0))),C2,a)) * <i>) is complex set
((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + (y (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + (y (#) (b `| a0))) - (Z (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + (y (#) (b `| a0))) + (- (Z (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + (y (#) (b `| a0))) - (Z (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + (y (#) (b `| a0))) - (Z (#) (d `| a0))),C2,a)) + ((integral (((((x (#) (b `| a0)) + (Z (#) (b `| a0))) + (b0 (#) (d `| a0))) + (y (#) (d `| a0))),C2,a)) * <i>) is complex set
((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + (Z (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + (Z (#) (b `| a0))) + (y (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + (Z (#) (b `| a0))) + (y (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + (Z (#) (b `| a0))) + (y (#) (d `| a0))),C2,a)) * <i> is complex set
(integral (((((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + (y (#) (b `| a0))) - (Z (#) (d `| a0))),C2,a)) + ((integral (((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + (Z (#) (b `| a0))) + (y (#) (d `| a0))),C2,a)) * <i>) is complex set
((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + ((y (#) (b `| a0)) - (Z (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral ((((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + ((y (#) (b `| a0)) - (Z (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
(integral ((((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + ((y (#) (b `| a0)) - (Z (#) (d `| a0)))),C2,a)) + ((integral (((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + (Z (#) (b `| a0))) + (y (#) (d `| a0))),C2,a)) * <i>) is complex set
((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + ((Z (#) (b `| a0)) + (y (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral ((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + ((Z (#) (b `| a0)) + (y (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
(integral ((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + ((Z (#) (b `| a0)) + (y (#) (d `| a0)))),C2,a)) * <i> is complex set
(integral ((((b0 (#) (b `| a0)) - (x (#) (d `| a0))) + ((y (#) (b `| a0)) - (Z (#) (d `| a0)))),C2,a)) + ((integral ((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + ((Z (#) (b `| a0)) + (y (#) (d `| a0)))),C2,a)) * <i>) is complex set
(integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a)) + (integral (((y (#) (b `| a0)) - (Z (#) (d `| a0))),C2,a)) is complex real ext-real Element of REAL
((integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a)) + (integral (((y (#) (b `| a0)) - (Z (#) (d `| a0))),C2,a))) + ((integral ((((x (#) (b `| a0)) + (b0 (#) (d `| a0))) + ((Z (#) (b `| a0)) + (y (#) (d `| a0)))),C2,a)) * <i>) is complex set
(integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) + (integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a)) is complex real ext-real Element of REAL
((integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) + (integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a))) * <i> is complex set
((integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a)) + (integral (((y (#) (b `| a0)) - (Z (#) (d `| a0))),C2,a))) + (((integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) + (integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a))) * <i>) is complex set
f is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
dom f is V57() Element of bool COMPLEX
C is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued () Element of bool [:REAL,COMPLEX:]
rng C is V57() Element of bool COMPLEX
(f,C) is complex set
C1 is complex real ext-real Element of REAL
C1 (#) f is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
((C1 (#) f),C) is complex set
C1 * (f,C) is complex set
dom C is V57() V58() V59() Element of bool REAL
C2 is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
[.C2,a.] is V57() V58() V59() Element of bool REAL
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V57() V58() V59() Element of bool REAL
d is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom d is V57() V58() V59() Element of bool REAL
a0 is V57() V58() V59() Element of bool REAL
b `| a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
d `| a0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) d is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
b + (<i> (#) d) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(b + (<i> (#) d)) | [.C2,a.] is Relation-like REAL -defined [.C2,a.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
<:b,d:> is Relation-like Function-like set
Re f is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re f) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Re f) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im f is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im f) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Im f) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
(C2,a,b,d,a0,f) is complex set
b0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b0 (#) (b `| a0)) - (x (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (x (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (x (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(b0 (#) (b `| a0)) + (- (x (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
x (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(x (#) (b `| a0)) + (b0 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) * <i> is complex set
(integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a)) + ((integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) * <i>) is complex set
dom (C1 (#) f) is V57() Element of bool COMPLEX
Re (C1 (#) f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re (C1 (#) f)) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Re (C1 (#) f)) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im (C1 (#) f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im (C1 (#) f)) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:b,d:> (#) ((Im (C1 (#) f)) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
(C2,a,b,d,a0,(C1 (#) f)) is complex set
y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
Z (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(y (#) (b `| a0)) - (Z (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (Z (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (Z (#) (d `| a0)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(y (#) (b `| a0)) + (- (Z (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((y (#) (b `| a0)) - (Z (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
Z (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(Z (#) (b `| a0)) + (y (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a) is complex real ext-real Element of REAL
(integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a)) * <i> is complex set
(integral (((y (#) (b `| a0)) - (Z (#) (d `| a0))),C2,a)) + ((integral (((Z (#) (b `| a0)) + (y (#) (d `| a0))),C2,a)) * <i>) is complex set
dom y is V57() V58() V59() Element of bool REAL
dom b0 is V57() V58() V59() Element of bool REAL
u0 is set
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Re (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
dom (Re (C1 (#) f)) is V57() Element of bool COMPLEX
C1 (#) (Re f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom (C1 (#) (Re f)) is V57() Element of bool COMPLEX
dom (Re f) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 is set
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
dom (Re f) is V57() Element of bool COMPLEX
C1 (#) (Re f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom (C1 (#) (Re f)) is V57() Element of bool COMPLEX
dom (Re (C1 (#) f)) is V57() Element of bool COMPLEX
dom ((Re (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom Z is V57() V58() V59() Element of bool REAL
dom x is V57() V58() V59() Element of bool REAL
u0 is set
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Im (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
dom (Im (C1 (#) f)) is V57() Element of bool COMPLEX
C1 (#) (Im f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom (C1 (#) (Im f)) is V57() Element of bool COMPLEX
dom (Im f) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 is set
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
dom (Im f) is V57() Element of bool COMPLEX
C1 (#) (Im f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
dom (C1 (#) (Im f)) is V57() Element of bool COMPLEX
dom (Im (C1 (#) f)) is V57() Element of bool COMPLEX
dom ((Im (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
C1 (#) (b0 (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (C1 (#) (b0 (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
C1 (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (C1 (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (b0 (#) (C1 (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom (C1 (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (C1 (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (y (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
u0 is set
(y (#) (b `| a0)) . u0 is complex real ext-real Element of REAL
(C1 (#) (b0 (#) (b `| a0))) . u0 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Re (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
y . u0 is complex real ext-real Element of REAL
((Re (C1 (#) f)) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Re (C1 (#) f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
C1 (#) (Re f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(C1 (#) (Re f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 . u0 is complex real ext-real Element of REAL
((Re f) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Re f) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
(b `| a0) . u0 is complex real ext-real Element of REAL
(y . u0) * ((b `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((Re f) . (() . (<:b,d:> . u0))) is complex real ext-real Element of REAL
(C1 * ((Re f) . (() . (<:b,d:> . u0)))) * ((b `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((b `| a0) . u0) is complex real ext-real Element of REAL
(b0 . u0) * (C1 * ((b `| a0) . u0)) is complex real ext-real Element of REAL
(C1 (#) (b `| a0)) . u0 is complex real ext-real Element of REAL
(b0 . u0) * ((C1 (#) (b `| a0)) . u0) is complex real ext-real Element of REAL
(b0 (#) (C1 (#) (b `| a0))) . u0 is complex real ext-real Element of REAL
C1 (#) (x (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (C1 (#) (x (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
C1 (#) (b `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (C1 (#) (b `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (x (#) (C1 (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom (C1 (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (C1 (#) (b `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (Z (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
u0 is set
(Z (#) (b `| a0)) . u0 is complex real ext-real Element of REAL
(C1 (#) (x (#) (b `| a0))) . u0 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Im (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
Z . u0 is complex real ext-real Element of REAL
((Im (C1 (#) f)) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Im (C1 (#) f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
C1 (#) (Im f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(C1 (#) (Im f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x . u0 is complex real ext-real Element of REAL
((Im f) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Im f) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
(b `| a0) . u0 is complex real ext-real Element of REAL
(Z . u0) * ((b `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((Im f) . (() . (<:b,d:> . u0))) is complex real ext-real Element of REAL
(C1 * ((Im f) . (() . (<:b,d:> . u0)))) * ((b `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((b `| a0) . u0) is complex real ext-real Element of REAL
(x . u0) * (C1 * ((b `| a0) . u0)) is complex real ext-real Element of REAL
(C1 (#) (b `| a0)) . u0 is complex real ext-real Element of REAL
(x . u0) * ((C1 (#) (b `| a0)) . u0) is complex real ext-real Element of REAL
(x (#) (C1 (#) (b `| a0))) . u0 is complex real ext-real Element of REAL
C1 (#) (b0 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (C1 (#) (b0 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
C1 (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 (#) (C1 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (b0 (#) (C1 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (C1 (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (C1 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
dom (y (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom y) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
u0 is set
(y (#) (d `| a0)) . u0 is complex real ext-real Element of REAL
(C1 (#) (b0 (#) (d `| a0))) . u0 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Re (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
y . u0 is complex real ext-real Element of REAL
((Re (C1 (#) f)) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Re (C1 (#) f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
C1 (#) (Re f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(C1 (#) (Re f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b0 . u0 is complex real ext-real Element of REAL
((Re f) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Re f) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
(d `| a0) . u0 is complex real ext-real Element of REAL
(y . u0) * ((d `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((Re f) . (() . (<:b,d:> . u0))) is complex real ext-real Element of REAL
(C1 * ((Re f) . (() . (<:b,d:> . u0)))) * ((d `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((d `| a0) . u0) is complex real ext-real Element of REAL
(b0 . u0) * (C1 * ((d `| a0) . u0)) is complex real ext-real Element of REAL
(C1 (#) (d `| a0)) . u0 is complex real ext-real Element of REAL
(b0 . u0) * ((C1 (#) (d `| a0)) . u0) is complex real ext-real Element of REAL
(b0 (#) (C1 (#) (d `| a0))) . u0 is complex real ext-real Element of REAL
C1 (#) (x (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (C1 (#) (x (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
C1 (#) (d `| a0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x (#) (C1 (#) (d `| a0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (x (#) (C1 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (C1 (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (C1 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
dom (Z (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom Z) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
u0 is set
(Z (#) (d `| a0)) . u0 is complex real ext-real Element of REAL
(C1 (#) (x (#) (d `| a0))) . u0 is complex real ext-real Element of REAL
proj1 <:b,d:> is set
<:b,d:> . u0 is set
dom ((Im (C1 (#) f)) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
() . (<:b,d:> . u0) is complex set
Z . u0 is complex real ext-real Element of REAL
((Im (C1 (#) f)) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Im (C1 (#) f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
C1 (#) (Im f) is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(C1 (#) (Im f)) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x . u0 is complex real ext-real Element of REAL
((Im f) * ()) . (<:b,d:> . u0) is complex real ext-real Element of REAL
(Im f) . (() . (<:b,d:> . u0)) is complex real ext-real Element of REAL
(d `| a0) . u0 is complex real ext-real Element of REAL
(Z . u0) * ((d `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((Im f) . (() . (<:b,d:> . u0))) is complex real ext-real Element of REAL
(C1 * ((Im f) . (() . (<:b,d:> . u0)))) * ((d `| a0) . u0) is complex real ext-real Element of REAL
C1 * ((d `| a0) . u0) is complex real ext-real Element of REAL
(x . u0) * (C1 * ((d `| a0) . u0)) is complex real ext-real Element of REAL
(C1 (#) (d `| a0)) . u0 is complex real ext-real Element of REAL
(x . u0) * ((C1 (#) (d `| a0)) . u0) is complex real ext-real Element of REAL
(x (#) (C1 (#) (d `| a0))) . u0 is complex real ext-real Element of REAL
u0 is set
C . u0 is complex set
(dom b) /\ (dom d) is V57() V58() V59() Element of bool REAL
proj1 <:b,d:> is set
<:b,d:> . u0 is set
b . u0 is complex real ext-real Element of REAL
d . u0 is complex real ext-real Element of REAL
[(b . u0),(d . u0)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) d) is V57() V58() V59() Element of bool REAL
(dom b) /\ (dom (<i> (#) d)) is V57() V58() V59() Element of bool REAL
dom (b + (<i> (#) d)) is V57() V58() V59() Element of bool REAL
[(b . u0),(d . u0)] `1 is set
[(b . u0),(d . u0)] `2 is set
(b + (<i> (#) d)) . u0 is complex set
(<i> (#) d) . u0 is complex set
(b . u0) + ((<i> (#) d) . u0) is complex set
<i> * (d . u0) is complex set
(b . u0) + (<i> * (d . u0)) is complex set
() . [(b . u0),(d . u0)] is complex set
() . (<:b,d:> . u0) is complex set
dom (Re f) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 is set
C . u0 is complex set
(dom b) /\ (dom d) is V57() V58() V59() Element of bool REAL
proj1 <:b,d:> is set
<:b,d:> . u0 is set
b . u0 is complex real ext-real Element of REAL
d . u0 is complex real ext-real Element of REAL
[(b . u0),(d . u0)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) d) is V57() V58() V59() Element of bool REAL
(dom b) /\ (dom (<i> (#) d)) is V57() V58() V59() Element of bool REAL
dom (b + (<i> (#) d)) is V57() V58() V59() Element of bool REAL
[(b . u0),(d . u0)] `1 is set
[(b . u0),(d . u0)] `2 is set
(b + (<i> (#) d)) . u0 is complex set
(<i> (#) d) . u0 is complex set
(b . u0) + ((<i> (#) d) . u0) is complex set
<i> * (d . u0) is complex set
(b . u0) + (<i> * (d . u0)) is complex set
() . [(b . u0),(d . u0)] is complex set
() . (<:b,d:> . u0) is complex set
dom (Im f) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
['C2,a'] is non empty V57() V58() V59() closed_interval interval Element of bool REAL
dom ((b0 (#) (b `| a0)) - (x (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (x (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (b0 (#) (b `| a0))) /\ (dom (x (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (b `| a0))) /\ (dom (x (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom (b `| a0))) /\ ((dom x) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom x) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom b0) /\ ((dom (b `| a0)) /\ ((dom x) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom x) is V57() V58() V59() Element of bool REAL
a0 /\ ((dom (d `| a0)) /\ (dom x)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (a0 /\ ((dom (d `| a0)) /\ (dom x))) is V57() V58() V59() Element of bool REAL
a0 /\ (dom x) is V57() V58() V59() Element of bool REAL
a0 /\ (a0 /\ (dom x)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (a0 /\ (a0 /\ (dom x))) is V57() V58() V59() Element of bool REAL
a0 /\ a0 is V57() V58() V59() Element of bool REAL
(a0 /\ a0) /\ (dom x) is V57() V58() V59() Element of bool REAL
(dom b0) /\ ((a0 /\ a0) /\ (dom x)) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom x) is V57() V58() V59() Element of bool REAL
((dom b0) /\ (dom x)) /\ a0 is V57() V58() V59() Element of bool REAL
dom ((x (#) (b `| a0)) + (b0 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (x (#) (b `| a0)) is V57() V58() V59() Element of bool REAL
dom (b0 (#) (d `| a0)) is V57() V58() V59() Element of bool REAL
(dom (x (#) (b `| a0))) /\ (dom (b0 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (b `| a0) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (b `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (b `| a0))) /\ (dom (b0 (#) (d `| a0))) is V57() V58() V59() Element of bool REAL
dom (d `| a0) is V57() V58() V59() Element of bool REAL
(dom b0) /\ (dom (d `| a0)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (b `| a0))) /\ ((dom b0) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom (b `| a0)) /\ ((dom b0) /\ (dom (d `| a0))) is V57() V58() V59() Element of bool REAL
(dom x) /\ ((dom (b `| a0)) /\ ((dom b0) /\ (dom (d `| a0)))) is V57() V58() V59() Element of bool REAL
(dom (d `| a0)) /\ (dom b0) is V57() V58() V59() Element of bool REAL
a0 /\ ((dom (d `| a0)) /\ (dom b0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (a0 /\ ((dom (d `| a0)) /\ (dom b0))) is V57() V58() V59() Element of bool REAL
a0 /\ (dom b0) is V57() V58() V59() Element of bool REAL
a0 /\ (a0 /\ (dom b0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (a0 /\ (a0 /\ (dom b0))) is V57() V58() V59() Element of bool REAL
a0 /\ a0 is V57() V58() V59() Element of bool REAL
(a0 /\ a0) /\ (dom b0) is V57() V58() V59() Element of bool REAL
(dom x) /\ ((a0 /\ a0) /\ (dom b0)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom b0) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom b0)) /\ a0 is V57() V58() V59() Element of bool REAL
((b0 (#) (b `| a0)) - (x (#) (d `| a0))) | ['C2,a'] is Relation-like REAL -defined ['C2,a'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((x (#) (b `| a0)) + (b0 (#) (d `| a0))) | ['C2,a'] is Relation-like REAL -defined ['C2,a'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(C1 (#) (b0 (#) (b `| a0))) - (C1 (#) (x (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (C1 (#) (x (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (C1 (#) (x (#) (d `| a0))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(C1 (#) (b0 (#) (b `| a0))) + (- (C1 (#) (x (#) (d `| a0)))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((C1 (#) (b0 (#) (b `| a0))) - (C1 (#) (x (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
(C1 (#) (x (#) (b `| a0))) + (C1 (#) (b0 (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((C1 (#) (x (#) (b `| a0))) + (C1 (#) (b0 (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
(integral (((C1 (#) (x (#) (b `| a0))) + (C1 (#) (b0 (#) (d `| a0)))),C2,a)) * <i> is complex set
(integral (((C1 (#) (b0 (#) (b `| a0))) - (C1 (#) (x (#) (d `| a0)))),C2,a)) + ((integral (((C1 (#) (x (#) (b `| a0))) + (C1 (#) (b0 (#) (d `| a0)))),C2,a)) * <i>) is complex set
C1 (#) ((b0 (#) (b `| a0)) - (x (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral ((C1 (#) ((b0 (#) (b `| a0)) - (x (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
(integral ((C1 (#) ((b0 (#) (b `| a0)) - (x (#) (d `| a0)))),C2,a)) + ((integral (((C1 (#) (x (#) (b `| a0))) + (C1 (#) (b0 (#) (d `| a0)))),C2,a)) * <i>) is complex set
C1 (#) ((x (#) (b `| a0)) + (b0 (#) (d `| a0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral ((C1 (#) ((x (#) (b `| a0)) + (b0 (#) (d `| a0)))),C2,a) is complex real ext-real Element of REAL
(integral ((C1 (#) ((x (#) (b `| a0)) + (b0 (#) (d `| a0)))),C2,a)) * <i> is complex set
(integral ((C1 (#) ((b0 (#) (b `| a0)) - (x (#) (d `| a0)))),C2,a)) + ((integral ((C1 (#) ((x (#) (b `| a0)) + (b0 (#) (d `| a0)))),C2,a)) * <i>) is complex set
C1 * (integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a)) is complex real ext-real Element of REAL
(C1 * (integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a))) + ((integral ((C1 (#) ((x (#) (b `| a0)) + (b0 (#) (d `| a0)))),C2,a)) * <i>) is complex set
C1 * (integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) is complex real ext-real Element of REAL
(C1 * (integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a))) * <i> is complex set
(C1 * (integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a))) + ((C1 * (integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a))) * <i>) is complex set
C1 * ((integral (((b0 (#) (b `| a0)) - (x (#) (d `| a0))),C2,a)) + ((integral (((x (#) (b `| a0)) + (b0 (#) (d `| a0))),C2,a)) * <i>)) is complex set
f is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-valued Element of bool [:COMPLEX,COMPLEX:]
dom f is V57() Element of bool COMPLEX
C is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued () Element of bool [:REAL,COMPLEX:]
rng C is V57() Element of bool COMPLEX
dom C is V57() V58() V59() Element of bool REAL
C1 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued () Element of bool [:REAL,COMPLEX:]
dom C1 is V57() V58() V59() Element of bool REAL
C2 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued () Element of bool [:REAL,COMPLEX:]
dom C2 is V57() V58() V59() Element of bool REAL
(f,C) is complex set
(f,C1) is complex set
(f,C2) is complex set
(f,C1) + (f,C2) is complex set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
[.a,b.] is V57() V58() V59() Element of bool REAL
d is complex real ext-real Element of REAL
[.a,d.] is V57() V58() V59() Element of bool REAL
[.d,b.] is V57() V58() V59() Element of bool REAL
a0 is complex real ext-real Element of REAL
b0 is complex real ext-real Element of REAL
[.a0,b0.] is V57() V58() V59() Element of bool REAL
x is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom x is V57() V58() V59() Element of bool REAL
y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom y is V57() V58() V59() Element of bool REAL
Z is V57() V58() V59() Element of bool REAL
x `| Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y `| Z is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) y is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
x + (<i> (#) y) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(x + (<i> (#) y)) | [.a0,b0.] is Relation-like REAL -defined [.a0,b0.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
inf [.a0,b0.] is ext-real set
sup [.a0,b0.] is ext-real set
<:x,y:> is Relation-like Function-like set
Re f is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Re f) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:x,y:> (#) ((Re f) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
Im f is Relation-like COMPLEX -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:COMPLEX,REAL:]
(Im f) * () is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
<:x,y:> (#) ((Im f) * ()) is Relation-like REAL -valued complex-valued ext-real-valued real-valued set
(a,b,x,y,Z,f) is complex set
u0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
v0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 (#) (x `| Z) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
v0 (#) (y `| Z) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (v0 (#) (y `| Z)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (v0 (#) (y `| Z)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(u0 (#) (x `| Z)) + (- (v0 (#) (y `| Z))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b) is complex real ext-real Element of REAL
v0 (#) (x `| Z) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u0 (#) (y `| Z) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b) is complex real ext-real Element of REAL
(integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i> is complex set
(integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) is complex set
a1 is complex real ext-real Element of REAL
b1 is complex real ext-real Element of REAL
[.a1,b1.] is V57() V58() V59() Element of bool REAL
x1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom x1 is V57() V58() V59() Element of bool REAL
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom y1 is V57() V58() V59() Element of bool REAL
Z1 is V57() V58() V59() Element of bool REAL
x1 `| Z1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 `| Z1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) y1 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
x1 + (<i> (#) y1) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(x1 + (<i> (#) y1)) | [.a1,b1.] is Relation-like REAL -defined [.a1,b1.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
inf [.a1,b1.] is ext-real set
sup [.a1,b1.] is ext-real set
rng C1 is V57() Element of bool COMPLEX
a2 is set
b2 is set
C1 . b2 is complex set
C . b2 is complex set
a2 is complex real ext-real Element of REAL
b2 is complex real ext-real Element of REAL
[.a2,b2.] is V57() V58() V59() Element of bool REAL
x2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom x2 is V57() V58() V59() Element of bool REAL
y2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom y2 is V57() V58() V59() Element of bool REAL
Z2 is V57() V58() V59() Element of bool REAL
x2 `| Z2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y2 `| Z2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
<i> (#) y2 is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
x2 + (<i> (#) y2) is Relation-like REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
(x2 + (<i> (#) y2)) | [.a2,b2.] is Relation-like REAL -defined [.a2,b2.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
inf [.a2,b2.] is ext-real set
sup [.a2,b2.] is ext-real set
rng C2 is V57() Element of bool COMPLEX
Z3 is set
ZZ is set
C2 . ZZ is complex set
C . ZZ is complex set
(d,b,x2,y2,Z2,f) is complex set
['a,b'] is non empty V57() V58() V59() closed_interval interval Element of bool REAL
dom u0 is V57() V58() V59() Element of bool REAL
Z3 is set
C . Z3 is complex set
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
proj1 <:x,y:> is set
<:x,y:> . Z3 is set
x . Z3 is complex real ext-real Element of REAL
y . Z3 is complex real ext-real Element of REAL
[(x . Z3),(y . Z3)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
[(x . Z3),(y . Z3)] `1 is set
[(x . Z3),(y . Z3)] `2 is set
(x + (<i> (#) y)) . Z3 is complex set
(<i> (#) y) . Z3 is complex set
(x . Z3) + ((<i> (#) y) . Z3) is complex set
<i> * (y . Z3) is complex set
(x . Z3) + (<i> * (y . Z3)) is complex set
() . [(x . Z3),(y . Z3)] is complex set
() . (<:x,y:> . Z3) is complex set
dom (Re f) is V57() Element of bool COMPLEX
dom ((Re f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom v0 is V57() V58() V59() Element of bool REAL
Z3 is set
C . Z3 is complex set
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
proj1 <:x,y:> is set
<:x,y:> . Z3 is set
x . Z3 is complex real ext-real Element of REAL
y . Z3 is complex real ext-real Element of REAL
[(x . Z3),(y . Z3)] is V24() set
dom () is non empty Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
[(x . Z3),(y . Z3)] `1 is set
[(x . Z3),(y . Z3)] `2 is set
(x + (<i> (#) y)) . Z3 is complex set
(<i> (#) y) . Z3 is complex set
(x . Z3) + ((<i> (#) y) . Z3) is complex set
<i> * (y . Z3) is complex set
(x . Z3) + (<i> * (y . Z3)) is complex set
() . [(x . Z3),(y . Z3)] is complex set
() . (<:x,y:> . Z3) is complex set
dom (Im f) is V57() Element of bool COMPLEX
dom ((Im f) * ()) is Relation-like REAL -defined REAL -valued complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is Relation-like REAL -defined ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is Relation-like REAL -defined ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) is V57() V58() V59() Element of bool REAL
dom (u0 (#) (x `| Z)) is V57() V58() V59() Element of bool REAL
dom (v0 (#) (y `| Z)) is V57() V58() V59() Element of bool REAL
(dom (u0 (#) (x `| Z))) /\ (dom (v0 (#) (y `| Z))) is V57() V58() V59() Element of bool REAL
dom (x `| Z) is V57() V58() V59() Element of bool REAL
(dom u0) /\ (dom (x `| Z)) is V57() V58() V59() Element of bool REAL
((dom u0) /\ (dom (x `| Z))) /\ (dom (v0 (#) (y `| Z))) is V57() V58() V59() Element of bool REAL
dom (y `| Z) is V57() V58() V59() Element of bool REAL
(dom v0) /\ (dom (y `| Z)) is V57() V58() V59() Element of bool REAL
((dom u0) /\ (dom (x `| Z))) /\ ((dom v0) /\ (dom (y `| Z))) is V57() V58() V59() Element of bool REAL
(dom u0) /\ Z is V57() V58() V59() Element of bool REAL
((dom u0) /\ Z) /\ ((dom v0) /\ (dom (y `| Z))) is V57() V58() V59() Element of bool REAL
(dom v0) /\ Z is V57() V58() V59() Element of bool REAL
((dom u0) /\ Z) /\ ((dom v0) /\ Z) is V57() V58() V59() Element of bool REAL
Z /\ ((dom v0) /\ Z) is V57() V58() V59() Element of bool REAL
(dom u0) /\ (Z /\ ((dom v0) /\ Z)) is V57() V58() V59() Element of bool REAL
Z /\ Z is V57() V58() V59() Element of bool REAL
(Z /\ Z) /\ (dom v0) is V57() V58() V59() Element of bool REAL
(dom u0) /\ ((Z /\ Z) /\ (dom v0)) is V57() V58() V59() Element of bool REAL
(dom u0) /\ (dom v0) is V57() V58() V59() Element of bool REAL
((dom u0) /\ (dom v0)) /\ Z is V57() V58() V59() Element of bool REAL
dom ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) is V57() V58() V59() Element of bool REAL
dom (v0 (#) (x `| Z)) is V57() V58() V59() Element of bool REAL
dom (u0 (#) (y `| Z)) is V57() V58() V59() Element of bool REAL
(dom (v0 (#) (x `| Z))) /\ (dom (u0 (#) (y `| Z))) is V57() V58() V59() Element of bool REAL
dom (x `| Z) is V57() V58() V59() Element of bool REAL
(dom v0) /\ (dom (x `| Z)) is V57() V58() V59() Element of bool REAL
((dom v0) /\ (dom (x `| Z))) /\ (dom (u0 (#) (y `| Z))) is V57() V58() V59() Element of bool REAL
dom (y `| Z) is V57() V58() V59() Element of bool REAL
(dom u0) /\ (dom (y `| Z)) is V57() V58() V59() Element of bool REAL
((dom v0) /\ (dom (x `| Z))) /\ ((dom u0) /\ (dom (y `| Z))) is V57() V58() V59() Element of bool REAL
(dom v0) /\ Z is V57() V58() V59() Element of bool REAL
((dom v0) /\ Z) /\ ((dom u0) /\ (dom (y `| Z))) is V57() V58() V59() Element of bool REAL
(dom u0) /\ Z is V57() V58() V59() Element of bool REAL
((dom v0) /\ Z) /\ ((dom u0) /\ Z) is V57() V58() V59() Element of bool REAL
Z /\ ((dom u0) /\ Z) is V57() V58() V59() Element of bool REAL
(dom v0) /\ (Z /\ ((dom u0) /\ Z)) is V57() V58() V59() Element of bool REAL
Z /\ Z is V57() V58() V59() Element of bool REAL
(Z /\ Z) /\ (dom u0) is V57() V58() V59() Element of bool REAL
(dom v0) /\ ((Z /\ Z) /\ (dom u0)) is V57() V58() V59() Element of bool REAL
(dom v0) /\ (dom u0) is V57() V58() V59() Element of bool REAL
((dom v0) /\ (dom u0)) /\ Z is V57() V58() V59() Element of bool REAL
integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d) is complex real ext-real Element of REAL
integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d) is complex real ext-real Element of REAL
(integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) * <i> is complex set
(integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) * <i>) is complex set
(a,d,x,y,Z,f) is complex set
integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b) is complex real ext-real Element of REAL
integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b) is complex real ext-real Element of REAL
(integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b)) * <i> is complex set
(integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b)) * <i>) is complex set
(d,b,x,y,Z,f) is complex set
(a,d,x1,y1,Z1,f) is complex set
Z /\ Z1 is V57() V58() V59() Element of bool REAL
ZZ is Element of bool the U1 of R^1
ZZ1 is Element of bool the U1 of R^1
ZZ /\ ZZ1 is Element of bool the U1 of R^1
Z3 is V57() V58() V59() Element of bool REAL
x | [.a,d.] is Relation-like REAL -defined [.a,d.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x1 | [.a,d.] is Relation-like REAL -defined [.a,d.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (x | [.a,d.]) is V57() V58() V59() Element of bool REAL
(dom x) /\ [.a,d.] is V57() V58() V59() Element of bool REAL
(dom x1) /\ [.a,d.] is V57() V58() V59() Element of bool REAL
dom (x1 | [.a,d.]) is V57() V58() V59() Element of bool REAL
y0 is set
(x | [.a,d.]) . y0 is complex real ext-real Element of REAL
(x1 | [.a,d.]) . y0 is complex real ext-real Element of REAL
(dom x1) /\ (dom y1) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y1) is V57() V58() V59() Element of bool REAL
(dom x1) /\ (dom (<i> (#) y1)) is V57() V58() V59() Element of bool REAL
dom (x1 + (<i> (#) y1)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
x0 is complex real ext-real Element of REAL
C . x0 is complex set
C1 . x0 is complex set
(x + (<i> (#) y)) . x0 is complex set
(x1 + (<i> (#) y1)) . x0 is complex set
x1 . x0 is complex real ext-real Element of REAL
(<i> (#) y1) . x0 is complex set
(x1 . x0) + ((<i> (#) y1) . x0) is complex set
y1 . x0 is complex real ext-real Element of REAL
<i> * (y1 . x0) is complex set
(x1 . x0) + (<i> * (y1 . x0)) is complex set
x . x0 is complex real ext-real Element of REAL
(<i> (#) y) . x0 is complex set
(x . x0) + ((<i> (#) y) . x0) is complex set
y . x0 is complex real ext-real Element of REAL
<i> * (y . x0) is complex set
(x . x0) + (<i> * (y . x0)) is complex set
x . y0 is complex real ext-real Element of REAL
x1 . y0 is complex real ext-real Element of REAL
y | [.a,d.] is Relation-like REAL -defined [.a,d.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 | [.a,d.] is Relation-like REAL -defined [.a,d.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (y | [.a,d.]) is V57() V58() V59() Element of bool REAL
(dom y) /\ [.a,d.] is V57() V58() V59() Element of bool REAL
(dom y1) /\ [.a,d.] is V57() V58() V59() Element of bool REAL
dom (y1 | [.a,d.]) is V57() V58() V59() Element of bool REAL
y0 is set
(y | [.a,d.]) . y0 is complex real ext-real Element of REAL
(y1 | [.a,d.]) . y0 is complex real ext-real Element of REAL
(dom x1) /\ (dom y1) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y1) is V57() V58() V59() Element of bool REAL
(dom x1) /\ (dom (<i> (#) y1)) is V57() V58() V59() Element of bool REAL
dom (x1 + (<i> (#) y1)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
x0 is complex real ext-real Element of REAL
C . x0 is complex set
C1 . x0 is complex set
(x + (<i> (#) y)) . x0 is complex set
(x1 + (<i> (#) y1)) . x0 is complex set
x1 . x0 is complex real ext-real Element of REAL
(<i> (#) y1) . x0 is complex set
(x1 . x0) + ((<i> (#) y1) . x0) is complex set
y1 . x0 is complex real ext-real Element of REAL
<i> * (y1 . x0) is complex set
(x1 . x0) + (<i> * (y1 . x0)) is complex set
x . x0 is complex real ext-real Element of REAL
(<i> (#) y) . x0 is complex set
(x . x0) + ((<i> (#) y) . x0) is complex set
y . x0 is complex real ext-real Element of REAL
<i> * (y . x0) is complex set
(x . x0) + (<i> * (y . x0)) is complex set
y . y0 is complex real ext-real Element of REAL
y1 . y0 is complex real ext-real Element of REAL
(x + (<i> (#) y)) | [.a,d.] is Relation-like REAL -defined [.a,d.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
rng ((x + (<i> (#) y)) | [.a,d.]) is V57() Element of bool COMPLEX
y0 is set
dom ((x + (<i> (#) y)) | [.a,d.]) is V57() V58() V59() Element of bool REAL
x0 is set
((x + (<i> (#) y)) | [.a,d.]) . x0 is complex set
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
(dom (x + (<i> (#) y))) /\ [.a,d.] is V57() V58() V59() Element of bool REAL
(dom (x + (<i> (#) y))) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
(x + (<i> (#) y)) | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
dom ((x + (<i> (#) y)) | [.a,b.]) is V57() V58() V59() Element of bool REAL
((x + (<i> (#) y)) | [.a,b.]) . x0 is complex set
rng ((x + (<i> (#) y)) | [.a,b.]) is V57() Element of bool COMPLEX
(x + (<i> (#) y)) . x0 is complex set
(x1 + (<i> (#) y1)) | [.a,d.] is Relation-like REAL -defined [.a,d.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
rng ((x1 + (<i> (#) y1)) | [.a,d.]) is V57() Element of bool COMPLEX
y0 is set
dom ((x1 + (<i> (#) y1)) | [.a,d.]) is V57() V58() V59() Element of bool REAL
x0 is set
((x1 + (<i> (#) y1)) | [.a,d.]) . x0 is complex set
dom (x1 + (<i> (#) y1)) is V57() V58() V59() Element of bool REAL
(dom (x1 + (<i> (#) y1))) /\ [.a,d.] is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom y)) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (<i> (#) y))) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
(dom (x + (<i> (#) y))) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
(x + (<i> (#) y)) | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
dom ((x + (<i> (#) y)) | [.a,b.]) is V57() V58() V59() Element of bool REAL
((x + (<i> (#) y)) | [.a,b.]) . x0 is complex set
rng ((x + (<i> (#) y)) | [.a,b.]) is V57() Element of bool COMPLEX
t is complex real ext-real Element of REAL
C . t is complex set
(x + (<i> (#) y)) . t is complex set
C1 . t is complex set
(x1 + (<i> (#) y1)) . t is complex set
(x1 + (<i> (#) y1)) . x0 is complex set
(x + (<i> (#) y)) . x0 is complex set
(a,d,x,y,Z3,f) is complex set
(a,d,x1,y1,Z3,f) is complex set
Z /\ Z2 is V57() V58() V59() Element of bool REAL
ZZ is Element of bool the U1 of R^1
ZZ1 is Element of bool the U1 of R^1
ZZ /\ ZZ1 is Element of bool the U1 of R^1
Z3 is V57() V58() V59() Element of bool REAL
x | [.d,b.] is Relation-like REAL -defined [.d,b.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x2 | [.d,b.] is Relation-like REAL -defined [.d,b.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (x | [.d,b.]) is V57() V58() V59() Element of bool REAL
(dom x) /\ [.d,b.] is V57() V58() V59() Element of bool REAL
(dom x2) /\ [.d,b.] is V57() V58() V59() Element of bool REAL
dom (x2 | [.d,b.]) is V57() V58() V59() Element of bool REAL
y0 is set
(x | [.d,b.]) . y0 is complex real ext-real Element of REAL
(x2 | [.d,b.]) . y0 is complex real ext-real Element of REAL
(dom x2) /\ (dom y2) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y2) is V57() V58() V59() Element of bool REAL
(dom x2) /\ (dom (<i> (#) y2)) is V57() V58() V59() Element of bool REAL
dom (x2 + (<i> (#) y2)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
x0 is complex real ext-real Element of REAL
C . x0 is complex set
C2 . x0 is complex set
(x + (<i> (#) y)) . x0 is complex set
(x2 + (<i> (#) y2)) . x0 is complex set
x2 . x0 is complex real ext-real Element of REAL
(<i> (#) y2) . x0 is complex set
(x2 . x0) + ((<i> (#) y2) . x0) is complex set
y2 . x0 is complex real ext-real Element of REAL
<i> * (y2 . x0) is complex set
(x2 . x0) + (<i> * (y2 . x0)) is complex set
x . x0 is complex real ext-real Element of REAL
(<i> (#) y) . x0 is complex set
(x . x0) + ((<i> (#) y) . x0) is complex set
y . x0 is complex real ext-real Element of REAL
<i> * (y . x0) is complex set
(x . x0) + (<i> * (y . x0)) is complex set
x . y0 is complex real ext-real Element of REAL
x2 . y0 is complex real ext-real Element of REAL
y | [.d,b.] is Relation-like REAL -defined [.d,b.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y2 | [.d,b.] is Relation-like REAL -defined [.d,b.] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (y | [.d,b.]) is V57() V58() V59() Element of bool REAL
(dom y) /\ [.d,b.] is V57() V58() V59() Element of bool REAL
(dom y2) /\ [.d,b.] is V57() V58() V59() Element of bool REAL
dom (y2 | [.d,b.]) is V57() V58() V59() Element of bool REAL
y0 is set
(y | [.d,b.]) . y0 is complex real ext-real Element of REAL
(y2 | [.d,b.]) . y0 is complex real ext-real Element of REAL
(dom x2) /\ (dom y2) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y2) is V57() V58() V59() Element of bool REAL
(dom x2) /\ (dom (<i> (#) y2)) is V57() V58() V59() Element of bool REAL
dom (x2 + (<i> (#) y2)) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
x0 is complex real ext-real Element of REAL
C . x0 is complex set
C2 . x0 is complex set
(x + (<i> (#) y)) . x0 is complex set
(x2 + (<i> (#) y2)) . x0 is complex set
x2 . x0 is complex real ext-real Element of REAL
(<i> (#) y2) . x0 is complex set
(x2 . x0) + ((<i> (#) y2) . x0) is complex set
y2 . x0 is complex real ext-real Element of REAL
<i> * (y2 . x0) is complex set
(x2 . x0) + (<i> * (y2 . x0)) is complex set
x . x0 is complex real ext-real Element of REAL
(<i> (#) y) . x0 is complex set
(x . x0) + ((<i> (#) y) . x0) is complex set
y . x0 is complex real ext-real Element of REAL
<i> * (y . x0) is complex set
(x . x0) + (<i> * (y . x0)) is complex set
y . y0 is complex real ext-real Element of REAL
y2 . y0 is complex real ext-real Element of REAL
(x + (<i> (#) y)) | [.d,b.] is Relation-like REAL -defined [.d,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
rng ((x + (<i> (#) y)) | [.d,b.]) is V57() Element of bool COMPLEX
y0 is set
dom ((x + (<i> (#) y)) | [.d,b.]) is V57() V58() V59() Element of bool REAL
x0 is set
((x + (<i> (#) y)) | [.d,b.]) . x0 is complex set
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
(dom (x + (<i> (#) y))) /\ [.d,b.] is V57() V58() V59() Element of bool REAL
(dom (x + (<i> (#) y))) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
(x + (<i> (#) y)) | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
dom ((x + (<i> (#) y)) | [.a,b.]) is V57() V58() V59() Element of bool REAL
((x + (<i> (#) y)) | [.a,b.]) . x0 is complex set
rng ((x + (<i> (#) y)) | [.a,b.]) is V57() Element of bool COMPLEX
(x + (<i> (#) y)) . x0 is complex set
(x2 + (<i> (#) y2)) | [.d,b.] is Relation-like REAL -defined [.d,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
rng ((x2 + (<i> (#) y2)) | [.d,b.]) is V57() Element of bool COMPLEX
y0 is set
dom ((x2 + (<i> (#) y2)) | [.d,b.]) is V57() V58() V59() Element of bool REAL
x0 is set
((x2 + (<i> (#) y2)) | [.d,b.]) . x0 is complex set
dom (x2 + (<i> (#) y2)) is V57() V58() V59() Element of bool REAL
(dom (x2 + (<i> (#) y2))) /\ [.d,b.] is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom y) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom y)) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
dom (<i> (#) y) is V57() V58() V59() Element of bool REAL
(dom x) /\ (dom (<i> (#) y)) is V57() V58() V59() Element of bool REAL
((dom x) /\ (dom (<i> (#) y))) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
dom (x + (<i> (#) y)) is V57() V58() V59() Element of bool REAL
(dom (x + (<i> (#) y))) /\ [.a,b.] is V57() V58() V59() Element of bool REAL
(x + (<i> (#) y)) | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined COMPLEX -valued Function-like complex-valued Element of bool [:REAL,COMPLEX:]
dom ((x + (<i> (#) y)) | [.a,b.]) is V57() V58() V59() Element of bool REAL
((x + (<i> (#) y)) | [.a,b.]) . x0 is complex set
rng ((x + (<i> (#) y)) | [.a,b.]) is V57() Element of bool COMPLEX
t is complex real ext-real Element of REAL
C . t is complex set
(x + (<i> (#) y)) . t is complex set
C2 . t is complex set
(x2 + (<i> (#) y2)) . t is complex set
(x2 + (<i> (#) y2)) . x0 is complex set
(x + (<i> (#) y)) . x0 is complex set
(d,b,x,y,Z3,f) is complex set
(d,b,x2,y2,Z3,f) is complex set
(integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b)) is complex real ext-real Element of REAL
((integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b))) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) is complex set
(integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) + (integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b)) is complex real ext-real Element of REAL
((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) + (integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b))) * <i> is complex set
((integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b))) + (((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) + (integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b))) * <i>) is complex set
(a,d,x1,y1,Z1,f) + (d,b,x,y,Z,f) is complex set