:: INTEGR16 semantic presentation

begin

theorem :: INTEGR16:1
for z being ( ( complex ) ( complex ) number )
for r being ( ( real ) ( complex real ext-real ) number ) holds
( Re (r : ( ( real ) ( complex real ext-real ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = r : ( ( real ) ( complex real ext-real ) number ) * (Re z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) & Im (r : ( ( real ) ( complex real ext-real ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = r : ( ( real ) ( complex real ext-real ) number ) * (Im z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ) ;

registration
let S be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
cluster Re S : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like FinSequence-like ;
cluster Im S : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like FinSequence-like ;
end;

definition
let S be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
:: original: Re
redefine func Re S -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;
:: original: Im
redefine func Im S -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;
end;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
let D be ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ;
mode middle_volume of f,D -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) means :: INTEGR16:def 1
( len it : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined K473(D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) -valued Function-like ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,K473(D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) = len D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for i being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real ) Nat) st i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real ) Nat) in dom D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V126() V127() V128() V129() V130() V131() ) Element of K6(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
ex c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) st
( c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) in rng (f : ( ( ) ( ) set ) | (divset (D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real ) Nat) )) : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like A : ( ( ) ( ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(A : ( ( ) ( ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V126() ) Element of K6(COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( ) set ) ) & it : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined K473(D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) -valued Function-like ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,K473(D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real ) Nat) : ( ( ) ( ) set ) = c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) * (vol (divset (D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ,i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real ) Nat) )) : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) ) );
end;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
let D be ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ;
let F be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of f : ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) ;
func middle_sum (f,F) -> ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) equals :: INTEGR16:def 2
 Sum F : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined K473(D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) -valued Function-like ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,K473(D : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
end;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
let T be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ;
mode middle_volume_Sequence of f,T -> ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) ) means :: INTEGR16:def 3
 for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) -valued Function-like ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( FinSequence-like ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) ) is ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of f : ( ( ) ( ) set ) ,T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) . k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( ) ( ) set ) ) ) ;
end;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
let T be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ;
let S be ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of f : ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) ;
let k be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ;
:: original: .
redefine func S . k -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of f : ( ( ) ( ) set ) ,T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) . k : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined K473(A : ( ( ) ( ) set ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) * : ( ( ) ( non empty functional FinSequence-membered ) M10(K473(A : ( ( ) ( ) set ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) )) -valued Function-like total quasi_total ) middle_volume_Sequence of T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ,S : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) -valued Function-like ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( ) ( ) set ) ) ) ;
end;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
let T be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ;
let S be ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of f : ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) ;
func middle_sum (f,S) -> ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Complex_Sequence) means :: INTEGR16:def 4
 for i being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined K473(A : ( ( ) ( ) set ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) * : ( ( ) ( non empty functional FinSequence-membered ) M10(K473(A : ( ( ) ( ) set ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) )) -valued Function-like total quasi_total ) middle_volume_Sequence of T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ,S : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) -valued Function-like ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex FinSequence-like ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = middle_sum (f : ( ( ) ( ) set ) ,(S : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) -valued Function-like ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,K473(T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) M10( REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of f : ( ( ) ( ) set ) ,T : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) . b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
end;

begin

theorem :: INTEGR16:2
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,)
for A being ( ( ) ( V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) holds Re (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( ) ( V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) = (Re f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) | A : ( ( ) ( V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: INTEGR16:3
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,)
for A being ( ( ) ( V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) holds Im (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( ) ( V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) = (Im f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) | A : ( ( ) ( V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ;

registration
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
cluster Re f : ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Element of K6(K7(A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Function-like quasi_total for ( ( Function-like ) ( Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) PartFunc of ,) ;
cluster Im f : ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Element of K6(K7(A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Function-like quasi_total for ( ( Function-like ) ( Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) PartFunc of ,) ;
end;

theorem :: INTEGR16:4
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for D being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )
for S being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) holds
( Re S : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) is ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Re f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) & Im S : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) is ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Im f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) ) ;

theorem :: INTEGR16:5
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for x being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) holds Re (F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ^ <*x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() V39(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = (Re F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ^ <*(Re x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() V39(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;

theorem :: INTEGR16:6
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for x being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) holds Im (F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ^ <*x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() V39(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = (Im F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ^ <*(Im x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() V39(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;

theorem :: INTEGR16:7
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for Fr being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) st Fr : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = Re F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) holds
Sum Fr : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = Re (Sum F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;

theorem :: INTEGR16:8
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for Fi being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) st Fi : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = Im F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) holds
Sum Fi : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = Im (Sum F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) FinSequence of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;

theorem :: INTEGR16:9
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for D being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) )
for Fr being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Re f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) st Fr : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Re b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) = Re F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) holds
Re (middle_sum (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = middle_sum ((Re f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,Fr : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Re b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;

theorem :: INTEGR16:10
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for D being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) )
for Fi being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Im f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,D : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) st Fi : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Im b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) = Im F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) FinSequence of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) holds
Im (middle_sum (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() ) middle_volume of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = middle_sum ((Im f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,Fi : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V32() FinSequence-like FinSubsequence-like V116() V117() V118() ) middle_volume of Im b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,b3 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like one-to-one V32() FinSequence-like FinSubsequence-like V116() V117() V118() V120() V122() ) Division of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) ;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
attr f is integrable means :: INTEGR16:def 5
( Re f : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like A : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(A : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is integrable & Im f : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like A : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(A : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is integrable );
end;

theorem :: INTEGR16:11
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) is bounded iff ( Re f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is bounded & Im f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) ;

theorem :: INTEGR16:12
for A being ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,)
for g being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) = g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) holds
( Re f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) = Re g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) & Im f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) = Im g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty V126() V127() V128() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: INTEGR16:13
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) is bounded iff ( Re f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is bounded & Im f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( Function-like ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) ;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
func integral f -> ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) equals :: INTEGR16:def 6
(integral (Re f : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like A : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(A : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) + ((integral (Im f : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like A : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(A : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
end;

theorem :: INTEGR16:14
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )
for T being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) )
for S being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) is bounded & f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) is integrable & delta T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (delta T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( middle_sum (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,S : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Complex_Sequence) is convergent & lim (middle_sum (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,S : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Complex_Sequence) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = integral f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) ;

theorem :: INTEGR16:15
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) is bounded holds
( f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) is integrable iff ex I being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) st
for T being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) )
for S being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) st delta T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (delta T : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like total quasi_total V116() V117() V118() ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( middle_sum (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,S : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b4 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Complex_Sequence) is convergent & lim (middle_sum (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,S : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) )) -valued Function-like total quasi_total ) middle_volume_Sequence of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ,b4 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined divs b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) DivSequence of ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Complex_Sequence) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = I : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) ) ;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ;
pred f is_integrable_on A means :: INTEGR16:def 7
( Re f : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on A : ( ( ) ( ) set ) & Im f : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on A : ( ( ) ( ) set ) );
end;

