:: INTEGR16 semantic presentation

REAL is non empty V32() V126() V127() V128() V132() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() Element of K6(REAL)
K6(REAL) is set
REAL * is non empty functional FinSequence-membered M10( REAL )
K7(NAT,(REAL *)) is set
K6(K7(NAT,(REAL *))) is set
ExtREAL is non empty V127() set
K7(NAT,ExtREAL) is V117() set
K6(K7(NAT,ExtREAL)) is set
K6(ExtREAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() set
K6(omega) is set
K6(NAT) is set
COMPLEX is non empty V32() V126() V132() set
RAT is non empty V32() V126() V127() V128() V129() V132() set
INT is non empty V32() V126() V127() V128() V129() V130() V132() set
K7(REAL,REAL) is V116() V117() V118() set
K6(K7(REAL,REAL)) is set
K291() is V44() V72() L8()
the U1 of K291() is set
K296() is V44() L8()
K297() is V44() V72() M13(K296())
K298() is V44() V72() V94() V154() M16(K296(),K297())
K300() is V44() V72() V94() V96() V98() L8()
K301() is V44() V72() V94() V154() M13(K300())
K7(COMPLEX,COMPLEX) is V116() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V116() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(K7(REAL,REAL),REAL) is V116() V117() V118() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is RAT -valued V116() V117() V118() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued V116() V117() V118() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued V116() V117() V118() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued V116() V117() V118() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued V116() V117() V118() V119() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued V116() V117() V118() V119() set
K6(K7(K7(NAT,NAT),NAT)) is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive V126() V127() V128() V129() V130() V131() Element of NAT
K7(1,1) is RAT -valued INT -valued V116() V117() V118() V119() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued V116() V117() V118() V119() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V116() V117() V118() set
K6(K7(K7(1,1),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive V126() V127() V128() V129() V130() V131() Element of NAT
K7(2,2) is RAT -valued INT -valued V116() V117() V118() V119() set
K7(K7(2,2),REAL) is V116() V117() V118() set
K6(K7(K7(2,2),REAL)) is set
K487(2) is V210() L16()
the U1 of K487(2) is set
K7(NAT,REAL) is V116() V117() V118() set
K6(K7(NAT,REAL)) is set
K563(NAT) is V237() set
K7(NAT,COMPLEX) is V116() set
K6(K7(NAT,COMPLEX)) is set
K6(K6(REAL)) is set
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive V126() V127() V128() V129() V130() V131() Element of NAT
<i> is complex Element of COMPLEX
K7(2,REAL) is V116() V117() V118() set
K6(K7(2,REAL)) is set
0 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real V126() V127() V128() V129() V130() V131() V132() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real V126() V127() V128() V129() V130() V131() V132() set
Re 0 is complex real ext-real Element of REAL
Im 0 is complex real ext-real Element of REAL
addcomplex is Relation-like K7(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like total quasi_total V116() V182( COMPLEX ) V183( COMPLEX ) V238( COMPLEX ) Element of K6(K7(K7(COMPLEX,COMPLEX),COMPLEX))
K435(COMPLEX,addcomplex) is complex Element of COMPLEX
{} is set
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like NAT -defined REAL -valued Function-like functional V32() FinSequence-like FinSubsequence-like FinSequence-membered ext-real V116() V117() V118() V119() V126() V127() V128() V129() V130() V131() V132() FinSequence of REAL
Sum (<*> REAL) is complex real ext-real Element of REAL
addreal is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total V116() V117() V118() V182( REAL ) V183( REAL ) V238( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
addreal $$ (<*> REAL) is complex real ext-real Element of REAL
f is complex set
Re f is complex real ext-real Element of REAL
Im f is complex real ext-real Element of REAL
A is complex real ext-real set
A * f is complex Element of COMPLEX
Re (A * f) is complex real ext-real Element of REAL
A * (Re f) is complex real ext-real Element of REAL
Im (A * f) is complex real ext-real Element of REAL
A * (Im f) is complex real ext-real Element of REAL
Re A is complex real ext-real Element of REAL
Im A is complex real ext-real Element of REAL
(Im A) * (Im f) is complex real ext-real Element of REAL
(A * (Re f)) - ((Im A) * (Im f)) is complex real ext-real Element of REAL
0 * (Im f) is complex real ext-real Element of REAL
(A * (Re f)) - (0 * (Im f)) is complex real ext-real Element of REAL
(Re f) * (Im A) is complex real ext-real Element of REAL
(A * (Im f)) + ((Re f) * (Im A)) is complex real ext-real Element of REAL
0 * (Re f) is complex real ext-real Element of REAL
(A * (Im f)) + (0 * (Re f)) is complex real ext-real Element of REAL
f is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
dom f is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
A is Relation-like Function-like set
dom A is set
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
Seg a is V32() V39(a) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= a ) } is set
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Re f is Relation-like NAT -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(NAT,REAL))
dom (Re f) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom f is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
Im f is Relation-like NAT -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(NAT,REAL))
dom (Im f) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom f is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Re f is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
Re f is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() Element of K6(K7(NAT,REAL))
rng (Re f) is V126() V127() V128() Element of K6(REAL)
Im f is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
Im f is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() Element of K6(K7(NAT,REAL))
rng (Im f) is V126() V127() V128() Element of K6(REAL)
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
a is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
len a is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom a is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
Seg (len a) is V32() V39( len a) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len a ) } is set
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
divset (a,b) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset (a,b)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
rng (A | (divset (a,b))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
vol (divset (a,b)) is complex real ext-real Element of REAL
dom A is V126() V127() V128() Element of K6(f)
K6(f) is set
dom (A | (divset (a,b))) is V126() V127() V128() Element of K6(f)
g0 is set
G is complex Element of COMPLEX
G * (vol (divset (a,b))) is complex Element of COMPLEX
b is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
dom b is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len b is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
a is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
b is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a)
Sum b is complex Element of COMPLEX
addcomplex $$ b is complex Element of COMPLEX
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
divs f is non empty set
K7(NAT,(divs f)) is set
K6(K7(NAT,(divs f))) is set
COMPLEX * is non empty functional FinSequence-membered M10( COMPLEX )
K7(NAT,(COMPLEX *)) is set
K6(K7(NAT,(COMPLEX *))) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
a is non empty Relation-like NAT -defined divs f -valued Function-like total quasi_total Element of K6(K7(NAT,(divs f)))
b is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
a . b is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
the Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . b) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . b)
G is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() Element of COMPLEX *
b is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total Element of K6(K7(NAT,(COMPLEX *)))
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
divs f is non empty set
K7(NAT,(divs f)) is set
K6(K7(NAT,(divs f))) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
a is non empty Relation-like NAT -defined divs f -valued Function-like total quasi_total Element of K6(K7(NAT,(divs f)))
b is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total (f,A,a)
g0 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
b . g0 is FinSequence-like set
a . g0 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
divs f is non empty set
K7(NAT,(divs f)) is set
K6(K7(NAT,(divs f))) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
a is non empty Relation-like NAT -defined divs f -valued Function-like total quasi_total Element of K6(K7(NAT,(divs f)))
b is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total (f,A,a)
g0 is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
G is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
T is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
g0 . T is complex Element of COMPLEX
G . T is complex Element of COMPLEX
a . T is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
(f,A,a,b,T) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . T)
(f,A,(a . T),(f,A,a,b,T)) is complex Element of COMPLEX
Sum (f,A,a,b,T) is complex Element of COMPLEX
addcomplex $$ (f,A,a,b,T) is complex Element of COMPLEX
K7(REAL,COMPLEX) is V116() set
K6(K7(REAL,COMPLEX)) is set
f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
A is V126() V127() V128() Element of K6(REAL)
f | A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re (f | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re f) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
a is set
dom ((Re f) | A) is V126() V127() V128() Element of K6(REAL)
dom (Re f) is V126() V127() V128() Element of K6(REAL)
(dom (Re f)) /\ A is V126() V127() V128() Element of K6(REAL)
dom f is V126() V127() V128() Element of K6(REAL)
(dom f) /\ A is V126() V127() V128() Element of K6(REAL)
dom (f | A) is V126() V127() V128() Element of K6(REAL)
dom (Re (f | A)) is V126() V127() V128() Element of K6(REAL)
(Re (f | A)) . a is complex real ext-real Element of REAL
(f | A) . a is complex set
Re ((f | A) . a) is complex real ext-real Element of REAL
f . a is complex set
Re (f . a) is complex real ext-real Element of REAL
(Re f) . a is complex real ext-real Element of REAL
((Re f) | A) . a is complex real ext-real Element of REAL
f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Im f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
A is V126() V127() V128() Element of K6(REAL)
f | A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Im (f | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im f) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
a is set
dom ((Im f) | A) is V126() V127() V128() Element of K6(REAL)
dom (Im f) is V126() V127() V128() Element of K6(REAL)
(dom (Im f)) /\ A is V126() V127() V128() Element of K6(REAL)
dom f is V126() V127() V128() Element of K6(REAL)
(dom f) /\ A is V126() V127() V128() Element of K6(REAL)
dom (f | A) is V126() V127() V128() Element of K6(REAL)
dom (Im (f | A)) is V126() V127() V128() Element of K6(REAL)
(Im (f | A)) . a is complex real ext-real Element of REAL
(f | A) . a is complex set
Im ((f | A) . a) is complex real ext-real Element of REAL
f . a is complex set
Im (f . a) is complex real ext-real Element of REAL
(Im f) . a is complex real ext-real Element of REAL
((Im f) | A) . a is complex real ext-real Element of REAL
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
Re A is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
dom A is V126() V127() V128() Element of K6(f)
K6(f) is set
dom (Re A) is V126() V127() V128() Element of K6(f)
a is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
Im A is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
dom A is V126() V127() V128() Element of K6(f)
K6(f) is set
dom (Im A) is V126() V127() V128() Element of K6(f)
a is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
Re A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
Im A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
a is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
b is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a)
(b) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
(b) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom b is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom (b) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len b is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
len a is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len a) is V32() V39( len a) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len a ) } is set
len (b) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom a is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
divset (a,G) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
(Re A) | (divset (a,G)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
rng ((Re A) | (divset (a,G))) is V126() V127() V128() Element of K6(REAL)
(b) . G is complex real ext-real Element of REAL
vol (divset (a,G)) is complex real ext-real Element of REAL
A | (divset (a,G)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
rng (A | (divset (a,G))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
b . G is complex set
T is complex Element of COMPLEX
T * (vol (divset (a,G))) is complex Element of COMPLEX
Re T is complex real ext-real Element of REAL
(Re T) * (vol (divset (a,G))) is complex real ext-real Element of REAL
dom (A | (divset (a,G))) is V126() V127() V128() Element of K6(f)
K6(f) is set
xs is set
(A | (divset (a,G))) . xs is complex set
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset (a,G)) is V126() V127() V128() Element of K6(REAL)
dom (Re A) is V126() V127() V128() Element of K6(f)
(dom (Re A)) /\ (divset (a,G)) is V126() V127() V128() Element of K6(REAL)
dom ((Re A) | (divset (a,G))) is V126() V127() V128() Element of K6(f)
A . xs is complex set
Re (A . xs) is complex real ext-real Element of REAL
(Re A) . xs is complex real ext-real Element of REAL
((Re A) | (divset (a,G))) . xs is complex real ext-real Element of REAL
Re (b . G) is complex real ext-real Element of REAL
dom (b) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len (b) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
divset (a,T) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
(Im A) | (divset (a,T)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
rng ((Im A) | (divset (a,T))) is V126() V127() V128() Element of K6(REAL)
(b) . T is complex real ext-real Element of REAL
vol (divset (a,T)) is complex real ext-real Element of REAL
A | (divset (a,T)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
rng (A | (divset (a,T))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
b . T is complex set
Si is complex Element of COMPLEX
Si * (vol (divset (a,T))) is complex Element of COMPLEX
Im Si is complex real ext-real Element of REAL
(Im Si) * (vol (divset (a,T))) is complex real ext-real Element of REAL
dom (A | (divset (a,T))) is V126() V127() V128() Element of K6(f)
K6(f) is set
S is set
(A | (divset (a,T))) . S is complex set
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset (a,T)) is V126() V127() V128() Element of K6(REAL)
dom (Im A) is V126() V127() V128() Element of K6(f)
(dom (Im A)) /\ (divset (a,T)) is V126() V127() V128() Element of K6(REAL)
dom ((Im A) | (divset (a,T))) is V126() V127() V128() Element of K6(f)
A . S is complex set
Im (A . S) is complex real ext-real Element of REAL
(Im A) . S is complex real ext-real Element of REAL
((Im A) | (divset (a,T))) . S is complex real ext-real Element of REAL
Im (b . T) is complex real ext-real Element of REAL
<*> COMPLEX is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like NAT -defined COMPLEX -valued Function-like functional V32() FinSequence-like FinSubsequence-like FinSequence-membered ext-real V116() V117() V118() V119() V126() V127() V128() V129() V130() V131() V132() FinSequence of COMPLEX
Sum (<*> COMPLEX) is complex Element of COMPLEX
addcomplex $$ (<*> COMPLEX) is complex Element of COMPLEX
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Sum f is complex Element of COMPLEX
addcomplex $$ f is complex Element of COMPLEX
A is complex Element of COMPLEX
<*A*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
[1,A] is set
{[1,A]} is set
f ^ <*A*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Sum (f ^ <*A*>) is complex Element of COMPLEX
addcomplex $$ (f ^ <*A*>) is complex Element of COMPLEX
(Sum f) + A is complex Element of COMPLEX
addcomplex . ((addcomplex $$ f),A) is complex Element of COMPLEX
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
(f) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
A is complex Element of COMPLEX
<*A*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
[1,A] is set
{[1,A]} is set
f ^ <*A*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
((f ^ <*A*>)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Re A is complex real ext-real Element of REAL
<*(Re A)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
[1,(Re A)] is set
{[1,(Re A)]} is set
(f) ^ <*(Re A)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom f is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom (f) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len f) is V32() V39( len f) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
len <*(Re A)*> is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom ((f ^ <*A*>)) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom (f ^ <*A*>) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len <*A*> is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(len f) + (len <*A*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg ((len f) + (len <*A*>)) is V32() V39((len f) + (len <*A*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= (len f) + (len <*A*>) ) } is set
len (f) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(len (f)) + (len <*A*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg ((len (f)) + (len <*A*>)) is V32() V39((len (f)) + (len <*A*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= (len (f)) + (len <*A*>) ) } is set
(len (f)) + (len <*(Re A)*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg ((len (f)) + (len <*(Re A)*>)) is V32() V39((len (f)) + (len <*(Re A)*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= (len (f)) + (len <*(Re A)*>) ) } is set
dom ((f) ^ <*(Re A)*>) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
g0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
len (f ^ <*A*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (f ^ <*A*>)) is V32() V39( len (f ^ <*A*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (f ^ <*A*>) ) } is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
(f ^ <*A*>) . g0 is complex set
Re ((f ^ <*A*>) . g0) is complex real ext-real Element of REAL
(len (f)) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f) ^ <*(Re A)*>) . ((len (f)) + 1) is complex real ext-real Element of REAL
((f) ^ <*(Re A)*>) . g0 is complex real ext-real Element of REAL
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
(f ^ <*A*>) . g0 is complex set
Re ((f ^ <*A*>) . g0) is complex real ext-real Element of REAL
f . g0 is complex set
Re (f . g0) is complex real ext-real Element of REAL
(f) . g0 is complex real ext-real Element of REAL
((f) ^ <*(Re A)*>) . g0 is complex real ext-real Element of REAL
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
((f) ^ <*(Re A)*>) . g0 is complex real ext-real Element of REAL
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
((f) ^ <*(Re A)*>) . g0 is complex real ext-real Element of REAL
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
(f) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
A is complex Element of COMPLEX
<*A*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
[1,A] is set
{[1,A]} is set
f ^ <*A*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
((f ^ <*A*>)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Im A is complex real ext-real Element of REAL
<*(Im A)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
[1,(Im A)] is set
{[1,(Im A)]} is set
(f) ^ <*(Im A)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom f is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom (f) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len f) is V32() V39( len f) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
len <*(Im A)*> is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom ((f ^ <*A*>)) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom (f ^ <*A*>) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len <*A*> is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(len f) + (len <*A*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg ((len f) + (len <*A*>)) is V32() V39((len f) + (len <*A*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= (len f) + (len <*A*>) ) } is set
len (f) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(len (f)) + (len <*A*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg ((len (f)) + (len <*A*>)) is V32() V39((len (f)) + (len <*A*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= (len (f)) + (len <*A*>) ) } is set
(len (f)) + (len <*(Im A)*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg ((len (f)) + (len <*(Im A)*>)) is V32() V39((len (f)) + (len <*(Im A)*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= (len (f)) + (len <*(Im A)*>) ) } is set
dom ((f) ^ <*(Im A)*>) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
g0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
len (f ^ <*A*>) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (f ^ <*A*>)) is V32() V39( len (f ^ <*A*>)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (f ^ <*A*>) ) } is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
(f ^ <*A*>) . g0 is complex set
Im ((f ^ <*A*>) . g0) is complex real ext-real Element of REAL
(len (f)) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f) ^ <*(Im A)*>) . ((len (f)) + 1) is complex real ext-real Element of REAL
((f) ^ <*(Im A)*>) . g0 is complex real ext-real Element of REAL
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
(f ^ <*A*>) . g0 is complex set
Im ((f ^ <*A*>) . g0) is complex real ext-real Element of REAL
f . g0 is complex set
Im (f . g0) is complex real ext-real Element of REAL
(f) . g0 is complex real ext-real Element of REAL
((f) ^ <*(Im A)*>) . g0 is complex real ext-real Element of REAL
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
((f) ^ <*(Im A)*>) . g0 is complex real ext-real Element of REAL
((f ^ <*A*>)) . g0 is complex real ext-real Element of REAL
((f) ^ <*(Im A)*>) . g0 is complex real ext-real Element of REAL
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(f) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum f is complex Element of COMPLEX
addcomplex $$ f is complex Element of COMPLEX
Re (Sum f) is complex real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum A is complex real ext-real Element of REAL
addreal $$ A is complex real ext-real Element of REAL
dom A is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom f is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
Seg (len f) is V32() V39( len f) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
len A is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
A is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len A is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
a is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
(A) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
A | f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Seg f is V32() V39(f) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= f ) } is set
A | (Seg f) is Relation-like FinSubsequence-like V116() set
b is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len b is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(b) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
A . (f + 1) is complex set
G is complex Element of COMPLEX
<*G*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
[1,G] is set
{[1,G]} is set
b ^ <*G*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Sum A is complex Element of COMPLEX
addcomplex $$ A is complex Element of COMPLEX
Re (Sum A) is complex real ext-real Element of REAL
Sum b is complex Element of COMPLEX
addcomplex $$ b is complex Element of COMPLEX
(Sum b) + G is complex Element of COMPLEX
Re ((Sum b) + G) is complex real ext-real Element of REAL
Re (Sum b) is complex real ext-real Element of REAL
Re G is complex real ext-real Element of REAL
(Re (Sum b)) + (Re G) is complex real ext-real Element of REAL
g0 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum g0 is complex real ext-real Element of REAL
addreal $$ g0 is complex real ext-real Element of REAL
(Sum g0) + (Re G) is complex real ext-real Element of REAL
<*(Re G)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
[1,(Re G)] is set
{[1,(Re G)]} is set
g0 ^ <*(Re G)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum (g0 ^ <*(Re G)*>) is complex real ext-real Element of REAL
addreal $$ (g0 ^ <*(Re G)*>) is complex real ext-real Element of REAL
Sum a is complex real ext-real Element of REAL
addreal $$ a is complex real ext-real Element of REAL
A is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len A is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
a is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
(A) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum a is complex real ext-real Element of REAL
addreal $$ a is complex real ext-real Element of REAL
Sum A is complex Element of COMPLEX
addcomplex $$ A is complex Element of COMPLEX
Re (Sum A) is complex real ext-real Element of REAL
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
(f) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum f is complex Element of COMPLEX
addcomplex $$ f is complex Element of COMPLEX
Re (Sum f) is complex real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum A is complex real ext-real Element of REAL
addreal $$ A is complex real ext-real Element of REAL
len f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(f) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum f is complex Element of COMPLEX
addcomplex $$ f is complex Element of COMPLEX
Im (Sum f) is complex real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum A is complex real ext-real Element of REAL
addreal $$ A is complex real ext-real Element of REAL
dom A is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom f is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
Seg (len f) is V32() V39( len f) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
len A is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
A is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len A is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
a is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
(A) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
A | f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Seg f is V32() V39(f) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= f ) } is set
A | (Seg f) is Relation-like FinSubsequence-like V116() set
b is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len b is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(b) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
A . (f + 1) is complex set
G is complex Element of COMPLEX
<*G*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
[1,G] is set
{[1,G]} is set
b ^ <*G*> is non empty Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
Sum A is complex Element of COMPLEX
addcomplex $$ A is complex Element of COMPLEX
Im (Sum A) is complex real ext-real Element of REAL
Sum b is complex Element of COMPLEX
addcomplex $$ b is complex Element of COMPLEX
(Sum b) + G is complex Element of COMPLEX
Im ((Sum b) + G) is complex real ext-real Element of REAL
Im (Sum b) is complex real ext-real Element of REAL
Im G is complex real ext-real Element of REAL
(Im (Sum b)) + (Im G) is complex real ext-real Element of REAL
g0 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum g0 is complex real ext-real Element of REAL
addreal $$ g0 is complex real ext-real Element of REAL
(Sum g0) + (Im G) is complex real ext-real Element of REAL
<*(Im G)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() V39(1) FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
[1,(Im G)] is set
{[1,(Im G)]} is set
g0 ^ <*(Im G)*> is non empty Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum (g0 ^ <*(Im G)*>) is complex real ext-real Element of REAL
addreal $$ (g0 ^ <*(Im G)*>) is complex real ext-real Element of REAL
Sum a is complex real ext-real Element of REAL
addreal $$ a is complex real ext-real Element of REAL
A is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
len A is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
a is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
(A) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum a is complex real ext-real Element of REAL
addreal $$ a is complex real ext-real Element of REAL
Sum A is complex Element of COMPLEX
addcomplex $$ A is complex Element of COMPLEX
Im (Sum A) is complex real ext-real Element of REAL
f is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
(f) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum f is complex Element of COMPLEX
addcomplex $$ f is complex Element of COMPLEX
Im (Sum f) is complex real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
Sum A is complex real ext-real Element of REAL
addreal $$ A is complex real ext-real Element of REAL
len f is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
a is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
Re A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
g0 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Re A,a
b is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a)
(b) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
(f,A,a,b) is complex Element of COMPLEX
Sum b is complex Element of COMPLEX
addcomplex $$ b is complex Element of COMPLEX
Re (f,A,a,b) is complex real ext-real Element of REAL
middle_sum ((Re A),g0) is complex real ext-real Element of REAL
Sum g0 is complex real ext-real Element of REAL
addreal $$ g0 is complex real ext-real Element of REAL
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
a is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
Im A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
g0 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Im A,a
b is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a)
(b) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
(f,A,a,b) is complex Element of COMPLEX
Sum b is complex Element of COMPLEX
addcomplex $$ b is complex Element of COMPLEX
Im (f,A,a,b) is complex real ext-real Element of REAL
middle_sum ((Im A),g0) is complex real ext-real Element of REAL
Sum g0 is complex real ext-real Element of REAL
addreal $$ g0 is complex real ext-real Element of REAL
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom f is V126() V127() V128() Element of K6(REAL)
A is complex real ext-real set
a is set
dom (Re f) is V126() V127() V128() Element of K6(REAL)
f . a is complex set
Re (f . a) is complex real ext-real Element of REAL
abs (Re (f . a)) is complex real ext-real Element of REAL
Re (Re (f . a)) is complex real ext-real Element of REAL
K707((Re (Re (f . a)))) is complex real ext-real Element of REAL
Im (Re (f . a)) is complex real ext-real Element of REAL
K707((Im (Re (f . a)))) is complex real ext-real Element of REAL
K707((Re (Re (f . a)))) + K707((Im (Re (f . a)))) is complex real ext-real Element of REAL
K709((K707((Re (Re (f . a)))) + K707((Im (Re (f . a)))))) is complex real ext-real Element of REAL
abs (f . a) is complex real ext-real Element of REAL
K707((Re (f . a))) is complex real ext-real Element of REAL
Im (f . a) is complex real ext-real Element of REAL
K707((Im (f . a))) is complex real ext-real Element of REAL
K707((Re (f . a))) + K707((Im (f . a))) is complex real ext-real Element of REAL
K709((K707((Re (f . a))) + K707((Im (f . a))))) is complex real ext-real Element of REAL
(Re f) . a is complex real ext-real Element of REAL
abs ((Re f) . a) is complex real ext-real Element of REAL
Re ((Re f) . a) is complex real ext-real Element of REAL
K707((Re ((Re f) . a))) is complex real ext-real Element of REAL
Im ((Re f) . a) is complex real ext-real Element of REAL
K707((Im ((Re f) . a))) is complex real ext-real Element of REAL
K707((Re ((Re f) . a))) + K707((Im ((Re f) . a))) is complex real ext-real Element of REAL
K709((K707((Re ((Re f) . a))) + K707((Im ((Re f) . a))))) is complex real ext-real Element of REAL
a is set
dom (Im f) is V126() V127() V128() Element of K6(REAL)
f . a is complex set
Im (f . a) is complex real ext-real Element of REAL
abs (Im (f . a)) is complex real ext-real Element of REAL
Re (Im (f . a)) is complex real ext-real Element of REAL
K707((Re (Im (f . a)))) is complex real ext-real Element of REAL
Im (Im (f . a)) is complex real ext-real Element of REAL
K707((Im (Im (f . a)))) is complex real ext-real Element of REAL
K707((Re (Im (f . a)))) + K707((Im (Im (f . a)))) is complex real ext-real Element of REAL
K709((K707((Re (Im (f . a)))) + K707((Im (Im (f . a)))))) is complex real ext-real Element of REAL
abs (f . a) is complex real ext-real Element of REAL
Re (f . a) is complex real ext-real Element of REAL
K707((Re (f . a))) is complex real ext-real Element of REAL
K707((Im (f . a))) is complex real ext-real Element of REAL
K707((Re (f . a))) + K707((Im (f . a))) is complex real ext-real Element of REAL
K709((K707((Re (f . a))) + K707((Im (f . a))))) is complex real ext-real Element of REAL
(Im f) . a is complex real ext-real Element of REAL
abs ((Im f) . a) is complex real ext-real Element of REAL
Re ((Im f) . a) is complex real ext-real Element of REAL
K707((Re ((Im f) . a))) is complex real ext-real Element of REAL
Im ((Im f) . a) is complex real ext-real Element of REAL
K707((Im ((Im f) . a))) is complex real ext-real Element of REAL
K707((Re ((Im f) . a))) + K707((Im ((Im f) . a))) is complex real ext-real Element of REAL
K709((K707((Re ((Im f) . a))) + K707((Im ((Im f) . a))))) is complex real ext-real Element of REAL
dom (Re f) is V126() V127() V128() Element of K6(REAL)
A is complex real ext-real set
dom (Im f) is V126() V127() V128() Element of K6(REAL)
a is complex real ext-real set
b is set
dom f is V126() V127() V128() Element of K6(REAL)
(Re f) . b is complex real ext-real Element of REAL
abs ((Re f) . b) is complex real ext-real Element of REAL
Re ((Re f) . b) is complex real ext-real Element of REAL
K707((Re ((Re f) . b))) is complex real ext-real Element of REAL
Im ((Re f) . b) is complex real ext-real Element of REAL
K707((Im ((Re f) . b))) is complex real ext-real Element of REAL
K707((Re ((Re f) . b))) + K707((Im ((Re f) . b))) is complex real ext-real Element of REAL
K709((K707((Re ((Re f) . b))) + K707((Im ((Re f) . b))))) is complex real ext-real Element of REAL
f . b is complex set
Re (f . b) is complex real ext-real Element of REAL
abs (Re (f . b)) is complex real ext-real Element of REAL
Re (Re (f . b)) is complex real ext-real Element of REAL
K707((Re (Re (f . b)))) is complex real ext-real Element of REAL
Im (Re (f . b)) is complex real ext-real Element of REAL
K707((Im (Re (f . b)))) is complex real ext-real Element of REAL
K707((Re (Re (f . b)))) + K707((Im (Re (f . b)))) is complex real ext-real Element of REAL
K709((K707((Re (Re (f . b)))) + K707((Im (Re (f . b)))))) is complex real ext-real Element of REAL
(Im f) . b is complex real ext-real Element of REAL
abs ((Im f) . b) is complex real ext-real Element of REAL
Re ((Im f) . b) is complex real ext-real Element of REAL
K707((Re ((Im f) . b))) is complex real ext-real Element of REAL
Im ((Im f) . b) is complex real ext-real Element of REAL
K707((Im ((Im f) . b))) is complex real ext-real Element of REAL
K707((Re ((Im f) . b))) + K707((Im ((Im f) . b))) is complex real ext-real Element of REAL
K709((K707((Re ((Im f) . b))) + K707((Im ((Im f) . b))))) is complex real ext-real Element of REAL
Im (f . b) is complex real ext-real Element of REAL
abs (Im (f . b)) is complex real ext-real Element of REAL
Re (Im (f . b)) is complex real ext-real Element of REAL
K707((Re (Im (f . b)))) is complex real ext-real Element of REAL
Im (Im (f . b)) is complex real ext-real Element of REAL
K707((Im (Im (f . b)))) is complex real ext-real Element of REAL
K707((Re (Im (f . b)))) + K707((Im (Im (f . b)))) is complex real ext-real Element of REAL
K709((K707((Re (Im (f . b)))) + K707((Im (Im (f . b)))))) is complex real ext-real Element of REAL
abs (f . b) is complex real ext-real Element of REAL
K707((Re (f . b))) is complex real ext-real Element of REAL
K707((Im (f . b))) is complex real ext-real Element of REAL
K707((Re (f . b))) + K707((Im (f . b))) is complex real ext-real Element of REAL
K709((K707((Re (f . b))) + K707((Im (f . b))))) is complex real ext-real Element of REAL
(abs (Re (f . b))) + (abs (Im (f . b))) is complex real ext-real Element of REAL
A + a is complex real ext-real Element of REAL
f is non empty V126() V127() V128() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
a is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
Re A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Re a is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
Im A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im a is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
Re A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
Im A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
dom A is V126() V127() V128() Element of K6(f)
K6(f) is set
a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
Re A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
integral (Re A) is complex real ext-real Element of REAL
Im A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
integral (Im A) is complex real ext-real Element of REAL
(integral (Im A)) * <i> is complex Element of COMPLEX
(integral (Re A)) + ((integral (Im A)) * <i>) is complex Element of COMPLEX
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
divs f is non empty set
K7(NAT,(divs f)) is set
K6(K7(NAT,(divs f))) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
(f,A) is complex Element of COMPLEX
Re A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
integral (Re A) is complex real ext-real Element of REAL
Im A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
integral (Im A) is complex real ext-real Element of REAL
(integral (Im A)) * <i> is complex Element of COMPLEX
(integral (Re A)) + ((integral (Im A)) * <i>) is complex Element of COMPLEX
a is non empty Relation-like NAT -defined divs f -valued Function-like total quasi_total Element of K6(K7(NAT,(divs f)))
delta a is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim (delta a) is complex real ext-real Element of REAL
b is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total (f,A,a)
(f,A,a,b) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
lim (f,A,a,b) is complex Element of COMPLEX
T is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
Re (f,A) is complex real ext-real Element of REAL
xs is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(f,A,a,b,xs) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . xs)
a . xs is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
((f,A,a,b,xs)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
xs is non empty Relation-like NAT -defined REAL * -valued Function-like total quasi_total Element of K6(K7(NAT,(REAL *)))
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(f,A,a,b,S) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . S)
a . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
((f,A,a,b,S)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom ((f,A,a,b,S)) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len (f,A,a,b,S) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (f,A,a,b,S)) is V32() V39( len (f,A,a,b,S)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (f,A,a,b,S) ) } is set
dom (f,A,a,b,S) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
Si is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
xs . S is FinSequence-like Element of REAL *
a . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
(f,A,a,b,S) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . S)
((f,A,a,b,S)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
seq is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom seq is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len (f,A,a,b,S) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (f,A,a,b,S)) is V32() V39( len (f,A,a,b,S)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (f,A,a,b,S) ) } is set
len (a . S) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (a . S)) is V32() V39( len (a . S)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (a . S) ) } is set
dom (a . S) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
xseq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
divset ((a . S),xseq) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((a . S),xseq)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
rng (A | (divset ((a . S),xseq))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
(f,A,a,b,S) . xseq is complex set
vol (divset ((a . S),xseq)) is complex real ext-real Element of REAL
rseqi is complex Element of COMPLEX
rseqi * (vol (divset ((a . S),xseq))) is complex Element of COMPLEX
Re rseqi is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
dom (A | (divset ((a . S),xseq))) is V126() V127() V128() Element of K6(f)
K6(f) is set
z is set
(A | (divset ((a . S),xseq))) . z is complex set
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset ((a . S),xseq)) is V126() V127() V128() Element of K6(REAL)
dom (Re A) is V126() V127() V128() Element of K6(f)
dom Si is V126() V127() V128() Element of K6(f)
(dom Si) /\ (divset ((a . S),xseq)) is V126() V127() V128() Element of K6(REAL)
Si | (divset ((a . S),xseq)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
dom (Si | (divset ((a . S),xseq))) is V126() V127() V128() Element of K6(f)
A . z is complex set
Re (A . z) is complex real ext-real Element of REAL
(Re A) . z is complex real ext-real Element of REAL
(Si | (divset ((a . S),xseq))) . z is complex real ext-real Element of REAL
H is complex real ext-real Element of REAL
rng (Si | (divset ((a . S),xseq))) is V126() V127() V128() Element of K6(REAL)
seq . xseq is complex real ext-real Element of REAL
Re ((f,A,a,b,S) . xseq) is complex real ext-real Element of REAL
H * (vol (divset ((a . S),xseq))) is complex real ext-real Element of REAL
len seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S is non empty Relation-like NAT -defined REAL * -valued Function-like total quasi_total middle_volume_Sequence of Si,a
middle_sum (Si,S) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
S is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S . seq is complex real ext-real Element of REAL
T . seq is complex Element of COMPLEX
Re (T . seq) is complex real ext-real Element of REAL
(f,A,a,b,seq) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . seq)
a . seq is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
((f,A,a,b,seq)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
S . seq is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Si,a . seq
middle_sum (Si,(S . seq)) is complex real ext-real Element of REAL
Sum (S . seq) is complex real ext-real Element of REAL
addreal $$ (S . seq) is complex real ext-real Element of REAL
(f,A,(a . seq),(f,A,a,b,seq)) is complex Element of COMPLEX
Sum (f,A,a,b,seq) is complex Element of COMPLEX
addcomplex $$ (f,A,a,b,seq) is complex Element of COMPLEX
Re (f,A,(a . seq),(f,A,a,b,seq)) is complex real ext-real Element of REAL
lim S is complex real ext-real Element of REAL
lim (middle_sum (Si,S)) is complex real ext-real Element of REAL
integral Si is complex real ext-real Element of REAL
seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S . seq is complex real ext-real Element of REAL
T . seq is complex Element of COMPLEX
Re (T . seq) is complex real ext-real Element of REAL
Si is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim Si is complex real ext-real Element of REAL
Si is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim Si is complex real ext-real Element of REAL
Im (f,A) is complex real ext-real Element of REAL
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(f,A,a,b,S) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . S)
a . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
((f,A,a,b,S)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
S is non empty Relation-like NAT -defined REAL * -valued Function-like total quasi_total Element of K6(K7(NAT,(REAL *)))
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
(f,A,a,b,S) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . S)
a . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
((f,A,a,b,S)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom ((f,A,a,b,S)) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len (f,A,a,b,S) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (f,A,a,b,S)) is V32() V39( len (f,A,a,b,S)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (f,A,a,b,S) ) } is set
dom (f,A,a,b,S) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
xs is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S . S is FinSequence-like Element of REAL *
a . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
(f,A,a,b,S) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . S)
((f,A,a,b,S)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
xseq is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom xseq is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
len (f,A,a,b,S) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (f,A,a,b,S)) is V32() V39( len (f,A,a,b,S)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (f,A,a,b,S) ) } is set
seq is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len seq) is V32() V39( len seq) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len seq ) } is set
dom seq is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
rseqi is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
divset ((a . S),rseqi) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((a . S),rseqi)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
rng (A | (divset ((a . S),rseqi))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
(f,A,a,b,S) . rseqi is complex set
vol (divset ((a . S),rseqi)) is complex real ext-real Element of REAL
k is complex Element of COMPLEX
k * (vol (divset ((a . S),rseqi))) is complex Element of COMPLEX
Im k is complex real ext-real Element of REAL
H is complex real ext-real Element of REAL
dom (A | (divset ((a . S),rseqi))) is V126() V127() V128() Element of K6(f)
K6(f) is set
j0 is set
(A | (divset ((a . S),rseqi))) . j0 is complex set
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset ((a . S),rseqi)) is V126() V127() V128() Element of K6(REAL)
dom (Im A) is V126() V127() V128() Element of K6(f)
dom xs is V126() V127() V128() Element of K6(f)
(dom xs) /\ (divset ((a . S),rseqi)) is V126() V127() V128() Element of K6(REAL)
xs | (divset ((a . S),rseqi)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
dom (xs | (divset ((a . S),rseqi))) is V126() V127() V128() Element of K6(f)
A . j0 is complex set
Im (A . j0) is complex real ext-real Element of REAL
(Im A) . j0 is complex real ext-real Element of REAL
(xs | (divset ((a . S),rseqi))) . j0 is complex real ext-real Element of REAL
z is complex real ext-real Element of REAL
rng (xs | (divset ((a . S),rseqi))) is V126() V127() V128() Element of K6(REAL)
xseq . rseqi is complex real ext-real Element of REAL
Im ((f,A,a,b,S) . rseqi) is complex real ext-real Element of REAL
z * (vol (divset ((a . S),rseqi))) is complex real ext-real Element of REAL
len xseq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S is non empty Relation-like NAT -defined REAL * -valued Function-like total quasi_total middle_volume_Sequence of xs,a
middle_sum (xs,S) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
seq is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
xseq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
seq . xseq is complex real ext-real Element of REAL
T . xseq is complex Element of COMPLEX
Im (T . xseq) is complex real ext-real Element of REAL
(f,A,a,b,xseq) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,a . xseq)
a . xseq is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
((f,A,a,b,xseq)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
S . xseq is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of xs,a . xseq
middle_sum (xs,(S . xseq)) is complex real ext-real Element of REAL
Sum (S . xseq) is complex real ext-real Element of REAL
addreal $$ (S . xseq) is complex real ext-real Element of REAL
(f,A,(a . xseq),(f,A,a,b,xseq)) is complex Element of COMPLEX
Sum (f,A,a,b,xseq) is complex Element of COMPLEX
addcomplex $$ (f,A,a,b,xseq) is complex Element of COMPLEX
Im (f,A,(a . xseq),(f,A,a,b,xseq)) is complex real ext-real Element of REAL
lim seq is complex real ext-real Element of REAL
lim (middle_sum (xs,S)) is complex real ext-real Element of REAL
integral xs is complex real ext-real Element of REAL
xseq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
seq . xseq is complex real ext-real Element of REAL
T . xseq is complex Element of COMPLEX
Im (T . xseq) is complex real ext-real Element of REAL
xs is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim xs is complex real ext-real Element of REAL
xs is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim xs is complex real ext-real Element of REAL
(lim xs) * <i> is complex Element of COMPLEX
(lim Si) + ((lim xs) * <i>) is complex Element of COMPLEX
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
divs f is non empty set
K7(NAT,(divs f)) is set
K6(K7(NAT,(divs f))) is set
A is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
(f,A) is complex Element of COMPLEX
Re A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
integral (Re A) is complex real ext-real Element of REAL
Im A is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
integral (Im A) is complex real ext-real Element of REAL
(integral (Im A)) * <i> is complex Element of COMPLEX
(integral (Re A)) + ((integral (Im A)) * <i>) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
g0 is non empty Relation-like NAT -defined divs f -valued Function-like total quasi_total Element of K6(K7(NAT,(divs f)))
delta g0 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim (delta g0) is complex real ext-real Element of REAL
G is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total (f,A,g0)
(f,A,g0,G) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
lim (f,A,g0,G) is complex Element of COMPLEX
a is complex Element of COMPLEX
a is complex Element of COMPLEX
Re a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
T is non empty Relation-like NAT -defined divs f -valued Function-like total quasi_total Element of K6(K7(NAT,(divs f)))
Si is non empty Relation-like NAT -defined REAL * -valued Function-like total quasi_total middle_volume_Sequence of Re A,T
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
T . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
Si . S is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Re A,T . S
S is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len S) is V32() V39( len S) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len S ) } is set
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
xseq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom S is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
divset ((T . S),xseq) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
(Re A) | (divset ((T . S),xseq)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
rng ((Re A) | (divset ((T . S),xseq))) is V126() V127() V128() Element of K6(REAL)
(Si . S) . xseq is complex real ext-real Element of REAL
vol (divset ((T . S),xseq)) is complex real ext-real Element of REAL
rseqi is complex real ext-real Element of REAL
rseqi * (vol (divset ((T . S),xseq))) is complex real ext-real Element of REAL
dom ((Re A) | (divset ((T . S),xseq))) is V126() V127() V128() Element of K6(f)
K6(f) is set
k is set
((Re A) | (divset ((T . S),xseq))) . k is complex real ext-real Element of REAL
dom (Re A) is V126() V127() V128() Element of K6(f)
(dom (Re A)) /\ (divset ((T . S),xseq)) is V126() V127() V128() Element of K6(REAL)
A | (divset ((T . S),xseq)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),xseq))) is V126() V127() V128() Element of K6(f)
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset ((T . S),xseq)) is V126() V127() V128() Element of K6(REAL)
H is complex real ext-real Element of REAL
(A | (divset ((T . S),xseq))) . H is complex set
rng (A | (divset ((T . S),xseq))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
z is complex Element of COMPLEX
(vol (divset ((T . S),xseq))) * z is complex Element of COMPLEX
j0 is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
dom seq is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
xseq is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() Element of COMPLEX *
rseqi is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom S is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
seq . k is complex set
divset ((T . S),rseqi) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),rseqi)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),rseqi))) is V126() V127() V128() Element of K6(f)
K6(f) is set
(Si . S) . rseqi is complex real ext-real Element of REAL
vol (divset ((T . S),rseqi)) is complex real ext-real Element of REAL
(Re A) | (divset ((T . S),rseqi)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
seq . rseqi is complex set
H is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
j0 is complex real ext-real Element of REAL
divset ((T . S),H) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),H)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),H))) is V126() V127() V128() Element of K6(f)
(Si . S) . H is complex real ext-real Element of REAL
vol (divset ((T . S),H)) is complex real ext-real Element of REAL
(Re A) | (divset ((T . S),H)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
((Re A) | (divset ((T . S),H))) . j0 is complex real ext-real Element of REAL
(vol (divset ((T . S),H))) * (((Re A) | (divset ((T . S),H))) . j0) is complex real ext-real Element of REAL
z is complex Element of COMPLEX
(A | (divset ((T . S),H))) . j0 is complex set
(vol (divset ((T . S),H))) * z is complex Element of COMPLEX
len seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total Element of K6(K7(NAT,(COMPLEX *)))
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S . S is FinSequence-like Element of COMPLEX *
T . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
Si . S is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Re A,T . S
seq is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
xseq is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
len xseq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom seq is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
rseqi is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
divset ((T . S),k) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),k)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),k))) is V126() V127() V128() Element of K6(f)
K6(f) is set
(Si . S) . k is complex real ext-real Element of REAL
vol (divset ((T . S),k)) is complex real ext-real Element of REAL
(Re A) | (divset ((T . S),k)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
xseq . k is set
z is complex real ext-real Element of REAL
((Re A) | (divset ((T . S),k))) . z is complex real ext-real Element of REAL
(vol (divset ((T . S),k))) * (((Re A) | (divset ((T . S),k))) . z) is complex real ext-real Element of REAL
H is complex Element of COMPLEX
(A | (divset ((T . S),k))) . z is complex set
(vol (divset ((T . S),k))) * H is complex Element of COMPLEX
j0 is complex Element of COMPLEX
divset ((T . S),rseqi) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),rseqi)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
rng (A | (divset ((T . S),rseqi))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
xseq . rseqi is set
vol (divset ((T . S),rseqi)) is complex real ext-real Element of REAL
j0 * (vol (divset ((T . S),rseqi))) is complex Element of COMPLEX
S is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total (f,A,T)
(f,A,T,S) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
delta T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim (delta T) is complex real ext-real Element of REAL
lim (f,A,T,S) is complex Element of COMPLEX
Re (f,A,T,S) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
rseqi is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
xseq is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
xs is complex Element of COMPLEX
Re xs is complex real ext-real Element of REAL
lim rseqi is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
rseqi . k is complex real ext-real Element of REAL
xseq . k is complex Element of COMPLEX
Re (xseq . k) is complex real ext-real Element of REAL
middle_sum ((Re A),Si) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
rseqi . k is complex real ext-real Element of REAL
(middle_sum ((Re A),Si)) . k is complex real ext-real Element of REAL
T . k is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
(f,A,T,S,k) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,T . k)
Si . k is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Re A,T . k
H is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len H is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
len z is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom H is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
((f,A,T,S,k)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom ((f,A,T,S,k)) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom (f,A,T,S,k) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
Seg (len H) is V32() V39( len H) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len H ) } is set
len (Si . k) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (Si . k)) is V32() V39( len (Si . k)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (Si . k) ) } is set
dom (Si . k) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
j0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
((f,A,T,S,k)) . j0 is complex real ext-real Element of REAL
(Si . k) . j0 is complex real ext-real Element of REAL
j is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
divset ((T . k),j) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . k),j)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . k),j))) is V126() V127() V128() Element of K6(f)
K6(f) is set
(Si . k) . j is complex real ext-real Element of REAL
vol (divset ((T . k),j)) is complex real ext-real Element of REAL
(Re A) | (divset ((T . k),j)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
z . j is set
tji is complex real ext-real Element of REAL
((Re A) | (divset ((T . k),j))) . tji is complex real ext-real Element of REAL
(vol (divset ((T . k),j))) * (((Re A) | (divset ((T . k),j))) . tji) is complex real ext-real Element of REAL
rji is complex Element of COMPLEX
(A | (divset ((T . k),j))) . tji is complex set
(vol (divset ((T . k),j))) * rji is complex Element of COMPLEX
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset ((T . k),j)) is V126() V127() V128() Element of K6(REAL)
dom (Re A) is V126() V127() V128() Element of K6(f)
(dom (Re A)) /\ (divset ((T . k),j)) is V126() V127() V128() Element of K6(REAL)
dom ((Re A) | (divset ((T . k),j))) is V126() V127() V128() Element of K6(f)
(Re A) . tji is complex real ext-real Element of REAL
A . tji is complex set
Re (A . tji) is complex real ext-real Element of REAL
Re rji is complex real ext-real Element of REAL
((f,A,T,S,k)) . j is complex real ext-real Element of REAL
(f,A,T,S,k) . j is complex set
Re ((f,A,T,S,k) . j) is complex real ext-real Element of REAL
j0 is set
((f,A,T,S,k)) . j0 is complex real ext-real Element of REAL
(Si . k) . j0 is complex real ext-real Element of REAL
xseq . k is complex Element of COMPLEX
Re (xseq . k) is complex real ext-real Element of REAL
(f,A,(T . k),(f,A,T,S,k)) is complex Element of COMPLEX
Sum (f,A,T,S,k) is complex Element of COMPLEX
addcomplex $$ (f,A,T,S,k) is complex Element of COMPLEX
Re (f,A,(T . k),(f,A,T,S,k)) is complex real ext-real Element of REAL
middle_sum ((Re A),(Si . k)) is complex real ext-real Element of REAL
Sum (Si . k) is complex real ext-real Element of REAL
addreal $$ (Si . k) is complex real ext-real Element of REAL
lim (middle_sum ((Re A),Si)) is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
T is non empty Relation-like NAT -defined divs f -valued Function-like total quasi_total Element of K6(K7(NAT,(divs f)))
Si is non empty Relation-like NAT -defined REAL * -valued Function-like total quasi_total middle_volume_Sequence of Im A,T
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
T . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
Si . S is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Im A,T . S
S is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len S) is V32() V39( len S) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len S ) } is set
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
xseq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom S is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
divset ((T . S),xseq) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
(Im A) | (divset ((T . S),xseq)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
rng ((Im A) | (divset ((T . S),xseq))) is V126() V127() V128() Element of K6(REAL)
(Si . S) . xseq is complex real ext-real Element of REAL
vol (divset ((T . S),xseq)) is complex real ext-real Element of REAL
rseqi is complex real ext-real Element of REAL
rseqi * (vol (divset ((T . S),xseq))) is complex real ext-real Element of REAL
dom ((Im A) | (divset ((T . S),xseq))) is V126() V127() V128() Element of K6(f)
K6(f) is set
k is set
((Im A) | (divset ((T . S),xseq))) . k is complex real ext-real Element of REAL
dom (Im A) is V126() V127() V128() Element of K6(f)
(dom (Im A)) /\ (divset ((T . S),xseq)) is V126() V127() V128() Element of K6(REAL)
A | (divset ((T . S),xseq)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),xseq))) is V126() V127() V128() Element of K6(f)
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset ((T . S),xseq)) is V126() V127() V128() Element of K6(REAL)
H is complex real ext-real Element of REAL
(A | (divset ((T . S),xseq))) . H is complex set
rng (A | (divset ((T . S),xseq))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
z is complex Element of COMPLEX
(vol (divset ((T . S),xseq))) * z is complex Element of COMPLEX
j0 is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() FinSequence of COMPLEX
dom seq is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
xseq is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() Element of COMPLEX *
rseqi is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom S is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
seq . k is complex set
divset ((T . S),rseqi) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),rseqi)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),rseqi))) is V126() V127() V128() Element of K6(f)
K6(f) is set
(Si . S) . rseqi is complex real ext-real Element of REAL
vol (divset ((T . S),rseqi)) is complex real ext-real Element of REAL
(Im A) | (divset ((T . S),rseqi)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
seq . rseqi is complex set
H is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
j0 is complex real ext-real Element of REAL
divset ((T . S),H) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),H)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),H))) is V126() V127() V128() Element of K6(f)
(Si . S) . H is complex real ext-real Element of REAL
vol (divset ((T . S),H)) is complex real ext-real Element of REAL
(Im A) | (divset ((T . S),H)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
((Im A) | (divset ((T . S),H))) . j0 is complex real ext-real Element of REAL
(vol (divset ((T . S),H))) * (((Im A) | (divset ((T . S),H))) . j0) is complex real ext-real Element of REAL
z is complex Element of COMPLEX
(A | (divset ((T . S),H))) . j0 is complex set
(vol (divset ((T . S),H))) * z is complex Element of COMPLEX
len seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total Element of K6(K7(NAT,(COMPLEX *)))
S is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
S . S is FinSequence-like Element of COMPLEX *
T . S is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
Si . S is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Im A,T . S
seq is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
xseq is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len seq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
len xseq is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom seq is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
rseqi is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
divset ((T . S),k) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),k)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . S),k))) is V126() V127() V128() Element of K6(f)
K6(f) is set
(Si . S) . k is complex real ext-real Element of REAL
vol (divset ((T . S),k)) is complex real ext-real Element of REAL
(Im A) | (divset ((T . S),k)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
xseq . k is set
z is complex real ext-real Element of REAL
((Im A) | (divset ((T . S),k))) . z is complex real ext-real Element of REAL
(vol (divset ((T . S),k))) * (((Im A) | (divset ((T . S),k))) . z) is complex real ext-real Element of REAL
H is complex Element of COMPLEX
(A | (divset ((T . S),k))) . z is complex set
(vol (divset ((T . S),k))) * H is complex Element of COMPLEX
j0 is complex Element of COMPLEX
divset ((T . S),rseqi) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . S),rseqi)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
rng (A | (divset ((T . S),rseqi))) is V126() Element of K6(COMPLEX)
K6(COMPLEX) is set
xseq . rseqi is set
vol (divset ((T . S),rseqi)) is complex real ext-real Element of REAL
j0 * (vol (divset ((T . S),rseqi))) is complex Element of COMPLEX
S is non empty Relation-like NAT -defined COMPLEX * -valued Function-like total quasi_total (f,A,T)
(f,A,T,S) is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
delta T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
lim (delta T) is complex real ext-real Element of REAL
lim (f,A,T,S) is complex Element of COMPLEX
Im (f,A,T,S) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
rseqi is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
xseq is non empty Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(NAT,COMPLEX))
xs is complex Element of COMPLEX
Im xs is complex real ext-real Element of REAL
lim rseqi is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
rseqi . k is complex real ext-real Element of REAL
xseq . k is complex Element of COMPLEX
Im (xseq . k) is complex real ext-real Element of REAL
middle_sum ((Im A),Si) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
rseqi . k is complex real ext-real Element of REAL
(middle_sum ((Im A),Si)) . k is complex real ext-real Element of REAL
T . k is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() Division of f
(f,A,T,S,k) is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like V116() (f,A,T . k)
Si . k is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() middle_volume of Im A,T . k
H is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len H is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
len z is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
dom H is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
((f,A,T,S,k)) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() FinSequence of REAL
dom ((f,A,T,S,k)) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
dom (f,A,T,S,k) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
Seg (len H) is V32() V39( len H) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len H ) } is set
len (Si . k) is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
Seg (len (Si . k)) is V32() V39( len (Si . k)) V126() V127() V128() V129() V130() V131() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT : ( 1 <= b₁ & b₁ <= len (Si . k) ) } is set
dom (Si . k) is V126() V127() V128() V129() V130() V131() Element of K6(NAT)
j0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real set
((f,A,T,S,k)) . j0 is complex real ext-real Element of REAL
(Si . k) . j0 is complex real ext-real Element of REAL
j is epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() Element of NAT
divset ((T . k),j) is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A | (divset ((T . k),j)) is Relation-like f -defined COMPLEX -valued Function-like V116() Element of K6(K7(f,COMPLEX))
dom (A | (divset ((T . k),j))) is V126() V127() V128() Element of K6(f)
K6(f) is set
(Si . k) . j is complex real ext-real Element of REAL
vol (divset ((T . k),j)) is complex real ext-real Element of REAL
(Im A) | (divset ((T . k),j)) is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
z . j is set
tji is complex real ext-real Element of REAL
((Im A) | (divset ((T . k),j))) . tji is complex real ext-real Element of REAL
(vol (divset ((T . k),j))) * (((Im A) | (divset ((T . k),j))) . tji) is complex real ext-real Element of REAL
rji is complex Element of COMPLEX
(A | (divset ((T . k),j))) . tji is complex set
(vol (divset ((T . k),j))) * rji is complex Element of COMPLEX
dom A is V126() V127() V128() Element of K6(f)
(dom A) /\ (divset ((T . k),j)) is V126() V127() V128() Element of K6(REAL)
dom (Im A) is V126() V127() V128() Element of K6(f)
(dom (Im A)) /\ (divset ((T . k),j)) is V126() V127() V128() Element of K6(REAL)
dom ((Im A) | (divset ((T . k),j))) is V126() V127() V128() Element of K6(f)
(Im A) . tji is complex real ext-real Element of REAL
A . tji is complex set
Im (A . tji) is complex real ext-real Element of REAL
Im rji is complex real ext-real Element of REAL
((f,A,T,S,k)) . j is complex real ext-real Element of REAL
(f,A,T,S,k) . j is complex set
Im ((f,A,T,S,k) . j) is complex real ext-real Element of REAL
j0 is set
((f,A,T,S,k)) . j0 is complex real ext-real Element of REAL
(Si . k) . j0 is complex real ext-real Element of REAL
xseq . k is complex Element of COMPLEX
Im (xseq . k) is complex real ext-real Element of REAL
(f,A,(T . k),(f,A,T,S,k)) is complex Element of COMPLEX
Sum (f,A,T,S,k) is complex Element of COMPLEX
addcomplex $$ (f,A,T,S,k) is complex Element of COMPLEX
Im (f,A,(T . k),(f,A,T,S,k)) is complex real ext-real Element of REAL
middle_sum ((Im A),(Si . k)) is complex real ext-real Element of REAL
Sum (Si . k) is complex real ext-real Element of REAL
addreal $$ (Si . k) is complex real ext-real Element of REAL
lim (middle_sum ((Im A),Si)) is complex real ext-real Element of REAL
g0 is complex real ext-real Element of REAL
a is complex Element of COMPLEX
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re A),f) is complex real ext-real Element of REAL
(Re A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
integral ((Re A) || f) is complex real ext-real Element of REAL
Im A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im A),f) is complex real ext-real Element of REAL
(Im A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Im A) || f) is complex real ext-real Element of REAL
(integral ((Im A),f)) * <i> is complex Element of COMPLEX
(integral ((Re A),f)) + ((integral ((Im A),f)) * <i>) is complex Element of COMPLEX
f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
A is V126() V127() V128() Element of K6(REAL)
f | A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re (f | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re f) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im (f | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im f) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom ((Re f) | A) is V126() V127() V128() Element of K6(REAL)
dom (Re f) is V126() V127() V128() Element of K6(REAL)
(dom (Re f)) /\ A is V126() V127() V128() Element of K6(REAL)
dom f is V126() V127() V128() Element of K6(REAL)
(dom f) /\ A is V126() V127() V128() Element of K6(REAL)
dom (f | A) is V126() V127() V128() Element of K6(REAL)
dom (Re (f | A)) is V126() V127() V128() Element of K6(REAL)
a is set
(Re (f | A)) . a is complex real ext-real Element of REAL
(f | A) . a is complex set
Re ((f | A) . a) is complex real ext-real Element of REAL
f . a is complex set
Re (f . a) is complex real ext-real Element of REAL
(Re f) . a is complex real ext-real Element of REAL
((Re f) | A) . a is complex real ext-real Element of REAL
dom ((Im f) | A) is V126() V127() V128() Element of K6(REAL)
dom (Im f) is V126() V127() V128() Element of K6(REAL)
(dom (Im f)) /\ A is V126() V127() V128() Element of K6(REAL)
dom (Im (f | A)) is V126() V127() V128() Element of K6(REAL)
a is set
(Im (f | A)) . a is complex real ext-real Element of REAL
(f | A) . a is complex set
Im ((f | A) . a) is complex real ext-real Element of REAL
f . a is complex set
Im (f . a) is complex real ext-real Element of REAL
(Im f) . a is complex real ext-real Element of REAL
((Im f) | A) . a is complex real ext-real Element of REAL
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
A | f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
a is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
Re a is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
Im a is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
dom a is V126() V127() V128() Element of K6(f)
K6(f) is set
dom A is V126() V127() V128() Element of K6(REAL)
(dom A) /\ f is V126() V127() V128() Element of K6(REAL)
Re A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom (Re A) is V126() V127() V128() Element of K6(REAL)
(dom (Re A)) /\ f is V126() V127() V128() Element of K6(REAL)
(Re A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
(Re A) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
g0 is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re g0 is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
b is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
Im A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom (Im A) is V126() V127() V128() Element of K6(REAL)
(dom (Im A)) /\ f is V126() V127() V128() Element of K6(REAL)
(Im A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
(Im A) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im g0 is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
G is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
Re A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom a is V126() V127() V128() Element of K6(f)
K6(f) is set
Re a is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
b is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re b is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
Im a is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
Im b is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
K7(f,COMPLEX) is V116() set
K6(K7(f,COMPLEX)) is set
A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
A | f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
(f,A) is complex Element of COMPLEX
Re A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re A),f) is complex real ext-real Element of REAL
(Re A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
integral ((Re A) || f) is complex real ext-real Element of REAL
Im A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im A),f) is complex real ext-real Element of REAL
(Im A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Im A) || f) is complex real ext-real Element of REAL
(integral ((Im A),f)) * <i> is complex Element of COMPLEX
(integral ((Re A),f)) + ((integral ((Im A),f)) * <i>) is complex Element of COMPLEX
a is non empty Relation-like f -defined COMPLEX -valued Function-like total quasi_total V116() Element of K6(K7(f,COMPLEX))
(f,a) is complex Element of COMPLEX
Re a is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
integral (Re a) is complex real ext-real Element of REAL
Im a is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
integral (Im a) is complex real ext-real Element of REAL
(integral (Im a)) * <i> is complex Element of COMPLEX
(integral (Re a)) + ((integral (Im a)) * <i>) is complex Element of COMPLEX
dom a is V126() V127() V128() Element of K6(f)
K6(f) is set
dom A is V126() V127() V128() Element of K6(REAL)
(dom A) /\ f is V126() V127() V128() Element of K6(REAL)
dom (Re A) is V126() V127() V128() Element of K6(REAL)
(dom (Re A)) /\ f is V126() V127() V128() Element of K6(REAL)
(Re A) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
g0 is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re g0 is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
b is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
dom (Im A) is V126() V127() V128() Element of K6(REAL)
(dom (Im A)) /\ f is V126() V127() V128() Element of K6(REAL)
(Im A) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im g0 is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
G is non empty Relation-like f -defined REAL -valued Function-like total quasi_total V116() V117() V118() Element of K6(K7(f,REAL))
f is complex real ext-real set
A is complex real ext-real set
a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re a),f,A) is complex real ext-real Element of REAL
Im a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im a),f,A) is complex real ext-real Element of REAL
(integral ((Im a),f,A)) * <i> is complex Element of COMPLEX
(integral ((Re a),f,A)) + ((integral ((Im a),f,A)) * <i>) is complex Element of COMPLEX
f is complex set
Re f is complex real ext-real Element of REAL
Im f is complex real ext-real Element of REAL
A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
f (#) A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
Re (f (#) A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Re A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re f) (#) (Re A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im f) (#) (Im A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Re f) (#) (Re A)) - ((Im f) (#) (Im A)) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im (f (#) A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re f) (#) (Im A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im f) (#) (Re A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Re f) (#) (Im A)) + ((Im f) (#) (Re A)) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom (Re (f (#) A)) is V126() V127() V128() Element of K6(REAL)
dom (f (#) A) is V126() V127() V128() Element of K6(REAL)
dom A is V126() V127() V128() Element of K6(REAL)
dom (Im (f (#) A)) is V126() V127() V128() Element of K6(REAL)
dom ((Re f) (#) (Re A)) is V126() V127() V128() Element of K6(REAL)
dom (Re A) is V126() V127() V128() Element of K6(REAL)
dom ((Im f) (#) (Im A)) is V126() V127() V128() Element of K6(REAL)
dom (Im A) is V126() V127() V128() Element of K6(REAL)
dom ((Im f) (#) (Re A)) is V126() V127() V128() Element of K6(REAL)
dom ((Re f) (#) (Im A)) is V126() V127() V128() Element of K6(REAL)
(dom A) /\ (dom A) is V126() V127() V128() Element of K6(REAL)
dom (((Re f) (#) (Re A)) - ((Im f) (#) (Im A))) is V126() V127() V128() Element of K6(REAL)
dom (((Re f) (#) (Im A)) + ((Im f) (#) (Re A))) is V126() V127() V128() Element of K6(REAL)
a is set
(Re (f (#) A)) . a is complex real ext-real Element of REAL
(f (#) A) . a is complex set
Re ((f (#) A) . a) is complex real ext-real Element of REAL
A . a is complex set
f * (A . a) is complex Element of COMPLEX
Re (f * (A . a)) is complex real ext-real Element of REAL
Re (A . a) is complex real ext-real Element of REAL
(Re f) * (Re (A . a)) is complex real ext-real Element of REAL
Im (A . a) is complex real ext-real Element of REAL
(Im f) * (Im (A . a)) is complex real ext-real Element of REAL
((Re f) * (Re (A . a))) - ((Im f) * (Im (A . a))) is complex real ext-real Element of REAL
(Re A) . a is complex real ext-real Element of REAL
(Re f) * ((Re A) . a) is complex real ext-real Element of REAL
((Re f) * ((Re A) . a)) - ((Im f) * (Im (A . a))) is complex real ext-real Element of REAL
(Im A) . a is complex real ext-real Element of REAL
(Im f) * ((Im A) . a) is complex real ext-real Element of REAL
((Re f) * ((Re A) . a)) - ((Im f) * ((Im A) . a)) is complex real ext-real Element of REAL
((Re f) (#) (Re A)) . a is complex real ext-real Element of REAL
(((Re f) (#) (Re A)) . a) - ((Im f) * ((Im A) . a)) is complex real ext-real Element of REAL
((Im f) (#) (Im A)) . a is complex real ext-real Element of REAL
(((Re f) (#) (Re A)) . a) - (((Im f) (#) (Im A)) . a) is complex real ext-real Element of REAL
(((Re f) (#) (Re A)) - ((Im f) (#) (Im A))) . a is complex real ext-real Element of REAL
a is set
(Im (f (#) A)) . a is complex real ext-real Element of REAL
(f (#) A) . a is complex set
Im ((f (#) A) . a) is complex real ext-real Element of REAL
A . a is complex set
f * (A . a) is complex Element of COMPLEX
Im (f * (A . a)) is complex real ext-real Element of REAL
Im (A . a) is complex real ext-real Element of REAL
(Re f) * (Im (A . a)) is complex real ext-real Element of REAL
Re (A . a) is complex real ext-real Element of REAL
(Im f) * (Re (A . a)) is complex real ext-real Element of REAL
((Re f) * (Im (A . a))) + ((Im f) * (Re (A . a))) is complex real ext-real Element of REAL
(Im A) . a is complex real ext-real Element of REAL
(Re f) * ((Im A) . a) is complex real ext-real Element of REAL
((Re f) * ((Im A) . a)) + ((Im f) * (Re (A . a))) is complex real ext-real Element of REAL
(Re A) . a is complex real ext-real Element of REAL
(Im f) * ((Re A) . a) is complex real ext-real Element of REAL
((Re f) * ((Im A) . a)) + ((Im f) * ((Re A) . a)) is complex real ext-real Element of REAL
((Re f) (#) (Im A)) . a is complex real ext-real Element of REAL
(((Re f) (#) (Im A)) . a) + ((Im f) * ((Re A) . a)) is complex real ext-real Element of REAL
((Im f) (#) (Re A)) . a is complex real ext-real Element of REAL
(((Re f) (#) (Im A)) . a) + (((Im f) (#) (Re A)) . a) is complex real ext-real Element of REAL
(((Re f) (#) (Im A)) + ((Im f) (#) (Re A))) . a is complex real ext-real Element of REAL
f is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
dom A is V126() V127() V128() Element of K6(REAL)
dom a is V126() V127() V128() Element of K6(REAL)
A | f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
a | f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
A + a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
A - a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
(f,(A + a)) is complex Element of COMPLEX
Re (A + a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re (A + a)),f) is complex real ext-real Element of REAL
(Re (A + a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
K7(f,REAL) is V116() V117() V118() set
K6(K7(f,REAL)) is set
integral ((Re (A + a)) || f) is complex real ext-real Element of REAL
Im (A + a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im (A + a)),f) is complex real ext-real Element of REAL
(Im (A + a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Im (A + a)) || f) is complex real ext-real Element of REAL
(integral ((Im (A + a)),f)) * <i> is complex Element of COMPLEX
(integral ((Re (A + a)),f)) + ((integral ((Im (A + a)),f)) * <i>) is complex Element of COMPLEX
(f,A) is complex Element of COMPLEX
Re A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re A),f) is complex real ext-real Element of REAL
(Re A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Re A) || f) is complex real ext-real Element of REAL
Im A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im A),f) is complex real ext-real Element of REAL
(Im A) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Im A) || f) is complex real ext-real Element of REAL
(integral ((Im A),f)) * <i> is complex Element of COMPLEX
(integral ((Re A),f)) + ((integral ((Im A),f)) * <i>) is complex Element of COMPLEX
(f,a) is complex Element of COMPLEX
Re a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re a),f) is complex real ext-real Element of REAL
(Re a) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Re a) || f) is complex real ext-real Element of REAL
Im a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im a),f) is complex real ext-real Element of REAL
(Im a) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Im a) || f) is complex real ext-real Element of REAL
(integral ((Im a),f)) * <i> is complex Element of COMPLEX
(integral ((Re a),f)) + ((integral ((Im a),f)) * <i>) is complex Element of COMPLEX
(f,A) + (f,a) is complex Element of COMPLEX
(f,(A - a)) is complex Element of COMPLEX
Re (A - a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re (A - a)),f) is complex real ext-real Element of REAL
(Re (A - a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Re (A - a)) || f) is complex real ext-real Element of REAL
Im (A - a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im (A - a)),f) is complex real ext-real Element of REAL
(Im (A - a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral ((Im (A - a)) || f) is complex real ext-real Element of REAL
(integral ((Im (A - a)),f)) * <i> is complex Element of COMPLEX
(integral ((Re (A - a)),f)) + ((integral ((Im (A - a)),f)) * <i>) is complex Element of COMPLEX
(f,A) - (f,a) is complex Element of COMPLEX
(Re A) + (Re a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im A) + (Im a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral (((Re A) + (Re a)),f) is complex real ext-real Element of REAL
((Re A) + (Re a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral (((Re A) + (Re a)) || f) is complex real ext-real Element of REAL
(integral ((Re A),f)) + (integral ((Re a),f)) is complex real ext-real Element of REAL
integral (((Im A) + (Im a)),f) is complex real ext-real Element of REAL
((Im A) + (Im a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral (((Im A) + (Im a)) || f) is complex real ext-real Element of REAL
(integral ((Im A),f)) + (integral ((Im a),f)) is complex real ext-real Element of REAL
(Re A) - (Re a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im A) - (Im a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral (((Re A) - (Re a)),f) is complex real ext-real Element of REAL
((Re A) - (Re a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral (((Re A) - (Re a)) || f) is complex real ext-real Element of REAL
(integral ((Re A),f)) - (integral ((Re a),f)) is complex real ext-real Element of REAL
integral (((Im A) - (Im a)),f) is complex real ext-real Element of REAL
((Im A) - (Im a)) || f is Relation-like f -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(f,REAL))
integral (((Im A) - (Im a)) || f) is complex real ext-real Element of REAL
(integral ((Im A),f)) - (integral ((Im a),f)) is complex real ext-real Element of REAL
dom (Re A) is V126() V127() V128() Element of K6(REAL)
dom (Re a) is V126() V127() V128() Element of K6(REAL)
dom (Im A) is V126() V127() V128() Element of K6(REAL)
dom (Im a) is V126() V127() V128() Element of K6(REAL)
Re (a | f) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im (a | f) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re a) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im a) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Re (A | f) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im (A | f) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re A) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im A) | f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Re (f,A) is complex real ext-real Element of REAL
Re (f,a) is complex real ext-real Element of REAL
(Re (f,A)) + (Re (f,a)) is complex real ext-real Element of REAL
Im (f,A) is complex real ext-real Element of REAL
Im (f,a) is complex real ext-real Element of REAL
(Im (f,A)) + (Im (f,a)) is complex real ext-real Element of REAL
(Re (f,A)) - (Re (f,a)) is complex real ext-real Element of REAL
(Im (f,A)) - (Im (f,a)) is complex real ext-real Element of REAL
Re (f,(A + a)) is complex real ext-real Element of REAL
Im (f,(A + a)) is complex real ext-real Element of REAL
Re (f,(A - a)) is complex real ext-real Element of REAL
Im (f,(A - a)) is complex real ext-real Element of REAL
Re ((f,A) + (f,a)) is complex real ext-real Element of REAL
Im ((f,A) + (f,a)) is complex real ext-real Element of REAL
Re ((f,A) - (f,a)) is complex real ext-real Element of REAL
Im ((f,A) - (f,a)) is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
A is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
dom a is V126() V127() V128() Element of K6(REAL)
a | A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
f (#) a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
(A,(f (#) a)) is complex Element of COMPLEX
Re (f (#) a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re (f (#) a)),A) is complex real ext-real Element of REAL
(Re (f (#) a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
K7(A,REAL) is V116() V117() V118() set
K6(K7(A,REAL)) is set
integral ((Re (f (#) a)) || A) is complex real ext-real Element of REAL
Im (f (#) a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im (f (#) a)),A) is complex real ext-real Element of REAL
(Im (f (#) a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Im (f (#) a)) || A) is complex real ext-real Element of REAL
(integral ((Im (f (#) a)),A)) * <i> is complex Element of COMPLEX
(integral ((Re (f (#) a)),A)) + ((integral ((Im (f (#) a)),A)) * <i>) is complex Element of COMPLEX
(A,a) is complex Element of COMPLEX
Re a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re a),A) is complex real ext-real Element of REAL
(Re a) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Re a) || A) is complex real ext-real Element of REAL
Im a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im a),A) is complex real ext-real Element of REAL
(Im a) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Im a) || A) is complex real ext-real Element of REAL
(integral ((Im a),A)) * <i> is complex Element of COMPLEX
(integral ((Re a),A)) + ((integral ((Im a),A)) * <i>) is complex Element of COMPLEX
f * (A,a) is complex Element of COMPLEX
f (#) (Re a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((f (#) (Re a)),A) is complex real ext-real Element of REAL
(f (#) (Re a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((f (#) (Re a)) || A) is complex real ext-real Element of REAL
f * (integral ((Re a),A)) is complex real ext-real Element of REAL
f (#) (Im a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((f (#) (Im a)),A) is complex real ext-real Element of REAL
(f (#) (Im a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((f (#) (Im a)) || A) is complex real ext-real Element of REAL
f * (integral ((Im a),A)) is complex real ext-real Element of REAL
Re (a | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im (a | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re a) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im a) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom (Re a) is V126() V127() V128() Element of K6(REAL)
dom (Im a) is V126() V127() V128() Element of K6(REAL)
Re (A,(f (#) a)) is complex real ext-real Element of REAL
Re (A,a) is complex real ext-real Element of REAL
f * (Re (A,a)) is complex real ext-real Element of REAL
Im (A,(f (#) a)) is complex real ext-real Element of REAL
Im (A,a) is complex real ext-real Element of REAL
f * (Im (A,a)) is complex real ext-real Element of REAL
(Re a) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Re (a | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im a) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im (a | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom (Re a) is V126() V127() V128() Element of K6(REAL)
dom (Im a) is V126() V127() V128() Element of K6(REAL)
Re (f * (A,a)) is complex real ext-real Element of REAL
Im (f * (A,a)) is complex real ext-real Element of REAL
f is complex set
A is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
dom a is V126() V127() V128() Element of K6(REAL)
a | A is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
f (#) a is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
(A,(f (#) a)) is complex Element of COMPLEX
Re (f (#) a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re (f (#) a)),A) is complex real ext-real Element of REAL
(Re (f (#) a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
K7(A,REAL) is V116() V117() V118() set
K6(K7(A,REAL)) is set
integral ((Re (f (#) a)) || A) is complex real ext-real Element of REAL
Im (f (#) a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im (f (#) a)),A) is complex real ext-real Element of REAL
(Im (f (#) a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Im (f (#) a)) || A) is complex real ext-real Element of REAL
(integral ((Im (f (#) a)),A)) * <i> is complex Element of COMPLEX
(integral ((Re (f (#) a)),A)) + ((integral ((Im (f (#) a)),A)) * <i>) is complex Element of COMPLEX
(A,a) is complex Element of COMPLEX
Re a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re a),A) is complex real ext-real Element of REAL
(Re a) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Re a) || A) is complex real ext-real Element of REAL
Im a is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im a),A) is complex real ext-real Element of REAL
(Im a) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Im a) || A) is complex real ext-real Element of REAL
(integral ((Im a),A)) * <i> is complex Element of COMPLEX
(integral ((Re a),A)) + ((integral ((Im a),A)) * <i>) is complex Element of COMPLEX
f * (A,a) is complex Element of COMPLEX
Re (f * (A,a)) is complex real ext-real Element of REAL
Re f is complex real ext-real Element of REAL
(Re f) * (integral ((Re a),A)) is complex real ext-real Element of REAL
Im f is complex real ext-real Element of REAL
(Im f) * (integral ((Im a),A)) is complex real ext-real Element of REAL
((Re f) * (integral ((Re a),A))) - ((Im f) * (integral ((Im a),A))) is complex real ext-real Element of REAL
Im (f * (A,a)) is complex real ext-real Element of REAL
(Re f) * (integral ((Im a),A)) is complex real ext-real Element of REAL
(Im f) * (integral ((Re a),A)) is complex real ext-real Element of REAL
((Re f) * (integral ((Im a),A))) + ((Im f) * (integral ((Re a),A))) is complex real ext-real Element of REAL
Re (A,a) is complex real ext-real Element of REAL
Im (A,a) is complex real ext-real Element of REAL
(Re a) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Re (a | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im a) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
Im (a | A) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom (Re a) is V126() V127() V128() Element of K6(REAL)
dom (Im a) is V126() V127() V128() Element of K6(REAL)
(Re f) (#) (Re a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Re f) (#) (Im a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im f) (#) (Re a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
(Im f) (#) (Im a) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Re f) (#) (Re a)) - ((Im f) (#) (Im a)) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Re f) (#) (Im a)) + ((Im f) (#) (Re a)) is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Re f) (#) (Re a)) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Re f) (#) (Im a)) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Im f) (#) (Re a)) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
((Im f) (#) (Im a)) | A is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
dom ((Re f) (#) (Re a)) is V126() V127() V128() Element of K6(REAL)
dom ((Re f) (#) (Im a)) is V126() V127() V128() Element of K6(REAL)
dom ((Im f) (#) (Re a)) is V126() V127() V128() Element of K6(REAL)
dom ((Im f) (#) (Im a)) is V126() V127() V128() Element of K6(REAL)
Re (A,(f (#) a)) is complex real ext-real Element of REAL
integral (((Re f) (#) (Re a)),A) is complex real ext-real Element of REAL
((Re f) (#) (Re a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral (((Re f) (#) (Re a)) || A) is complex real ext-real Element of REAL
integral (((Im f) (#) (Im a)),A) is complex real ext-real Element of REAL
((Im f) (#) (Im a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral (((Im f) (#) (Im a)) || A) is complex real ext-real Element of REAL
(integral (((Re f) (#) (Re a)),A)) - (integral (((Im f) (#) (Im a)),A)) is complex real ext-real Element of REAL
((Re f) * (integral ((Re a),A))) - (integral (((Im f) (#) (Im a)),A)) is complex real ext-real Element of REAL
Im (A,(f (#) a)) is complex real ext-real Element of REAL
integral (((Re f) (#) (Im a)),A) is complex real ext-real Element of REAL
((Re f) (#) (Im a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral (((Re f) (#) (Im a)) || A) is complex real ext-real Element of REAL
integral (((Im f) (#) (Re a)),A) is complex real ext-real Element of REAL
((Im f) (#) (Re a)) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral (((Im f) (#) (Re a)) || A) is complex real ext-real Element of REAL
(integral (((Re f) (#) (Im a)),A)) + (integral (((Im f) (#) (Re a)),A)) is complex real ext-real Element of REAL
((Re f) * (integral ((Im a),A))) + (integral (((Im f) (#) (Re a)),A)) is complex real ext-real Element of REAL
f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
A is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
(A,f) is complex Element of COMPLEX
Re f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re f),A) is complex real ext-real Element of REAL
(Re f) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
K7(A,REAL) is V116() V117() V118() set
K6(K7(A,REAL)) is set
integral ((Re f) || A) is complex real ext-real Element of REAL
Im f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im f),A) is complex real ext-real Element of REAL
(Im f) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Im f) || A) is complex real ext-real Element of REAL
(integral ((Im f),A)) * <i> is complex Element of COMPLEX
(integral ((Re f),A)) + ((integral ((Im f),A)) * <i>) is complex Element of COMPLEX
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
[.a,b.] is V126() V127() V128() Element of K6(REAL)
(a,b,f) is complex Element of COMPLEX
integral ((Re f),a,b) is complex real ext-real Element of REAL
integral ((Im f),a,b) is complex real ext-real Element of REAL
(integral ((Im f),a,b)) * <i> is complex Element of COMPLEX
(integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>) is complex Element of COMPLEX
Re (A,f) is complex real ext-real Element of REAL
Im (A,f) is complex real ext-real Element of REAL
Re (a,b,f) is complex real ext-real Element of REAL
Im (a,b,f) is complex real ext-real Element of REAL
f is Relation-like REAL -defined COMPLEX -valued Function-like V116() Element of K6(K7(REAL,COMPLEX))
A is non empty V126() V127() V128() closed_interval V224() V259() V260() Element of K6(REAL)
(A,f) is complex Element of COMPLEX
Re f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Re f),A) is complex real ext-real Element of REAL
(Re f) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
K7(A,REAL) is V116() V117() V118() set
K6(K7(A,REAL)) is set
integral ((Re f) || A) is complex real ext-real Element of REAL
Im f is Relation-like REAL -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(REAL,REAL))
integral ((Im f),A) is complex real ext-real Element of REAL
(Im f) || A is Relation-like A -defined REAL -valued Function-like V116() V117() V118() Element of K6(K7(A,REAL))
integral ((Im f) || A) is complex real ext-real Element of REAL
(integral ((Im f),A)) * <i> is complex Element of COMPLEX
(integral ((Re f),A)) + ((integral ((Im f),A)) * <i>) is complex Element of COMPLEX
- (A,f) is complex Element of COMPLEX
b is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
[.b,a.] is V126() V127() V128() Element of K6(REAL)
(a,b,f) is complex Element of COMPLEX
integral ((Re f),a,b) is complex real ext-real Element of REAL
integral ((Im f),a,b) is complex real ext-real Element of REAL
(integral ((Im f),a,b)) * <i> is complex Element of COMPLEX
(integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>) is complex Element of COMPLEX
Re (a,b,f) is complex real ext-real Element of REAL
Im (a,b,f) is complex real ext-real Element of REAL
Re (- (A,f)) is complex real ext-real Element of REAL
Re (A,f) is complex real ext-real Element of REAL
- (Re (A,f)) is complex real ext-real Element of REAL
- (integral ((Re f),A)) is complex real ext-real Element of REAL
Im (- (A,f)) is complex real ext-real Element of REAL
Im (A,f) is complex real ext-real Element of REAL
- (Im (A,f)) is complex real ext-real Element of REAL
- (integral ((Im f),A)) is complex real ext-real Element of REAL