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