:: INTEGRA7 semantic presentation

begin

theorem :: INTEGRA7:1
for a being ( ( real ) ( V11() real ext-real ) number )
for A being ( ( non empty ) ( non empty ) set )
for f, g being ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of A : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) st rng f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) is bounded_above & rng g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) is bounded_above & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in A : ( ( non empty ) ( non empty ) set ) holds
abs ((f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <= a : ( ( real ) ( V11() real ext-real ) number ) ) holds
( (upper_bound (rng f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (upper_bound (rng g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <= a : ( ( real ) ( V11() real ext-real ) number ) & (upper_bound (rng g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (upper_bound (rng f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <= a : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: INTEGRA7:2
for a being ( ( real ) ( V11() real ext-real ) number )
for A being ( ( non empty ) ( non empty ) set )
for f, g being ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of A : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) st rng f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) is bounded_below & rng g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) is bounded_below & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in A : ( ( non empty ) ( non empty ) set ) holds
abs ((f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <= a : ( ( real ) ( V11() real ext-real ) number ) ) holds
( (lower_bound (rng f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (lower_bound (rng g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <= a : ( ( real ) ( V11() real ext-real ) number ) & (lower_bound (rng g : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (lower_bound (rng f : ( ( V18() V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16(b2 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27(b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Function of b2 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <= a : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: INTEGRA7:3
for X being ( ( ) ( ) set )
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded ;

theorem :: INTEGRA7:4
for X being ( ( ) ( ) set )
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,)
for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in X : ( ( ) ( ) set ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x : ( ( ) ( V11() real ext-real ) Real) holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_in x : ( ( ) ( V11() real ext-real ) Real) ;

theorem :: INTEGRA7:5
for X being ( ( ) ( ) set )
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on X : ( ( ) ( ) set ) holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) ;

theorem :: INTEGRA7:6
for X being ( ( ) ( ) set )
for f, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
( f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on X : ( ( ) ( ) set ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) - g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on X : ( ( ) ( ) set ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on X : ( ( ) ( ) set ) ) ;

theorem :: INTEGRA7:7
for r being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
r : ( ( real ) ( V11() real ext-real ) number ) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on X : ( ( ) ( ) set ) ;

theorem :: INTEGRA7:8
for X being ( ( ) ( ) set )
for g, f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <> 0 : ( ( ) ( empty natural V11() real ext-real V50() V51() V52() V53() V54() V55() V56() V89() V90() bounded_below V100() ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) / g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on X : ( ( ) ( ) set ) ;

theorem :: INTEGRA7:9
for X being ( ( ) ( ) set )
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <> 0 : ( ( ) ( empty natural V11() real ext-real V50() V51() V52() V53() V54() V55() V56() V89() V90() bounded_below V100() ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ^ : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on X : ( ( ) ( ) set ) ;

theorem :: INTEGRA7:10
for a, b being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for F being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) `| X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) | ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . b : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = (integral ((F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) + (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

begin

definition
let X be ( ( ) ( ) set ) ;
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ;
func IntegralFuncs (f,X) -> ( ( ) ( ) set ) means :: INTEGRA7:def 1
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) iff ex F being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st
( x : ( ( ) ( ) set ) = F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_differentiable_on X : ( ( real ) ( V11() real ext-real ) set ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) `| X : ( ( real ) ( V11() real ext-real ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) = f : ( ( real ) ( V11() real ext-real ) set ) | X : ( ( real ) ( V11() real ext-real ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ) );
end;

definition
let X be ( ( ) ( ) set ) ;
let F, f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ;
pred F is_integral_of f,X means :: INTEGRA7:def 2
F : ( ( real ) ( V11() real ext-real ) set ) in IntegralFuncs (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,X : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( ) set ) ;
end;

theorem :: INTEGRA7:11
for X being ( ( ) ( ) set )
for F, f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= dom F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: INTEGRA7:12
for X being ( ( ) ( ) set )
for F, f, G, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) & G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
( F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) + G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,X : ( ( ) ( ) set ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) - G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) - g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,X : ( ( ) ( ) set ) ) ;

theorem :: INTEGRA7:13
for r being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for F, f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
r : ( ( real ) ( V11() real ext-real ) number ) (#) F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of r : ( ( real ) ( V11() real ext-real ) number ) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,X : ( ( ) ( ) set ) ;

theorem :: INTEGRA7:14
for X being ( ( ) ( ) set )
for F, f, G, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) & G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) + (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,X : ( ( ) ( ) set ) ;

theorem :: INTEGRA7:15
for X being ( ( ) ( ) set )
for G, F, f, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) <> 0 : ( ( ) ( empty natural V11() real ext-real V50() V51() V52() V53() V54() V55() V56() V89() V90() bounded_below V100() ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) & G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) / G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of ((f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) - (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) / (G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,X : ( ( ) ( ) set ) ;

theorem :: INTEGRA7:16
for a, b being ( ( real ) ( V11() real ext-real ) number )
for f, F being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is continuous & ].a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() open non left_end non right_end V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) in ].a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() open non left_end non right_end V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = (integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,a : ( ( real ) ( V11() real ext-real ) number ) ,x : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) + (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,].a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() open non left_end non right_end V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: INTEGRA7:17
for a, b being ( ( real ) ( V11() real ext-real ) number )
for f, F being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,)
for x, x0 being ( ( real ) ( V11() real ext-real ) number ) st f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() closed V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is continuous & [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() closed V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & x : ( ( real ) ( V11() real ext-real ) number ) in ].a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() open non left_end non right_end V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & x0 : ( ( real ) ( V11() real ext-real ) number ) in ].a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() open non left_end non right_end V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,].a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() open non left_end non right_end V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = (integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,x0 : ( ( real ) ( V11() real ext-real ) number ) ,x : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) + (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . x0 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

theorem :: INTEGRA7:18
for a, b being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for F, f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integrable_on ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . b : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = (integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) + (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

theorem :: INTEGRA7:19
for a, b being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() closed V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is continuous holds
( f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integrable_on ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ;

theorem :: INTEGRA7:20
for a, b being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for f, F being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() closed V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is continuous & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . b : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = (integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) + (F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

theorem :: INTEGRA7:21
for b, a being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for f, g, F, G being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st b : ( ( real ) ( V11() real ext-real ) number ) <= a : ( ( real ) ( V11() real ext-real ) number ) & ['b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integrable_on ['b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integrable_on ['b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | ['b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | ['b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded & X : ( ( ) ( ) set ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & X : ( ( ) ( ) set ) c= dom g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) & G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
((F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) * (G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - ((F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) * (G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = (integral ((f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) + (integral ((F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

theorem :: INTEGRA7:22
for b, a being ( ( real ) ( V11() real ext-real ) number )
for X being ( ( ) ( ) set )
for f, g, F, G being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) st b : ( ( real ) ( V11() real ext-real ) number ) <= a : ( ( real ) ( V11() real ext-real ) number ) & [.b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() closed V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & X : ( ( ) ( ) set ) c= dom g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) : ( ( ) ( V50() V51() V52() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is continuous & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is continuous & F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) & G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) is_integral_of g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ,X : ( ( ) ( ) set ) holds
((F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) * (G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - ((F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) * (G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = (integral ((f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) G : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) + (integral ((F : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) (#) g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

begin

theorem :: INTEGRA7:23
sin : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of cos : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ;

theorem :: INTEGRA7:24
for b, a being ( ( real ) ( V11() real ext-real ) number ) holds (sin : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (sin : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = integral (cos : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

theorem :: INTEGRA7:25
(- 1 : ( ( ) ( non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real V89() ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) (#) cos : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of sin : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ;

theorem :: INTEGRA7:26
for a, b being ( ( real ) ( V11() real ext-real ) number ) holds (cos : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (cos : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = integral (sin : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

theorem :: INTEGRA7:27
exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ;

theorem :: INTEGRA7:28
for b, a being ( ( real ) ( V11() real ext-real ) number ) holds (exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - (exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = integral (exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

theorem :: INTEGRA7:29
for n being ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds #Z (n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integral_of (n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) (#) (#Z n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ;

theorem :: INTEGRA7:30
for b, a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds ((#Z (n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) - ((#Z (n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = integral (((n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) (#) (#Z n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V18() ) ( non empty V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ;

begin

theorem :: INTEGRA7:31
for a, b being ( ( real ) ( V11() real ext-real ) number )
for H being ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) )
for rseq being ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Real_Sequence) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & ( for n being ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( H : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) . n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & (H : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) . n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) | ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded & rseq : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Real_Sequence) . n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = integral ((H : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) . n : ( ( ) ( natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below ) Element of NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ) & H : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) is_unif_conv_on ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) holds
( (lim (H : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ,['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) | ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is bounded & lim (H : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ,['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) is_integrable_on ['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) & rseq : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Real_Sequence) is convergent & lim rseq : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() total V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V40() V41() V42() ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) = integral ((lim (H : ( ( V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) ( V13() V16( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) V18() V27( NAT : ( ( ) ( V50() V51() V52() V53() V54() V55() V56() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) , PFuncs (REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) ) Functional_Sequence of ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ,['a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) '] : ( ( non empty V72() ) ( non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() ) Element of K6(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V17( REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) V18() V40() V41() V42() ) Element of K6(K7(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ,REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) : ( ( ) ( V40() V41() V42() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() ) set ) ) ) ;