definition
let A be ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ;
func integral (f,A) -> ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) equals :: INTEGR16:def 8
(integral ((Re f : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( ) set ) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) + ((integral ((Im f : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( ) set ) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
end;

theorem :: INTEGR16:16
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,)
for g being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) = g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) iff g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) is integrable ) ;

theorem :: INTEGR16:17
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,)
for g being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) = g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) holds
integral (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = integral g : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like total quasi_total V116() ) Function of b1 : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) , COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;

definition
let a, b be ( ( real ) ( complex real ext-real ) number ) ;
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ;
func integral (f,a,b) -> ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) equals :: INTEGR16:def 9
(integral ((Re f : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) + ((integral ((Im f : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real V126() V127() V128() V129() V130() V131() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V126() V127() V128() V129() V130() V131() V132() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;
end;

begin

theorem :: INTEGR16:18
for c being ( ( complex ) ( complex ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) holds
( Re (c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) = ((Re c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) (#) (Re f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) - ((Im c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) (#) (Im f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) & Im (c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) = ((Re c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) (#) (Im f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) + ((Im c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) (#) (Re f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -valued Function-like V116() V117() V118() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( V116() V117() V118() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: INTEGR16:19
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) c= dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( ) ( V126() V127() V128() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) & A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) c= dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( ) ( V126() V127() V128() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is bounded & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
( f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & integral ((f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = (integral (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) + (integral (f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) & integral ((f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = (integral (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) - (integral (f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) ;

theorem :: INTEGR16:20
for r being ( ( ) ( complex real ext-real ) Real)
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) st A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( ) ( V126() V127() V128() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
( r : ( ( ) ( complex real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & integral ((r : ( ( ) ( complex real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = r : ( ( ) ( complex real ext-real ) Real) * (integral (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) ;

theorem :: INTEGR16:21
for c being ( ( complex ) ( complex ) number )
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) st A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( ) ( V126() V127() V128() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) | A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
( c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) & integral ((c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) Element of K6(K7(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ,COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( V116() ) set ) ) : ( ( ) ( ) set ) ) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = c : ( ( complex ) ( complex ) number ) * (integral (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ) ;

theorem :: INTEGR16:22
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,)
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( ) ( complex real ext-real ) Real) st A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) = [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V126() V127() V128() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) holds
integral (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = integral (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;

theorem :: INTEGR16:23
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,)
for A being ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( ) ( complex real ext-real ) Real) st A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) = [.b : ( ( ) ( complex real ext-real ) Real) ,a : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V126() V127() V128() ) Element of K6(REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) ) : ( ( ) ( ) set ) ) holds
- (integral (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V126() V127() V128() closed_interval V224() V259() V260() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) = integral (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V32() V126() V127() V128() V132() ) set ) -defined COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) -valued Function-like V116() ) PartFunc of ,) ,a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V32() V126() V132() ) set ) ) ;