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 ;
then A8: c <= b by ;
A9: a <= c by ;
then A10: ['c,b'] c= ['a,b'] by ;
A11: d <= b by ;
A12: a <= d by ;
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 ;
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 ; :: thesis: verum
end;
suppose A16: not c <= d ; :: thesis: integral (f,c,d) = e * (d - c)
then ['d,c'] c= ['a,c'] by ;
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 ;
then A18: integral (f,c,d) = - (integral (f,d,c)) by ;
['d,c'] c= dom f by A3, A12, A8, A6, A16, Th18;
then integral (f,d,c) = e * (c - d) by ;
hence integral (f,c,d) = e * (d - c) by A18; :: thesis: verum
end;
end;