let a, b, c, d be Real; :: thesis: for Y being RealBanachSpace

for f being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds

f is_integrable_on ['c,d']

let Y be RealBanachSpace; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds

f is_integrable_on ['c,d']

let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f implies f is_integrable_on ['c,d'] )

assume A1: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f ) ; :: thesis: f is_integrable_on ['c,d']

then A2: ( c <= b & a <= d ) by XXREAL_0:2;

then A4: ( c in ['a,b'] & d in ['a,b'] ) by A1, INTEGR19:1;

( c = min (c,d) & d = max (c,d) ) by A1, XXREAL_0:def 9, XXREAL_0:def 10;

then ['c,d'] c= ['a,b'] by A2, A1, XXREAL_0:2, A4, Lm2;

then ['c,d'] c= dom f by A1;

hence f is_integrable_on ['c,d'] by A1, INTEGR20:19; :: thesis: verum

for f being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds

f is_integrable_on ['c,d']

let Y be RealBanachSpace; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds

f is_integrable_on ['c,d']

let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f implies f is_integrable_on ['c,d'] )

assume A1: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f ) ; :: thesis: f is_integrable_on ['c,d']

then A2: ( c <= b & a <= d ) by XXREAL_0:2;

then A4: ( c in ['a,b'] & d in ['a,b'] ) by A1, INTEGR19:1;

( c = min (c,d) & d = max (c,d) ) by A1, XXREAL_0:def 9, XXREAL_0:def 10;

then ['c,d'] c= ['a,b'] by A2, A1, XXREAL_0:2, A4, Lm2;

then ['c,d'] c= dom f by A1;

hence f is_integrable_on ['c,d'] by A1, INTEGR20:19; :: thesis: verum