let a, b, e, c, d be real number ; :: thesis: for f being PartFunc of REAL ,REAL st a <= b & ( for x being real number 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 number 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 A1: ( a <= b & ( for x being real number st x in ['a,b'] holds
f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral f,c,d = e * (d - c)
then ['a,b'] = [.a,b.] by INTEGRA5:def 4;
then A2: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;
then A3: ( ['c,b'] c= ['a,b'] & ['a,c'] c= ['a,b'] ) by Lm3;
A4: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) by A1, Th26;

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

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

then A6: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) by A2, A4, Th18;
['c,d'] c= ['c,b'] by A2, A5, Lm3;
then ['c,d'] c= ['a,b'] by A3, XBOOLE_1:1;
then for x being real number st x in ['c,d'] holds
f . x = e by A1;
hence integral f,c,d = e * (d - c) by A5, A6, Th26; :: thesis: verum

end;

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

then A8: ( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded & ['d,c'] c= dom f ) by A2, A4, Th18;
['d,c'] c= ['a,c'] by A2, A7, Lm3;
then ['d,c'] c= ['a,b'] by A3, XBOOLE_1:1;
then for x being real number st x in ['d,c'] holds
f . x = e by A1;
then A9: integral f,d,c = e * (c - d) by A7, A8, Th26;
integral f,c,d = - (integral f,['d,c']) by A7, INTEGRA5:def 5;
then integral f,c,d = - (integral f,d,c) by A7, INTEGRA5:def 5;
hence integral f,c,d = e * (d - c) by A9; :: thesis: verum

end;

end;