func R2-to-C -> ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like total quasi_total complex-valued ) Function of [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) , COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) means :: INTEGR1C:def 1
for p being ( ( ) ( ) Element of [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) )
for a, b being ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) st a : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) = p : ( ( ) ( ) Element of [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) ) `1 : ( ( ) ( ) set ) & b : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) = p : ( ( ) ( ) Element of [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) ) `2 : ( ( ) ( ) set ) holds
it : ( ( V58() right_end ) ( V58() right_end ) set ) . [a : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) ,b : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) ] : ( ( ) ( V24() ) set ) : ( ( ) ( ) set ) = a : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) + (b : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;

func integral (f,x,y,a,b,Z) -> ( ( complex ) ( complex ) Complex) means :: INTEGR1C:def 2
ex u0, v0 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st
( u0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) = ((Re f : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued complex-valued ext-real-valued real-valued ) Element of bool b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) * R2-to-C : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like total quasi_total complex-valued ) Function of [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) , COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) ) : ( ( Function-like ) ( Relation-like [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:[:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) * <:x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,y : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( Relation-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) & v0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) = ((Im f : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued complex-valued ext-real-valued real-valued ) Element of bool b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) * R2-to-C : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like total quasi_total complex-valued ) Function of [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) , COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) ) : ( ( Function-like ) ( Relation-like [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:[:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) * <:x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,y : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( Relation-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) & it : ( ( ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued complex-valued ext-real-valued real-valued ) Element of bool x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = (integral (((u0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `| Z : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) - (v0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (y : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `| Z : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) + ((integral (((v0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `| Z : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) + (u0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (y : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `| Z : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,x : ( ( Function-like ) ( Relation-like a : ( ( V58() right_end ) ( V58() right_end ) set ) -defined b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( V58() right_end ) ( V58() right_end ) set ) ,b : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) );

attr C is C1-curve-like means :: INTEGR1C:def 3
ex a, b being ( ( ) ( complex real ext-real ) Real) ex x, y being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ex Z being ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( complex real ext-real ) Real) <= b : ( ( ) ( complex real ext-real ) Real) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) = dom C : ( ( V58() right_end ) ( V58() right_end ) set ) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= dom x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= dom y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) is open & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is continuous & y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is continuous & C : ( ( V58() right_end ) ( V58() right_end ) set ) = (x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + (<i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) (#) y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) | [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined [.b₁ : ( ( ) ( complex real ext-real ) Real) ,b₂ : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) );

cluster Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued C1-curve-like for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) ;

func integral (f,C) -> ( ( complex ) ( complex ) Complex) means :: INTEGR1C:def 4
ex a, b being ( ( ) ( complex real ext-real ) Real) ex x, y being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ex Z being ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( complex real ext-real ) Real) <= b : ( ( ) ( complex real ext-real ) Real) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) = dom C : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= dom x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= dom y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) is open & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is continuous & y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is continuous & C : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) = (x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + (<i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) (#) y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) | [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined [.b₁ : ( ( ) ( complex real ext-real ) Real) ,b₂ : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) & it : ( ( Function-like ) ( Relation-like f : ( ( V58() right_end ) ( V58() right_end ) set ) -defined C : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:f : ( ( V58() right_end ) ( V58() right_end ) set ) ,C : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = integral (f : ( ( V58() right_end ) ( V58() right_end ) set ) ,x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ,y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ,a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( complex ) ( complex ) Complex) );

pred f is_integrable_on C means :: INTEGR1C:def 5
for a, b being ( ( ) ( complex real ext-real ) Real)
for x, y being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for Z being ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) )
for u0, v0 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st a : ( ( ) ( complex real ext-real ) Real) <= b : ( ( ) ( complex real ext-real ) Real) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) = dom C : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= dom x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= dom y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) is open & [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) c= Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is continuous & y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is continuous & C : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) = (x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + (<i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) ) (#) y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) | [.a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined [.b₁ : ( ( ) ( complex real ext-real ) Real) ,b₂ : ( ( ) ( complex real ext-real ) Real) .] : ( ( ) ( V57() V58() V59() ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) -valued Function-like complex-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,COMPLEX : ( ( ) ( non empty V39() V57() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ) set ) : ( ( ) ( non empty ) set ) ) holds
( (u0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) - (v0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is_integrable_on ['a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) '] : ( ( non empty closed_interval ) ( non empty V57() V58() V59() closed_interval interval ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) & (v0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (x : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) + (u0 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (y : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -defined REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) :] : ( ( ) ( non empty Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty ) set ) ) is_integrable_on ['a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) '] : ( ( non empty closed_interval ) ( non empty V57() V58() V59() closed_interval interval ) Element of bool REAL : ( ( ) ( non empty V39() V57() V58() V59() V63() ) set ) : ( ( ) ( non empty ) set ) ) );