let a, b, c, d, e be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ( for x being Real st x in ['a,b'] holds
f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = e * (d - c)
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ( for x being Real st x in ['a,b'] holds
f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = e * (d - c) )
assume that
A1: a <= b and
A2: for x being Real st x in ['a,b'] holds
f . x = e and
A3: ['a,b'] c= dom f and
A4: c in ['a,b'] and
A5: d in ['a,b'] ; :: thesis: integral (f,c,d) = e * (d - c)
A6: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A2, A3, Th26;
A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A8: c <= b by A4, XXREAL_1:1;
A9: a <= c by A4, A7, XXREAL_1:1;
then A10: ['c,b'] c= ['a,b'] by A8, Lm3;
A11: d <= b by A5, A7, XXREAL_1:1;
A12: a <= d by A5, A7, XXREAL_1:1;
A13: ['a,c'] c= ['a,b'] by A9, A8, Lm3;

per cases ( c <= d or not c <= d ) ;

suppose A14: c <= d ; :: thesis: integral (f,c,d) = e * (d - c)

then ['c,d'] c= ['c,b'] by A11, Lm3;
then ['c,d'] c= ['a,b'] by A10;
then A15: for x being Real st x in ['c,d'] holds
f . x = e by A2;
['c,d'] c= dom f by A3, A9, A11, A6, A14, Th18;
hence integral (f,c,d) = e * (d - c) by A14, A15, Th26; :: thesis: verum

end;

suppose A16: not c <= d ; :: thesis: integral (f,c,d) = e * (d - c)

then ['d,c'] c= ['a,c'] by A12, Lm3;
then ['d,c'] c= ['a,b'] by A13;
then A17: for x being Real st x in ['d,c'] holds
f . x = e by A2;
integral (f,c,d) = - (integral (f,['d,c'])) by A16, INTEGRA5:def 4;
then A18: integral (f,c,d) = - (integral (f,d,c)) by A16, INTEGRA5:def 4;
['d,c'] c= dom f by A3, A12, A8, A6, A16, Th18;
then integral (f,d,c) = e * (c - d) by A16, A17, Th26;
hence integral (f,c,d) = e * (d - c) by A18; :: thesis: verum

end;

end;