let a, b be Real; :: 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 3;
assume that
A2: [.a,b.] c= X and
A3: X c= dom f and
A4: f | X is continuous ; :: thesis: ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )
thus A5: f | ['a,b'] is continuous by A1, A2, A4, FCONT_1:16; :: thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )
[.a,b.] c= dom f by A2, A3;
hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A5, INTEGRA5:10, INTEGRA5:17; :: thesis: verum