:: INTEGR10 semantic presentation

begin

theorem :: INTEGR10:1
for a, b, g1, M being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) < g1 : ( ( real ) ( V11() real ext-real ) number ) & 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) < M : ( ( real ) ( V11() real ext-real ) number ) holds
ex r being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) st
( a : ( ( real ) ( V11() real ext-real ) number ) < r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) & r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) < b : ( ( real ) ( V11() real ext-real ) number ) & (b : ( ( real ) ( V11() real ext-real ) number ) - r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) * M : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) < g1 : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: INTEGR10:2
for a, b, g1, M being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) < g1 : ( ( real ) ( V11() real ext-real ) number ) & 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) < M : ( ( real ) ( V11() real ext-real ) number ) holds
ex r being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) st
( a : ( ( real ) ( V11() real ext-real ) number ) < r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) & r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) < b : ( ( real ) ( V11() real ext-real ) number ) & (r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) - a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) * M : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) < g1 : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: INTEGR10:3
for b, a being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) holds (exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() continuous ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) . b : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) - (exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() continuous ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() continuous ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ;

begin

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let a, b be ( ( ) ( V11() real ext-real ) Real) ;
pred f is_right_ext_Riemann_integrable_on a,b means :: INTEGR10:def 1
( ( for d being ( ( ) ( V11() real ext-real ) Real) st a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) <= d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) & d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) < b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V13() V18() ) ( V13() V18() ) set ) is_integrable_on ['a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V13() V18() ) ( V13() V18() ) set ) | ['a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) & ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = [.a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .[ : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_left_convergent_in b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let a, b be ( ( ) ( V11() real ext-real ) Real) ;
pred f is_left_ext_Riemann_integrable_on a,b means :: INTEGR10:def 2
( ( for d being ( ( ) ( V11() real ext-real ) Real) st a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) < d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) & d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) <= b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V13() V18() ) ( V13() V18() ) set ) is_integrable_on ['d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V13() V18() ) ( V13() V18() ) set ) | ['d : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) & ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = ].a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .] : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_right_convergent_in a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let a, b be ( ( ) ( V11() real ext-real ) Real) ;
assume f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_right_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ;
func ext_right_integral (f,a,b) -> ( ( ) ( V11() real ext-real ) Real) means :: INTEGR10:def 3
 ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = [.a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .[ : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_left_convergent_in b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & it : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = lim_left (Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let a, b be ( ( ) ( V11() real ext-real ) Real) ;
assume f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_left_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ;
func ext_left_integral (f,a,b) -> ( ( ) ( V11() real ext-real ) Real) means :: INTEGR10:def 4
 ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = ].a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .] : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_right_convergent_in a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) & it : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = lim_right (Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let a be ( ( real ) ( V11() real ext-real ) number ) ;
pred f is_+infty_ext_Riemann_integrable_on a means :: INTEGR10:def 5
( ( for b being ( ( ) ( V11() real ext-real ) Real) st a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) <= b : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) holds
( f : ( ( V13() V18() ) ( V13() V18() ) set ) is_integrable_on ['a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,b : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V13() V18() ) ( V13() V18() ) set ) | ['a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,b : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) & ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = right_closed_halfline a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is convergent_in+infty ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let b be ( ( real ) ( V11() real ext-real ) number ) ;
pred f is_-infty_ext_Riemann_integrable_on b means :: INTEGR10:def 6
( ( for a being ( ( ) ( V11() real ext-real ) Real) st a : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) <= b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) holds
( f : ( ( V13() V18() ) ( V13() V18() ) set ) is_integrable_on ['a : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V13() V18() ) ( V13() V18() ) set ) | ['a : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) & ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = left_closed_halfline b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is convergent_in-infty ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let a be ( ( real ) ( V11() real ext-real ) number ) ;
assume f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_+infty_ext_Riemann_integrable_on a : ( ( real ) ( V11() real ext-real ) number ) ;
func infty_ext_right_integral (f,a) -> ( ( ) ( V11() real ext-real ) Real) means :: INTEGR10:def 7
 ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = right_closed_halfline a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is convergent_in+infty & it : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,a : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = lim_in+infty Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
let b be ( ( real ) ( V11() real ext-real ) number ) ;
assume f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_-infty_ext_Riemann_integrable_on b : ( ( real ) ( V11() real ext-real ) number ) ;
func infty_ext_left_integral (f,b) -> ( ( ) ( V11() real ext-real ) Real) means :: INTEGR10:def 8
 ex Intf being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st
( dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = left_closed_halfline b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in dom Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,x : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) & Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is convergent_in-infty & it : ( ( V18() ) ( V13() V16(f : ( ( V13() V18() ) ( V13() V18() ) set ) ) V17(b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(f : ( ( V13() V18() ) ( V13() V18() ) set ) ,b : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = lim_in-infty Intf : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
attr f is infty_ext_Riemann_integrable means :: INTEGR10:def 9
( f : ( ( V13() V18() ) ( V13() V18() ) set ) is_+infty_ext_Riemann_integrable_on 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( V13() V18() ) ( V13() V18() ) set ) is_-infty_ext_Riemann_integrable_on 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) );
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
func infty_ext_integral f -> ( ( ) ( V11() real ext-real ) Real) equals :: INTEGR10:def 10
(infty_ext_right_integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Real) + (infty_ext_left_integral (f : ( ( V13() V18() ) ( V13() V18() ) set ) ,0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ;
end;

begin

theorem :: INTEGR10:4
for f, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a, b being ( ( ) ( V11() real ext-real ) Real) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_right_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_right_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) holds
( f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_right_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) & ext_right_integral ((f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Real) = (ext_right_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( V11() real ext-real ) Real) + (ext_right_integral (g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:5
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a, b being ( ( ) ( V11() real ext-real ) Real) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_right_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) holds
for r being ( ( ) ( V11() real ext-real ) Real) holds
( r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_right_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) & ext_right_integral ((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Real) = r : ( ( ) ( V11() real ext-real ) Real) * (ext_right_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:6
for f, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a, b being ( ( ) ( V11() real ext-real ) Real) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_left_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_left_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) holds
( f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_left_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) & ext_left_integral ((f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Real) = (ext_left_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( V11() real ext-real ) Real) + (ext_left_integral (g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:7
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a, b being ( ( ) ( V11() real ext-real ) Real) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_left_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) holds
for r being ( ( ) ( V11() real ext-real ) Real) holds
( r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_left_ext_Riemann_integrable_on a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) & ext_left_integral ((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Real) = r : ( ( ) ( V11() real ext-real ) Real) * (ext_left_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:8
for f, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a being ( ( real ) ( V11() real ext-real ) number ) st right_closed_halfline a : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & right_closed_halfline a : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_+infty_ext_Riemann_integrable_on a : ( ( real ) ( V11() real ext-real ) number ) & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_+infty_ext_Riemann_integrable_on a : ( ( real ) ( V11() real ext-real ) number ) holds
( f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_+infty_ext_Riemann_integrable_on a : ( ( real ) ( V11() real ext-real ) number ) & infty_ext_right_integral ((f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Real) = (infty_ext_right_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Real) + (infty_ext_right_integral (g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:9
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a being ( ( real ) ( V11() real ext-real ) number ) st right_closed_halfline a : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_+infty_ext_Riemann_integrable_on a : ( ( real ) ( V11() real ext-real ) number ) holds
for r being ( ( ) ( V11() real ext-real ) Real) holds
( r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_+infty_ext_Riemann_integrable_on a : ( ( real ) ( V11() real ext-real ) number ) & infty_ext_right_integral ((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Real) = r : ( ( ) ( V11() real ext-real ) Real) * (infty_ext_right_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:10
for f, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for b being ( ( real ) ( V11() real ext-real ) number ) st left_closed_halfline b : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & left_closed_halfline b : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_-infty_ext_Riemann_integrable_on b : ( ( real ) ( V11() real ext-real ) number ) & g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_-infty_ext_Riemann_integrable_on b : ( ( real ) ( V11() real ext-real ) number ) holds
( f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_-infty_ext_Riemann_integrable_on b : ( ( real ) ( V11() real ext-real ) number ) & infty_ext_left_integral ((f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Real) = (infty_ext_left_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Real) + (infty_ext_left_integral (g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:11
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for b being ( ( real ) ( V11() real ext-real ) number ) st left_closed_halfline b : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_-infty_ext_Riemann_integrable_on b : ( ( real ) ( V11() real ext-real ) number ) holds
for r being ( ( ) ( V11() real ext-real ) Real) holds
( r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_-infty_ext_Riemann_integrable_on b : ( ( real ) ( V11() real ext-real ) number ) & infty_ext_left_integral ((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Real) = r : ( ( ) ( V11() real ext-real ) Real) * (infty_ext_left_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ;

theorem :: INTEGR10:12
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a, b being ( ( ) ( V11() real ext-real ) Real) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_integrable_on ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) | ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
ext_right_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Real) = integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ;

theorem :: INTEGR10:13
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a, b being ( ( ) ( V11() real ext-real ) Real) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) is_integrable_on ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) | ['a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) '] : ( ( non empty V63() ) ( non empty V55() V56() V57() V63() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
ext_left_integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Real) = integral (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ,a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ;

begin

definition
let s be ( ( real ) ( V11() real ext-real ) number ) ;
func exp*- s -> ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() ) Function of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) means :: INTEGR10:def 11
 for t being ( ( ) ( V11() real ext-real ) Real) holds it : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) . t : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = exp_R : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() continuous ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) . (- (s : ( ( V13() V18() ) ( V13() V18() ) set ) * t : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ;
end;

definition
let f be ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ;
func One-sided_Laplace_transform f -> ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) means :: INTEGR10:def 12
( dom it : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = right_open_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for s being ( ( ) ( V11() real ext-real ) Real) st s : ( ( ) ( V11() real ext-real ) Real) in dom it : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
it : ( ( natural ) ( ordinal natural V11() real ext-real non negative ) set ) . s : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) = infty_ext_right_integral ((f : ( ( V13() V18() ) ( V13() V18() ) set ) (#) (exp*- s : ( ( ) ( V11() real ext-real ) Real) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() ) Function of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ,0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Real) ) );
end;

begin

theorem :: INTEGR10:14
for f, g being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) st dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = right_closed_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & dom g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = right_closed_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for s being ( ( ) ( V11() real ext-real ) Real) st s : ( ( ) ( V11() real ext-real ) Real) in right_open_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) (#) (exp*- s : ( ( ) ( V11() real ext-real ) Real) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() ) Function of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_+infty_ext_Riemann_integrable_on 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for s being ( ( ) ( V11() real ext-real ) Real) st s : ( ( ) ( V11() real ext-real ) Real) in right_open_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) (#) (exp*- s : ( ( ) ( V11() real ext-real ) Real) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() ) Function of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_+infty_ext_Riemann_integrable_on 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
( ( for s being ( ( ) ( V11() real ext-real ) Real) st s : ( ( ) ( V11() real ext-real ) Real) in right_open_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
(f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) (#) (exp*- s : ( ( ) ( V11() real ext-real ) Real) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() ) Function of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_+infty_ext_Riemann_integrable_on 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) & One-sided_Laplace_transform (f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) = (One-sided_Laplace_transform f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) + (One-sided_Laplace_transform g : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: INTEGR10:15
for f being ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,)
for a being ( ( ) ( V11() real ext-real ) Real) st dom f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) = right_closed_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for s being ( ( ) ( V11() real ext-real ) Real) st s : ( ( ) ( V11() real ext-real ) Real) in right_open_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) (#) (exp*- s : ( ( ) ( V11() real ext-real ) Real) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() ) Function of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_+infty_ext_Riemann_integrable_on 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
( ( for s being ( ( ) ( V11() real ext-real ) Real) st s : ( ( ) ( V11() real ext-real ) Real) in right_open_halfline 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V55() V56() V57() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) (#) (exp*- s : ( ( ) ( V11() real ext-real ) Real) ) : ( ( V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V27( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V41() V42() V43() ) Function of REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) , REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) is_+infty_ext_Riemann_integrable_on 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() ) Element of NAT : ( ( ) ( V55() V56() V57() V58() V59() V60() V61() ) Element of K6(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) & One-sided_Laplace_transform (a : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) = a : ( ( ) ( V11() real ext-real ) Real) (#) (One-sided_Laplace_transform f : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) ) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) PartFunc of ,) : ( ( V18() ) ( V13() V16( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V17( REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) V18() V41() V42() V43() ) Element of K6(K7(REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ,REAL : ( ( ) ( non empty V55() V56() V57() V61() V68() ) set ) ) : ( ( ) ( V41() V42() V43() ) set ) ) : ( ( ) ( ) set ) ) ) ;