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