let a, b be real number ; :: thesis: for X being set
for f being PartFunc of REAL ,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds
( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )
let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds
( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )
let f be PartFunc of REAL ,REAL ; :: thesis: ( a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous implies ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) )
assume a <= b ; :: thesis: ( not [.a,b.] c= X or not X c= dom f or not f | X is continuous or ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) )
then A1: [.a,b.] = ['a,b'] by INTEGRA5:def 4;
assume Z: ( [.a,b.] c= X & X c= dom f & f | X is continuous ) ; :: thesis: ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )
then X: [.a,b.] c= dom f by XBOOLE_1:1;
thus f | ['a,b'] is continuous by A1, Z, FCONT_1:17; :: thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )
hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, X, INTEGRA5:10, INTEGRA5:17; :: thesis: verum