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